Formal analysis of real-world security protocols

Aleksi Peltonen, Cas Cremers

News

Exercise Sheet 6

Written on 16.12.24 by Alexander Dax

Dear Students,

we have released the sixth and final exercise sheet today. You can find it under the Materials.
The exercise sheet must be submitted as a team by January 6th at 14:00.

To successfully complete the exercise sheet, you will need to have Tamarin installed.
Remember that there… Read more

Dear Students,

we have released the sixth and final exercise sheet today. You can find it under the Materials.
The exercise sheet must be submitted as a team by January 6th at 14:00.

To successfully complete the exercise sheet, you will need to have Tamarin installed.
Remember that there will be limited support over the holidays, so make sure to check
the exercises early and potentially ask questions already this week in the forum.


Please be reminded that submissions must be made in teams of no more than 2 members
-- sharing or copying solutions from others is strictly prohibited.

Exercise Sheet 5 and Office Hour

Written on 09.12.24 by Alexander Dax

Dear Students,

we have released the fifth exercise sheet today. You can find it under the Materials.

To successfully complete the exercise sheet, you will need to have Tamarin installed.
To assist with any installation challenges, we will hold an Office Hour on Friday, 13th December,
from… Read more

Dear Students,

we have released the fifth exercise sheet today. You can find it under the Materials.

To successfully complete the exercise sheet, you will need to have Tamarin installed.
To assist with any installation challenges, we will hold an Office Hour on Friday, 13th December,
from 13:00 to 15:00 in E9.1, Room 0.07. Feel free to drop by if you need help!
 

The exercise sheet must be submitted as a team by December 16th at 14:00. If you have any questions, don’t hesitate to ask in the forum.
Please be reminded that submissions must be made in teams of no more than 2 members -- sharing or copying solutions from others is strictly prohibited.

Midterm Exam Inspection and Re-Exam Information

Written on 04.12.24 by Alexander Dax

 

Dear all,

As you may have noticed, the final results of the midterm have been published
on your personal page. If you would like to review your exam, we will hold the
midterm exam inspection next week. Additionally, the re-exam will be offered
in early January. Please find the details for… Read more

 

Dear all,

As you may have noticed, the final results of the midterm have been published
on your personal page. If you would like to review your exam, we will hold the
midterm exam inspection next week. Additionally, the re-exam will be offered
in early January. Please find the details for both events below.
 

Midterm Exam Inspection

  • Date: Friday, December 13
  • Time: 9:00 - 11:00
  • Location: E9.1, Room 0.07

To inspect your exam, please make sure to bring your student ID.
 

Re-Exam Information

  • Date: Friday, January 10
  • Time: 16:00 - 18:00
  • Location: E9.1, Lecture Hall

Registration for the re-exam is now open.

Midterm Exam Reminder

Written on 27.11.24 by Alexander Dax

Dear students,

this is a reminder that the midterm exam is happening on Monday, 02.12! Here’s what you need to know:
 

Time and Place:

- The Exam will take place in the E9.1 Lecture Hall.
- Arrive before 14:00; the exam starts promptly at 14:15.

What to Bring:

- A permanent pen (no… Read more

Dear students,

this is a reminder that the midterm exam is happening on Monday, 02.12! Here’s what you need to know:
 

Time and Place:

- The Exam will take place in the E9.1 Lecture Hall.
- Arrive before 14:00; the exam starts promptly at 14:15.

What to Bring:

- A permanent pen (no pencils or erasable ink).  
- Your student ID.

Important Rules: 

- The exam is closed-book (no notes, textbooks, or other materials). 
- Attendance is mandatory to qualify for the re-exam.  

Extra Notes: 

- Anyone who attends the midterm may retake it to try for a better grade.  
- Passing the midterm is required to receive a final course grade.  
 

If you have any questions, feel free to reach out. Good luck, and see you on Monday!

Midterm - Office Hours

Written on 18.11.24 by Alexander Dax

Dear Students,

We will be offering an office hour on Tuesday, November 26th, from 12:30 to 17:30 in the E9.1 lecture hall. This is not a full session where everyone is expected to attend the entire time. Instead, you are welcome to stop by at any point during the time slot to ask questions about… Read more

Dear Students,

We will be offering an office hour on Tuesday, November 26th, from 12:30 to 17:30 in the E9.1 lecture hall. This is not a full session where everyone is expected to attend the entire time. Instead, you are welcome to stop by at any point during the time slot to ask questions about the exercise sheets or topics related to the midterm.

Feel free to drop by if you need assistance or clarification. If you have any additional questions, don’t hesitate to ask in the forum.

Looking forward to seeing you there!

Exercise Sheet 4

Written on 18.11.24 by Alexander Dax

Dear Students,

we have released the fourth exercise sheet today. You can find it under the Materials.

The exercise sheet must be submitted as a team by November 25th at 14:00. If you have any questions, don’t hesitate to ask in the forum.
Please be reminded that submissions must be made in… Read more

Dear Students,

we have released the fourth exercise sheet today. You can find it under the Materials.

The exercise sheet must be submitted as a team by November 25th at 14:00. If you have any questions, don’t hesitate to ask in the forum.
Please be reminded that submissions must be made in teams of no more than 2 members -- sharing or copying solutions from others is strictly prohibited.

Important Announcements

Written on 13.11.24 (last change on 13.11.24) by Alexander Dax

Midterm Registration
 
Midterm registration is now open! You can sign up on your personal CMS page until November 25, 2024, 14:00. Remember, passing the midterm is required to participate in the final project, and re-exam eligibility depends on completing the main midterm. No LSF registration is… Read more
Midterm Registration
 
Midterm registration is now open! You can sign up on your personal CMS page until November 25, 2024, 14:00. Remember, passing the midterm is required to participate in the final project, and re-exam eligibility depends on completing the main midterm. No LSF registration is required for the midterm.
 
Plagiarism Reminder
 
We have observed cases of shared or copied solutions in Exercise Sheets 1 and 2, resulting in 0 points for all involved. Moving forward, confirmed cases of plagiarism will lead to exclusion from the course. Additionally, we’ll be using plagiarism detection software, starting with the Tamarin exercises and final project.
 
Use of ChatGPT
 
While tools like ChatGPT and other internet resources can be helpful for studying, we strongly discourage copying answers directly. In specialized areas like ours, ChatGPT’s responses are often inaccurate, which can lead to wrong answers for you and additional work for us. Please use online resources thoughtfully, and focus on understanding the concepts rather than relying on generated answers.
 
Unification Cheat Sheet
 
We understand that some students found the unification exercise on Sheet 2 challenging. To support your midterm preparation, we are providing a unification cheat sheet to clarify key concepts. You can find it on the Materials page. We hope this resource helps!

Updated Exercise Sheet 3

Written on 12.11.24 by Alexander Dax

Dear all,

we have just updated Exercise Sheet 3 to fix some bugs and typos. Please make sure to use the latest version for your submission.

If you come across any additional issues on this or future exercise sheets, don’t hesitate to reach out to us by email or post in the forum.

Exercise Sheet 3

Written on 11.11.24 by Alexander Dax

Dear Students,

we have released the third exercise sheet today. You can find it under the Materials.

Since the topic on lemmas were only briefly covered in today’s lecture, the exercises on lemmas are optional for bonus points.
If you’d like to complete them, refer to the full slide set or… Read more

Dear Students,

we have released the third exercise sheet today. You can find it under the Materials.

Since the topic on lemmas were only briefly covered in today’s lecture, the exercises on lemmas are optional for bonus points.
If you’d like to complete them, refer to the full slide set or Chapter 6 in the book.

The exercise sheet must be submitted as a team by November 11th at 14:00. If you have any questions, don’t hesitate to ask in the forum.
Please be reminded that submissions must be made in teams of no more than 2 members -- sharing or copying solutions from others is strictly prohibited.

Exercise Sheet 2

Written on 04.11.24 by Alexander Dax

Dear Students,

we have released the second exercise sheet today. You can find it under the Materials.

The exercise sheet must be submitted as a team by November 11th at 14:00. If you have any questions, don’t hesitate to ask in the forum.
Please be reminded that submissions must be made in… Read more

Dear Students,

we have released the second exercise sheet today. You can find it under the Materials.

The exercise sheet must be submitted as a team by November 11th at 14:00. If you have any questions, don’t hesitate to ask in the forum.
Please be reminded that submissions must be made in teams of no more than 2 members -- sharing or copying solutions from others is strictly prohibited.

Exercise Sheet 1

Written on 28.10.24 by Alexander Dax

Dear Students,

we have released the first exercise sheet today. You can find it under the Materials.

The exercise sheet must be submitted as a team by November 4th at 14:00. If you have any questions, don’t hesitate to ask in the forum.
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.

 

Plagiarism

We have observed cases of shared or copied solutions in Exercise Sheets 1 and 2, resulting in 0 points for all involved. Moving forward, confirmed cases of plagiarism will lead to exclusion from the course. Additionally, we’ll be using plagiarism detection software, starting with the Tamarin exercises and final project.
 

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.
 
Time and location
The lectures will take place in-person every Monday from 14.00 (c.t.) - 16.00, starting 21.10.2024.
Location: E9 1 (CISPA), room 0.05 (lecture hall ground floor).
 
Important dates
- Registration deadline: 03.11.2024 - 23:59h
- Lectures start: 21.10.2024
- Mid-term exam: 02.12.2024
- Project start: 06.01.2025
- Project deadline: 28.02.2025
 
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.
Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.