Formal analysis of real-world security protocols

Cas Cremers
Sorry, but the limit for this course is reached (70 students)!
You cannot register for this course anymore.

News

Lecture 0: Slides

Written on 27.10.25 by Erik Pallas

Dear students,

we just uploaded the slides of today's lectures, with some minor additions.
Please note that this week there is no exercise sheet yet; we will release the first one after next week's lecture.

Announcement: Course Time and Dates

Written on 13.10.25 (last change on 13.10.25) by Erik Pallas

Dear students,

our lecture will take place Mondays, 14-16h c.t. in E9 1, room 0.05, starting on October 27th, 2025. Course details and important dates are now available on the CMS main page and will shortly be added to the calendar.

As we have already reached the participant limit, we would also… Read more

Dear students,

our lecture will take place Mondays, 14-16h c.t. in E9 1, room 0.05, starting on October 27th, 2025. Course details and important dates are now available on the CMS main page and will shortly be added to the calendar.

As we have already reached the participant limit, we would also like to ask everybody who is not planning to actively participate in the course to unregister and give other students the opportunity to join this lecture. Thanks a lot for your understanding!

Formal Analysis of Real-World Security Protocols

This is an advanced course in formal analysis of security protocols. The course consists of a theoretical and a practical part. In the theoretical part, you will learn the foundations of protocol verification in the symbolic model. In the practical part, you will use a state-of-the-art cryptographic verification tool, the Tamarin prover, to model and analyze security protocols.
 
The course is taught in English and is suitable for both bachelor and master students with a background in computer science. It is highly recommended to, at the very least, have taken CySec1/CySec2 or Security prior to this course.
 

Course Goals

In this course, you will learn about the symbolic model of cryptography, and how to model protocols within it. You will learn how to read specifications of protocols, and how to translate them into formal models. Finally, you will use the Tamarin prover, a state-of-the-art verification tool, to model and verify security properties of small/medium size protocols.
 

Organization

The course consists of weekly live lectures, exercises, a midterm exam, and a project.
The exercises and the project are made to be solved in teams of two.
Note that the following information is tentative and might change until the start of the lecture.
 
Time and location
The lectures will take place in-person weekly (Monday, 2pm-4pm c.t.), starting on 27.10.2025.
Location: E9 1, 0.05 (CISPA building, lecture hall on ground floor)
 
Important dates
- Lectures start: 27.10.2025
- Midterm registration deadline: 01.12.2025, 23:59h (CMS)
- Mid-term exam: 08.12.2025
- Project start: 12.01.2026
- Project registration deadline: 27.02.2025 (CMS)
- Project deadline: 06.03.2026
 
Communication
All course-relevant information will be shared via announcements in the CMS.
You can contact us under farwsp@cispa.de. If your question might be of interest to other course participants as well (e.g., question about exercise sheets or course contents) please use the forum instead.
 
Passing criteria
To pass the course, a student needs to:
- receive at least 50% of the total exercise points,
- pass the midterm exam, and
- pass the project.
 
Grading
The final grade will depend on the midterm exam and the project:
- Midterm: 30% of the final grade
- Project: 70% of the final grade
 
The grade can be negatively impacted if a student lets their partner do the majority of the project or is not able to answer questions about the solution. Not contributing at all to the project will lead to failing the course. Confirmed cases of plagiarism will lead to exclusion from the course. Additionally, we will be using plagiarism detection software, starting with the Tamarin exercises and final project.
Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.