BlanchetSAS02
Bruno Blanchet
Back to publications
Bruno Blanchet.
From Secrecy to Authenticity in Security
Protocols.
In Manuel Hermenegildo and Germán Puebla, editors, 9th
International Static Analysis Symposium
(SAS'02), volume 2477 of
Lecture Notes in Computer Science, pages 342-359, Madrid, Spain, September
2002. Springer.
Copyright
© Springer-Verlag.
Get the paper
.ps.gz, 91 Kb
Links
LNCS series home page. LNCS Volume 2477 at Springer.
Slides of the talk.
Abstract
We present a new technique for verifying authenticity in cryptographic
protocols. This technique is fully automatic, it can handle an
unbounded number of sessions of the protocol, and it is efficient in
practice.
It significantly extends a previous technique for the verification
of secrecy.
The protocol is represented in an extension of the pi calculus with
fairly arbitrary cryptographic primitives. This protocol
representation includes the authentication specification to be
verified, but no other annotation. Our technique has
been proved correct, implemented, and tested on various
protocols from the literature. The experimental results show that
we can verify these protocols in less than 1 s.
Bibtex
@INPROCEEDINGS{BlanchetSAS02,
AUTHOR = {Bruno Blanchet},
TITLE = {From {S}ecrecy to {A}uthenticity in {S}ecurity {P}rotocols},
BOOKTITLE = {9th International Static Analysis Symposium (SAS'02)},
PAGES = {342--359},
YEAR = 2002,
EDITOR = {Manuel Hermenegildo and Germ{\'a}n Puebla},
VOLUME = 2477,
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Madrid, Spain},
MONTH = SEP,
PUBLISHER = {Springer}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)