A Calculus for Cryptographic Protocols

Andy Gordon

Microsoft Research

Description

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.

Prerequisites

Some exposure to the formal semantics of programming languages.

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, Digital Systems Research Center (1998).)

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