BlanchetTDSC07
Bruno Blanchet
Back to publications
Bruno Blanchet.
A Computationally Sound Mechanized Prover for Security
Protocols.
IEEE Transactions on Dependable and Secure Computing,
5(4):193-207, October-December 2008.
Special issue IEEE Symposium on Security and Privacy 2006. Electronic
version available at
http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005.
Copyright
© IEEE.
Get the paper
.ps.gz, 471 Kb, .pdf, 789 Kb
Abstract
We present a new mechanized prover for secrecy properties of
security 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-key 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
@ARTICLE{BlanchetTDSC07,
AUTHOR = {Bruno Blanchet},
TITLE = {A Computationally Sound Mechanized Prover for Security Protocols},
JOURNAL = {IEEE Transactions on Dependable and Secure Computing},
YEAR = 2008,
VOLUME = 5,
NUMBER = 4,
PAGES = {193--207},
MONTH = OCT # {--} # DEC,
NOTE = {Special issue IEEE Symposium on Security and Privacy 2006. Electronic version available at http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005.}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)