Formal analysis of real-world security protocols

Aleksi Peltonen, Cas Cremers

News

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 (tentative)
- Project deadline: TBA
 
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.