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

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