Paper 2005/401 Original: eprint.iacr.org/2005/401 ↗
A Computationally Sound Mechanized Prover for Security Protocols
Abstract
We present a new mechanized prover for secrecy properties of cryptographic 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- 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.
Metadata
- Available format(s)
PDF- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2012-06-16: last updated
- 2005-11-14: published
- Short URL
- https://ia.cr/2005/401
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2005/401,
author = {Bruno Blanchet},
title = {A Computationally Sound Mechanized Prover for Security Protocols},
howpublished = {Cryptology {ePrint} Archive, Paper 2005/401},
year = {2005},
url = {https://eprint.iacr.org/2005/401}
}