A Computationally Sound Mechanized Prover for Security Protocols
Top Cited Papers
- 11 November 2008
- journal article
- research article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Dependable and Secure Computing
- Vol. 5 (4) , 193-207
- https://doi.org/10.1109/tdsc.2007.1005
Abstract
We present a new mechanized prover for secrecy properties of security protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these games are formalized in a probabilistic polynomial-time process calculus. Our tool provides a generic method for specifying security properties of the cryptographic primitives, which can handle shared-key and public-key encryption, signatures, message authentication codes, and hash functions. Our tool produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. We have implemented our tool and tested it on a number of examples of protocols from the literature.Keywords
This publication has 36 references indexed in Scilit:
- A probabilistic polynomial-time process calculus for the analysis of cryptographic protocolsTheoretical Computer Science, 2006
- Password-based authenticated key exchange in the three-party settingIEE Proceedings - Information Security, 2006
- Relating Symbolic and Cryptographic SecrecyIEEE Transactions on Dependable and Secure Computing, 2005
- A computational interpretation of Dolev–Yao adversariesTheoretical Computer Science, 2005
- The Security of the Cipher Block Chaining Message Authentication CodeJournal of Computer and System Sciences, 2000
- Prudent engineering practice for cryptographic protocolsIEEE Transactions on Software Engineering, 1996
- Efficient and timely mutual authenticationACM SIGOPS Operating Systems Review, 1987
- Simple Word Problems in Universal AlgebrasPublished by Springer Nature ,1983
- Timestamps in key distribution protocolsCommunications of the ACM, 1981
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978