BlanchetFOSAD14
Bruno Blanchet
Back to publications
Bruno Blanchet.
Automatic Verification of Security Protocols in the
Symbolic Model: the Verifier ProVerif.
In Alessandro Aldini, Javier Lopez, and Fabio Martinelli, editors,
Foundations of Security Analysis and Design VII, FOSAD Tutorial
Lectures, volume 8604 of Lecture Notes in Computer Science, pages
54-87. Springer, 2014.
Copyright
© Springer-Verlag.
Get the paper
.pdf, 316 Kb
Links
LNCS series home page.
This paper at Springer http://link.springer.com/chapter/10.1007/978-3-319-10082-1_3.
Abstract
After giving general context on the verification of security
protocols, we focus on the automatic symbolic protocol verifier
ProVerif. This verifier can prove secrecy, authentication, and
observational equivalence properties of security protocols, for an
unbounded number of sessions of the protocol. It supports a wide range
of cryptographic primitives defined by rewrite rules or by equations.
The tool takes as input a description of the protocol to verify in a
process calculus, an extension of the pi calculus with
cryptography. It automatically translates this protocol into an abstract
representation of the protocol by Horn clauses, and determines whether
the desired security properties hold by resolution on these clauses.
Bibtex
@INCOLLECTION{BlanchetFOSAD14,
AUTHOR = {Bruno Blanchet},
TITLE = {Automatic Verification of Security Protocols in the Symbolic Model: the Verifier {P}ro{V}erif},
BOOKTITLE = {Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures},
PAGES = {54--87},
PUBLISHER = {Springer},
YEAR = 2014,
EDITOR = {Alessandro Aldini and Javier Lopez and Fabio Martinelli},
VOLUME = 8604,
SERIES = {Lecture Notes in Computer Science}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)