Department of Computer Science and Technology

Technical reports

A calculus for cryptographic protocols
The SPI calculus

Martín Abadi, Andrew D. Gordon

January 1997, 105 pages

DOI: 10.48456/tr-414


We introduce the spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.

Full text

PS (0.3 MB)

BibTeX record

  author =	 {Abadi, Mart{\'\i}n and Gordon, Andrew D.},
  title = 	 {{A calculus for cryptographic protocols : The SPI calculus}},
  year = 	 1997,
  month = 	 jan,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-414},
  number = 	 {UCAM-CL-TR-414}