Journal of Computer Security · 1998 · 506 citations · 0 references
ComputingComputer ScienceCryptographyFormal MethodsSecurity ProtocolsAuthentication ProtocolsCryptographic ProtocolsDeductive VerificationProtocol AnalysisProtocol VerificationSecurity Protocol VerificationCryptographic Protocol AnalysisFormal Methods For Security ProtocolsFormal Verification Of Cryptographic ProtocolsInductive DefinitionsPrincipalsProtocol Formal VerificationPublic-key EncryptionSecurity Properties Of Protocols
Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state systems. Proofs are generated using Isabelle/HOL. The huma