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 protocols.
Syllabus
- Discussion of several simple protocols and the typical attacks against them.
- 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 and tools.
- Discussion of (un)decidability and complexity results of security problems.
- Application of the BAN logic of belief to protocol analysis.
Reading
TBA in the course.