Formal analysis of real-world security protocols

Cas Cremers

News

Reminder: Midterm Inspection & LSF Registration

Written on 17.12.25 by Erik Pallas

Dear students,

this is a reminder for the midterm inspection happening today from 15:00 through 16:00 in E9 1, 0.07; see our message from Monday for more details.
Please also keep in mind that you have to register for this lecture in LSF by 05.01.2026 if you want to receive a grade at the end of this course.

Lecture 4: Slides & Exercise Sheet

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

Dear students,

we just released the slides of yesterday's lecture; please excuse the delay. The fourth exercise sheet has already been published yesterday.

Midterm: Results & Inspection

Written on 15.12.25 by Erik Pallas

Dear students,

we just released the results of the midterm; you can find your grade and the number of points you scored in the CMS.

We will offer an exam inspection this Wednesday, 17.12.2025, from 15:00 through 16:00 at E9 1, 0.07. Please bring a valid photo ID, otherwise we cannot hand out… Read more

Dear students,

we just released the results of the midterm; you can find your grade and the number of points you scored in the CMS.

We will offer an exam inspection this Wednesday, 17.12.2025, from 15:00 through 16:00 at E9 1, 0.07. Please bring a valid photo ID, otherwise we cannot hand out your exam. If you cannot make it yourself, you can send someone else to inspect your midterm on your behalf; in this case, you need to provide them with a signed letter of authorization (find a sample letter below). They also need to bring their photo ID (but not yours).

Please remember that aside from passing the midterm and the final project, you also need 50% of the points on the exercise sheets to pass this course.

Sample Letter of Authorization:

I, NAME OF STUDENT, born on DATE OF BIRTH, hereby grant NAME OF REPRESENTATIVE, born on DATE OF BIRTH, the right to inspect my midterm exam, taken on 08.12.2025 in the lecture Formal Analysis of Real-World Security Protocols at Saarland University. [He/She/They may also produce scans or photographies of my exam in order to forward them to me.]

NAME OF STUDENT, DATE, LOCATION
SIGNATURE

Announcement: Course Evaluation

Written on 15.12.25 by Erik Pallas

Dear students,

currently, course evaluations are taking place at Saarland University; if you have not done so already, please share your feedback on this lecture here. This will help us improve the next iterations of the course. Thanks a lot!

Midterm: Reminder & Recap Slides

Written on 01.12.25 by Erik Pallas

Dear Students,

please remember the midterm exam next week! Here is a summary of the key facts:

Time and Place

  • 08.12.2025, 14:00; exam starts at 14:15 sharp!
  • 90min duration
  • E9 1, 0.05

What to Bring

  • a permanent pen (no pencils or erasable ink)
  • your student ID with picture,… Read more

Dear Students,

please remember the midterm exam next week! Here is a summary of the key facts:

Time and Place

  • 08.12.2025, 14:00; exam starts at 14:15 sharp!
  • 90min duration
  • E9 1, 0.05

What to Bring

  • a permanent pen (no pencils or erasable ink)
  • your student ID with picture, or additional photo ID

Rules

  • closed-book (no notes, textbooks, etc.)
  • Passing the midterm is required to pass the course

    
We also uploaded the slides of the lecture recap; please have a look, but remember that this is just a summary and does not cover the lecture contents in sufficient detail for the midterm.

If you have any question, please use the forum or reach out to us at farwsp@cispa.de. Best of luck, and see you next Monday!

Exercise Sheet 3: Results Available

Written on 28.11.25 by Erik Pallas

Dear students,

we just released the scores for the third exercise sheet. You can inspect your corrected submissions during Monday's office hour; we will also give a brief recap on the midterm contents.

Announcement: Update on Lecture Plan

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

Dear students,

a brief update on the lecture plan for the remainder of the semester:

  • Next Monday, 01.12.2025, instead of a lecture we offer an Office Hour (usual time and place); we will give a brief recap about the topics covered so far and will answer your questions about the exercise… Read more

Dear students,

a brief update on the lecture plan for the remainder of the semester:

  • Next Monday, 01.12.2025, instead of a lecture we offer an Office Hour (usual time and place); we will give a brief recap about the topics covered so far and will answer your questions about the exercise sheets and lecture contents.
  • On Monday, 08.12.2025, we have the midterm; it will cover contents from lectures 0 through 3. Don't forget to register for the midterm in the CMS!
  • The week after that, 15.12.2025, we proceed with lecture 4 and will publish exercise sheet #4, which is due on 05.01.2026.
  • The project will start as planned on 12.01.2026 and has to be submitted by 06.03.2026.

Announcement: Cancellation of today's lecture

Written on 24.11.25 by Erik Pallas

Dear students,

unfortunately, we have to cancel today's lecture. We will let you know how this impacts the lecture plan and the contents of the midterm as soon as we know more.
This also means that there will be no new exercise sheet released today. The deadline for exercise sheet #3 remains… Read more

Dear students,

unfortunately, we have to cancel today's lecture. We will let you know how this impacts the lecture plan and the contents of the midterm as soon as we know more.
This also means that there will be no new exercise sheet released today. The deadline for exercise sheet #3 remains today, 2pm.
We will still provide feedback on and answer questions about exercise sheet #2 starting today at 2pm in E9 1, 0.05. Alternatively, you can also have a look at your submission during next week's office hour.

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.