AbadiBlanchetFournetESOP2004
Bruno Blanchet
Back to publications
Martín Abadi, Bruno Blanchet, and Cédric Fournet.
Just Fast Keying in the Pi Calculus.
In David Schmidt, editor, Programming Languages and Systems:
Proceedings of the 13th European Symposium on Programming (ESOP'04),
volume 2986 of Lecture Notes in Computer Science, pages 340-354,
Barcelona, Spain, March 2004. Springer.
Copyright
© Springer-Verlag.
Get the paper
.ps.gz, 68 Kb, .pdf, 166 Kb
Links
LNCS series home page. LNCS Volume 2986 at Springer.
Software, scripts, and long version
Abstract
JFK is a recent, attractive protocol for fast key establishment as
part of securing IP communication. In this paper, we analyze it
formally in the applied pi calculus (partly in terms of
observational equivalences, partly with the assistance of an
automatic protocol verifier). We treat JFK's core security
properties, and also other properties that are rarely articulated
and studied rigorously, such as resistance to denial-of-service attacks.
In the course of this analysis we found some ambiguities and minor
problems, but we mostly obtain positive results about JFK. For this
purpose, we develop ideas and techniques that should be useful more
generally in the specification and verification of security
protocols.
Bibtex
@INPROCEEDINGS{AbadiBlanchetFournetESOP2004,
AUTHOR = {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'e}dric Fournet},
TITLE = {Just {F}ast {K}eying in the {P}i {C}alculus},
BOOKTITLE = {Programming Languages and Systems: Proceedings of the
13th European Symposium on Programming ({ESOP}'04)},
PAGES = {340--354},
YEAR = 2004,
EDITOR = {David Schmidt},
VOLUME = 2986,
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Barcelona, Spain},
MONTH = MAR,
PUBLISHER = {Springer}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)