A Calculus for
Cryptographic Protocols
Andy Gordon, Microsoft Research
Theory
Mini-Course, Michaelmas 2001
This course takes a programming language approach to solving problems in the analysis of cryptographic protocols. Our method is based on specifying a protocol as a program coded up in the spi calculus of Abadi and Gordon. Spi is a small concurrent language with primitives for cryptography. Protocol properties such as authenticity and secrecy are expressed in terms of equations and events. We check properties of our code by borrowing techniques from programming language theory such as bisimulations and type systems. These techniques have led to the independent rediscovery of flaws in existing protocols and helped verify the design of new and improved protocols. As well as reviewing established work on spi, the course covers ongoing work on type-checking protocols, and highlights opportunities for further research.
Much of the content of the course draws on joint work with Martín Abadi and with Alan Jeffrey.
Monday November 12,
Wednesday November 14,
Prerequisites: some exposure to the formal semantics of programming languages.
Materials: course notes and slides.
Background reading:
M. Abadi and A.D. Gordon A calculus for cryptographic protocols: the spi calculus.
Information and Computation 148:1-70 (1999).
An extended version
appears as Research Report 149,
M. Abadi Secrecy by typing in
security protocols
Journal of the ACM 46(5): 749-786 (1999).
A.D. Gordon and A. Jeffrey Authenticity
by typing for security protocols
14th IEEE Computer Security Foundations Workshop (CSFW 2001), 145-159 (2001).