Journal of the ACM · 2005 · 158 citations · 38 references
ComputingComputer ScienceFormal MethodsProgramming LanguagesSecurity ProtocolsCryptographic ProtocolsProtocol AnalysisProtocol VerificationSecurity Protocol VerificationType CheckingType SystemsCryptographic OperationsCryptographic Protocol AnalysisFormal Methods For Security ProtocolsFormal Verification Of Cryptographic ProtocolsFormal Verification Tools For Cryptographic ProtocolsProcess CalculusSecrecy PropertiesSecurity Properties Of Protocols
The study builds on two language‑based techniques for analyzing security protocols—a typed process calculus and untyped logic programs—both focusing on secrecy properties. The authors aim to study and extend these techniques, adding a flexible, generic treatment of many cryptographic operations to the typed process calculus. They extend the typed process calculus with a flexible, generic treatment of many cryptographic operations and further develop both techniques. They establish an equivalence between the typed process calculus and the untyped logic program techniques.
We study and further develop two language-based techniques for analyzing security protocols. One is based on a typed process calculus; the other, on untyped logic programs. Both focus on secrecy properties. We contribute to these two techniques, in particular by extending the former with a flexible, generic treatment of many cryptographic operations. We also establish an equivalence between the two techniques.
38
A calculus for cryptographic protocols
Martı́n Abadi, Andrew D. Gordon · 1997 · 1.2K citations · Full text
Andrew C. Myers · 1999 · 1K citations · Full text