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

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-)