Formal Analysis of Cryptographic Protocols
8 lectures given by Sibylle Fröschle
Starting: Thursday, 15 February 2007
To: 5 April 2007 inclusive
Venue: JCMB, Room 2509
Although cryptographic protocols are typically only a few lines long their
design is highly error-prone: as coined by Ross Anderson and Roger Needham
protocol design amounts to "Programming Satan's Computer". In this course
we will study key approaches to the formal analysis and verification of
cryptographic protocols. Throughout we will assume perfect cryptography,
and thus only concentrate on the correctness of the logic of the
Discussion of several simple protocols and the typical attacks
Introduction of the main models used to formally present
protocols, e.g., strand spaces and multiset rewriting.
Survey of the most significant automated reasoning techniques
Discussion of (un)decidability and complexity results of security problems.
Application of the BAN logic of belief to protocol analysis.
TBA in the course.