Verified interoperable implementations of security protocols
- 12 December 2008
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 31 (1) , 1-61
- https://doi.org/10.1145/1452044.1452049
Abstract
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.Keywords
This publication has 28 references indexed in Scilit:
- Secure sessions for Web servicesACM Transactions on Information and System Security, 2007
- A semantics for web services authenticationTheoretical Computer Science, 2005
- A hierarchy of equivalences for asynchronous calculiThe Journal of Logic and Algebraic Programming, 2005
- Verification of cryptographic protocols: tagging enforces terminationTheoretical Computer Science, 2005
- On the secure implementation of security protocolsScience of Computer Programming, 2004
- A Calculus for Cryptographic Protocols: The Spi CalculusInformation and Computation, 1999
- Functions as processesMathematical Structures in Computer Science, 1992
- Efficient and timely mutual authenticationACM SIGOPS Operating Systems Review, 1987
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978