ETH Zuerich - Homepage
Information Security

Formal Methods for Information Security

Master in Information Security

For more information about the Information Security Master Track visit:

263-4600-00L (2V + 1U) Autumn Semester 2009


Lecturers and Tutors: Sebastian Mödersheim and Christoph Sprenger

Lectures: Monday 16-18, IFW B42
Exercises: Tuesday 15-16, IFW B42
Credit: 4 ETCS
Homework: optional, but strongly recommened
Exams: oral exam (session examination)
Language: English



The lecture treats formal and cryptographic methods for the modelling and analysis of security-critical systems. The first and main part of the lecture will concentrate on cryptographic protocols. Cryptographic protocols such as SSL/TLS, SSH, Kerberos and IPSec, form the basis for secure communication and business processes. Numerous attacks on published protocols, such as public-key Kerberos, show that the design of these protocols is extremely error-prone. A rigorous analysis of these protocols is therefore indispensable. Besides an overview of existing analysis methods and tools the lecture will convey the theoretical basis and functioning of some selected methods and tools. The tutorials offer the possibility of applying some tools on concrete protocols. The second part of the lecture will be concerned with formal methods in other parts of information security such as access control.

Course Material

The slides of the lecture and the exercise sheets are available on the course material page.


The lecture is based mainly on various journal/conference papers, but see also:


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 13 October 2009