Cryptology ePrint Archive: Report 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.
Category / Keywords: cryptographic protocols /
Publication Info: A short version of this paper appears at IEEE Symposium on Security and Privacy, Oakland, 2006. This is the full version.
Date: received 7 Nov 2005, last revised 16 Jun 2012
Contact author: blanchet at di ens fr
Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation
Note: The revision includes extensions to handle more cryptographic primitives, improvements in the simplification of games, and a few minor updates and bug fixes.
Version: 20120616:095147 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]