Paper 2005/401

A Computationally Sound Mechanized Prover for Security Protocols

Bruno Blanchet


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.

Note: The revision includes extensions to handle more cryptographic primitives, improvements in the simplification of games, and a few minor updates and bug fixes.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. A short version of this paper appears at IEEE Symposium on Security and Privacy, Oakland, 2006. This is the full version.
Contact author(s)
blanchet @ di ens fr
2012-06-16: last of 4 revisions
2005-11-14: received
See all versions
Short URL
Creative Commons Attribution


      author = {Bruno Blanchet},
      title = {A Computationally Sound Mechanized Prover for Security Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2005/401},
      year = {2005},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.