BlanchetOakland06
Bruno Blanchet
Back to publications
Bruno Blanchet.
A Computationally Sound Mechanized Prover for Security
Protocols.
In IEEE Symposium on Security and Privacy, pages 140-154,
Oakland, California, May 2006.
Get the paper
.ps.gz, 162 Kb, .pdf, 261 Kb
Links
Extended version available as ePrint Report 2005/401, http://eprint.iacr.org/2005/401
Slides of the talk.
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
@INPROCEEDINGS{BlanchetOakland06,
AUTHOR = {Bruno Blanchet},
TITLE = {A Computationally Sound Mechanized Prover for Security Protocols},
BOOKTITLE = {IEEE Symposium on Security and Privacy},
PAGES = {140-154},
YEAR = 2006,
ADDRESS = {Oakland, California},
MONTH = MAY
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)