AbadiBlanchetFournetJACM17

Bruno Blanchet Back to publications
Martín Abadi, Bruno Blanchet, and Cédric Fournet. The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. Journal of the ACM, 65(1):1:1-1:41, October 2017.

Links

Official ACM version (you can download the full text from there):

ACM DL Author-ize serviceThe Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
Martín Abadi, Bruno Blanchet, Cédric Fournet
Journal of the ACM (JACM), 2017

Technical report version

Abstract

We study the interaction of the programming construct ``new'', which generates statically scoped names, with communication via messages on channels. This interaction is crucial in security protocols, which are the main motivating examples for our work, it also appears in other programming-language contexts. We define the applied pi calculus, a simple, general extension of the pi calculus in which values can be formed from names via the application of built-in functions, subject to equations, and be sent as messages. (In contrast, the pure pi calculus lacks built-in functions, its only messages are atomic names.) We develop semantics and proof techniques for this extended language and apply them in reasoning about security protocols. This paper essentially subsumes the conference paper that introduced the applied pi calculus in 2001. It fills gaps, incorporates improvements, and further explains and studies the applied pi calculus. Since 2001, the applied pi calculus has been the basis for much further work, described in many research publications and sometimes embodied in useful software, such as the tool ProVerif, which relies on the applied pi calculus to support the specification and automatic analysis of security protocols. Although this paper does not aim to be a complete review of the subject, it benefits from that further work and provides better foundations for some of it. In particular, the applied pi calculus has evolved through its implementation in ProVerif, and the present definition reflects that evolution.

Bibtex


@ARTICLE{AbadiBlanchetFournetJACM17,
  AUTHOR = {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'e}dric Fournet},
  TITLE = {The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication},
  JOURNAL = {Journal of the ACM},
  YEAR = {2017},
  VOLUME = {65},
  NUMBER = {1},
  MONTH = OCT,
  PAGES = {1:1--1:41},
  ARTICLENO = {1},
  NUMPAGES = {41}
}


E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)