ACM Transactions on Programming Languages and Systems · 2008 · 76 citations · 35 references
ComputingComputer ScienceCybersecurityCryptographyFormal MethodsSecurity ProtocolsCryptographic ProtocolsDeductive VerificationProtocol VerificationSecurity Protocol VerificationVerificationWeb ProtocolsFormal Methods For Security ProtocolsFormal VerificationFormal Verification Of Cryptographic ProtocolsFormal Verification Tools For Cryptographic ProtocolsProtocol Formal VerificationProverifSymbolic Protocol VerificationWeb Services
We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.
35
On the security of public key protocols
Danny Dolev, A. Yao · IEEE Transactions on Information Theory · 1983 · 5.7K citations
A calculus for cryptographic protocols
Martı́n Abadi, Andrew D. Gordon · 1997 · 1.2K citations · Full text
Mobile values, new names, and secure communication
Martı́n Abadi, Cédric Fournet · 2001 · 843 citations