Security Protocols: Principles and Calculi

Security protocols, as used in distributed systems for authentication and related purposes, are notoriously prone to failures. Therefore, over time, various methods have been developed for the design and analysis of these protocols. This talk introduces principles of protocol design. Taking a more formal approach, it describes calculi for reasoning about protcols, in particular an extension of the pi calculus with function symbols that can represent cryptographic operations. The principles emphasize that protocol messages have meaning; the calculi exploit the idea that programming languages provide a setting and a body of techniques for the study of security.

Professor Abadi is well known for his wide-ranging work on security, programming languages, and specification and verification methods. In particular, he was one of the creators of the influential "BAN logic" for reasoning about authentication in distributed systems, and the spi calculus for describing cryptographic protocols. Prior to joining the University of California at Santa Cruz, he worked at Digital's System Research Center and other industrial research labs.

This is a public lecture, open to all, and will be followed by a reception at 5.30pm in the Talbot Rice Gallery. This is one of a range of events comprising the University of Edinburgh Informatics Jamboree, 22-24 May 2002.

The annual Milner Lecture was founded by a donation from Robin Milner "to keep a live connection between theory and application in computer science".