BlanchetFnTPS16
Bruno Blanchet
Back to publications
Bruno Blanchet.
Modeling and Verifying Security Protocols with the Applied
Pi Calculus and ProVerif.
Foundations and Trends in Privacy and Security, 1(1-2):1-135,
October 2016.
Get the paper
.pdf, 1103 Kb
Links
Foundations and Trends in Privacy and Security
The paper is available here: http://dx.doi.org/10.1561/3300000004 (can be ordered as a book).
Abstract
ProVerif is an automatic symbolic protocol verifier. It supports a
wide range of cryptographic primitives, defined by rewrite rules or
by equations. It can prove various security properties: secrecy,
authentication, and process equivalences,
for an unbounded message space and an unbounded number of sessions.
It takes as input a description of the protocol to verify in a
dialect of the applied pi calculus, an extension of the pi calculus
with cryptography. It automatically translates this protocol description
into Horn clauses and determines whether
the desired security properties hold by resolution on these clauses.
This survey presents an overview of the research on
ProVerif.
Bibtex
@ARTICLE{BlanchetFnTPS16,
AUTHOR = {Bruno Blanchet},
TITLE = {Modeling and Verifying Security Protocols with
the Applied Pi Calculus and {P}ro{V}erif},
JOURNAL = {Foundations and Trends in Privacy and Security},
YEAR = {2016},
VOLUME = {1},
NUMBER = {1--2},
PAGES = {1--135},
MONTH = OCT
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)