BlanchetMOD11
Bruno Blanchet
Back to publications
Bruno Blanchet.
Mechanizing Game-Based Proofs of Security Protocols.
In Tobias Nipkow, Olga Grumberg, and Benedikt Hauptmann, editors,
Software Safety and Security - Tools for Analysis and Verification,
volume 33 of NATO Science for Peace and Security Series - D:
Information and Communication Security, pages 1-25. IOS Press, May 2012.
Proceedings of the summer school MOD 2011.
Get the paper
.pdf, 204 Kb
Abstract
After a short introduction to the field of security
protocol verification, we present the automatic
protocol verifier CryptoVerif. In contrast to most
previous protocol verifiers, CryptoVerif does not
rely on the Dolev-Yao model, but on the
computational model. It produces proofs presented as
sequences of games, like those manually done by
cryptographers; these games are formalized in a
probabilistic process calculus. CryptoVerif provides
a generic method for specifying security properties
of the cryptographic primitives. It can prove
secrecy and correspondence properties (including
authentication). It produces proofs valid for any
number of sessions, in the presence of an active
adversary. It also provides an explicit formula for
the probability of success of an attack against the
protocol, as a function of the probability of
breaking each primitive and of the number of
sessions.
Bibtex
@INCOLLECTION{BlanchetMOD11,
AUTHOR = {Bruno Blanchet},
TITLE = {Mechanizing Game-Based Proofs of Security Protocols},
BOOKTITLE = {Software Safety and Security - Tools for Analysis and Verification},
PAGES = {1--25},
PUBLISHER = {IOS Press},
YEAR = 2012,
EDITOR = {Tobias Nipkow and Olga Grumberg and Benedikt Hauptmann},
VOLUME = 33,
SERIES = {NATO Science for Peace and Security Series -- D: Information and Communication Security},
MONTH = MAY,
IBSN = {978-1-61499-027-7},
NOTE = {Proceedings of the summer school MOD 2011}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)