International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Paper: A Computationally Sound Mechanized Prover for Security Protocols

Authors:
Bruno Blanchet
Download:
URL: http://eprint.iacr.org/2005/401
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2005-12735,
  title={A Computationally Sound Mechanized Prover for Security Protocols},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols /},
  url={http://eprint.iacr.org/2005/401},
  note={A short version of this paper appears at IEEE Symposium on Security and Privacy, Oakland, 2006. This is the full version. blanchet@di.ens.fr 13546 received 7 Nov 2005, last revised 2 Feb 2007},
  author={Bruno Blanchet},
  year=2005
}