(... to be written)


An excellent introduction to the Pi Calculus is [P01], and the wiki page on the pi calculus[PiWiki] is worth visiting too.

The Pi Calculus has been introduced by Milner et al[MPW90]. An improved version of it optimized for cryptographic protocols, the Spi Calculus, has been proposed by Abadi and Gordon[AG99]. An interesting presentation of the pi calculus is in [ABF18]. The reason we care about the pi calculus is[B16], i.e. its use in ProVerif (and other verification tools).

A talk by Luke Ong, on the "Security Analysis of the Pi Protocol":


  • [MPW90] Robin Milner, Joachim Parrow, David Walker: A Calculus of Mobile Processes, June 1989 (Revised September 1990): part 1, part 2.
  • [AG99] Martín Abadi, Andrew D. Gordon: A Calculus for Cryptographic Protocols: The Spi Calculus. In: Information and Computation, Vol. 148, pages 1-70. (1999). full pdf.
  • [AB05] Martín Abadi and Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102-146, January 2005. (acm.org pdf available, full pdf)
  • [B16] Bruno Blanchet: Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. In: Foundations and Trends in Privacy and Security, Volume 1 Issue 1-2, 31 10 2016, pages 1-135 (paywalled version, full pdf)
  • [ABF18] Martín Abadi, Bruno Blanchet, Cédric Fournet: The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. In: Journal of the ACM, Volume 65 Issue 1, January 2018, Article No. 1. (acm.org pdf available, older pdf at arxiv.org)
  • [P01] Joachim Parrow: An Introduction to the Pi-Calculus. In: Handbook of Process Algebra, ed. Bergstra, Ponse and Smolka. 2001. (elsevier paywalled, full pdf)
  • [B13] Bruno Blanchet: Automatic Verification of Cryptographic Protocols in the Symbolic Model, Automatic Verifier ProVerif. September 2013. (slides pdf)
  • [B15] Bruno Blanchet: The Applied Pi Calculus... with Proofs. April 2015. (slides pdf)
  • [PiWiki] The Pi-Calculus on Wikipedia