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.

 

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.

 

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.

 

The lectures will take place in-person weekly (timeslot TBA), starting the week of 20.10.2025.

Location: TBA

 

- Registration deadline: TBA
- Lectures start: week of 20.10.2025
- Mid-term exam: TBA
- Project start: TBA
- Project deadline: TBA

 

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.

 

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.