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

Exercise Sheet 2: Results Available

Written on 21.11.25 by Erik Pallas

Dear students,

we just released the scores for the first exercise sheet. If you want to have a look at your corrected submission, you can again do so on Monday: Please pick up your sheet before the lecture and return it by the end of the lecture.

Lecture 3: Slides & Exercise Sheet

Written on 17.11.25 by Erik Pallas

Dear students,

we just released the slides of today's lectures and the third exercise sheet. Please note that this week's sheet again contains a few bonus exercises.

Exercise Sheet 1: Results Available

Written on 12.11.25 by Erik Pallas

Dear students,

we just released the scores for the first exercise sheet. If you want to have a look at your corrected submission, you can do so on Monday: Please pick up your sheet before the lecture and return it by the end of the lecture.
For all future submissions, please make sure to follow… Read more

Dear students,

we just released the scores for the first exercise sheet. If you want to have a look at your corrected submission, you can do so on Monday: Please pick up your sheet before the lecture and return it by the end of the lecture.
For all future submissions, please make sure to follow the instructions at the top of the exercise sheets; we retain the right to deduct points or not consider a submission if these instructions are ignored repeatedly.

Lecture 2: Slides & Exercise Sheet

Written on 10.11.25 by Erik Pallas

Dear students,

we just released the slides of today's lectures, the second exercise sheet and some additional material on unification. Please note that exercise 3 on this week's sheet is a bonus exercise and does not count to the maximum number of points; for more details see the instructions on… Read more

Dear students,

we just released the slides of today's lectures, the second exercise sheet and some additional material on unification. Please note that exercise 3 on this week's sheet is a bonus exercise and does not count to the maximum number of points; for more details see the instructions on the sheet itself.

Lecture 1: Slides & Exercise Sheet

Written on 03.11.25 by Erik Pallas

Dear students,

we just uploaded the slides of today's lectures and the first exercise sheet.
Also note that there will be no lecture on December 1st; instead, we will offer an Office Hour to answer your questions about the lecture and exercise sheet contents.

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!
Show all

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.