Main Page

News

30.08.2022	Final Grades Are Released Dear all, We published the project grades and the final grades in the CMS. They are not yet in the LSF. Due to your detailed documentation, we have decided to forgo the oral exam of your projects. Feel free to contact us via mail if you want to challenge the... Read more Dear all, We published the project grades and the final grades in the CMS. They are not yet in the LSF. Due to your detailed documentation, we have decided to forgo the oral exam of your projects. Feel free to contact us via mail if you want to challenge the grading of your project or have any other questions. Best, Niklas
14.07.2022	Final Project Released! Dear all, We have just released the description of the final project. The project is due Wednesday, 24.08.2022 at 23:59h. Best, Niklas
12.07.2022	No lecture on July 13th; Last lecture on July 20th Dear all, There will be no lecture tomorrow (July 13th). The last lecture will be on July 20th, and will be about many new and exciting open research topics around protocol verification, and Tamarin in general. Hope to see you then! Cas
28.06.2022	Next lectures will be online-only Dear all, The next lectures, starting from tomorrow Wednesday June 29th, will be online-only. Best, Cas
27.06.2022	Updated submission date for Exercise 3 Hi all, we updated the submission date for Exercise sheet 3 to the 6th of July. We apologise for the misunderstanding. Best, Aurora
15.06.2022	Zoom Location for Today's Lecture Hi all, today's lecture will take place in a different Zoom room: https://zoom.us/j/9248268309?pwd=MEd4T0tnSXVCcjFKeDVzUzdUZmZPdz09 Best, Niklas
02.06.2022	Registration for Mid-Term Hi all, we set up a registration for the mid-term. Please register such that we know how many exams we have to print. Cheers, Niklas
01.06.2022	Mid-Term Exam Hi all, next week, we will have our mid-term exam. The mid-term will take place in the CISPA lecture hall during our regular lecture slot. That is Wednesday (08.06.22) from 10:00 to 11:30. The mid-term will take 90 minutes. Make sure to be there by 9:45 such... Read more Hi all, next week, we will have our mid-term exam. The mid-term will take place in the CISPA lecture hall during our regular lecture slot. That is Wednesday (08.06.22) from 10:00 to 11:30. The mid-term will take 90 minutes. Make sure to be there by 9:45 such that we can start on time. Do not forget to bring your student ID and a non-erasable pen for writing. There are no additional materials allowed during the exam. Cheers, Niklas
30.05.2022	First Hybrid Lecture this Wednesday! Hi all, This Wednesday, the 1st of June, we will have our first hybrid lecture! You can physically attend this lecture at the CISPA lecture hall (E9.1., Room 0.05) Looking forward to seeing all of you in person! Cheers, Niklas Note that for the... Read more Hi all, This Wednesday, the 1st of June, we will have our first hybrid lecture! You can physically attend this lecture at the CISPA lecture hall (E9.1., Room 0.05) Looking forward to seeing all of you in person! Cheers, Niklas Note that for the foreseeable future, wearing masks will be mandatory in the CISPA building. Hence, even if UdS does not require masks, they will be required when attending the in-person lecture in the CISPA building.
25.05.2022	Hybrid Classroom Hi all, we've decided to change the format of the lecture to be hybrid (in-person AND via zoom). Starting next week (Wednesday 01.06), the lecture will take place in the CISPA building's lecture hall (room 0.05). We're looking forward to seeing you next week! ... Read more Hi all, we've decided to change the format of the lecture to be hybrid (in-person AND via zoom). Starting next week (Wednesday 01.06), the lecture will take place in the CISPA building's lecture hall (room 0.05). We're looking forward to seeing you next week! Note that for the foreseeable future, wearing masks will be mandatory in the CISPA building. Hence, even if UdS does not require masks, they will be required when attending the in-person lecture in the CISPA building. Cheers, Niklas
06.05.2022	Updated Exercise Sheet 1 Hi all, we revised Exercise Sheet 1. Please check the latest version.
27.04.2022	CMS Updates and Team Groupings Hi all, as announced this morning in the lecture, we did update the CMS and will also clarify the team groupings here: CMS The CMS got some updates today so please check the main page again. The most important changes contain: - There is now a link... Read more Hi all, as announced this morning in the lecture, we did update the CMS and will also clarify the team groupings here: CMS The CMS got some updates today so please check the main page again. The most important changes contain: - There is now a link to the Discord server (which will be used for the office hours) - We reduced the number of total assignments from 5 to 4 - We added information to the timetable (it will be updated again, so check it regularly) - We updated the Material section. Note: we will upload the recordings of the lectures as well in the next few days. Materials and recordings for the upcoming lectures will be uploaded in a timely manner. Team Groupings As already mentioned in the CMS and in the lecture, assignments as well as the final project are made for groups of two people. In the CMS you will find the feature to register or join a group. Please do so until the 17.05.2022 AND before you submit the first assignment that will be released next week. You can use the Forum in the CMS as well as the Discord to look for teammates. If it was not possible to find a teammate until the deadline, please contact us, so we can discuss further steps. Best, Alexander
20.04.2022	Poll: Hybrid Classroom Hi all, we're considering to change the format of the lectures to be hybrid (in-person AND via zoom) instead of having only virtual lectures. To make this decision, we need your input by filling out the following anonymous poll by the end of this week (Sunday... Read more Hi all, we're considering to change the format of the lectures to be hybrid (in-person AND via zoom) instead of having only virtual lectures. To make this decision, we need your input by filling out the following anonymous poll by the end of this week (Sunday 23:59). https://xoyondo.com/ap/NKueGogEkSFcjFy We will provide more updates regarding in-person lectures soon. Note that for the foreseeable future, wearing masks will be mandatory in the CISPA building. Hence, even if UdS does not require masks, they will be required when attending the in-person lecture in the CISPA building.
12.04.2022	Kickoff Lecture on Wednesday, 20.04. at 10:15 am Welcome to the first iteration of the Formal analysis of real-world security protocols lecture! Our first lecture will be on Wednesday, April 20, starting at 10 c.t. over Zoom. For the details of how to access the Zoom call, we will update the main page... Read more Welcome to the first iteration of the Formal analysis of real-world security protocols lecture! Our first lecture will be on Wednesday, April 20, starting at 10 c.t. over Zoom. For the details of how to access the Zoom call, we will update the main page accordingly by next week.

Show all

Formal analysis of real-world security protocols

In this advanced lecture we will study how to analyse and verify real-world security protocols.
This course is separated into two main parts: a theoretical, and a practical.
In the theoretical part, we will learn the foundations of current state-of-the-art protocol verification.
In the practical part, we will teach you how to translate a specification of a protocol into a model,
and how to verify it with the Tamarin Prover.
Finally, you will use the knowledge you have gained to work on a project of your own.

At the very least, having taken CySec1/CySec2 or Security will significantly ease taking 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

We will hold one lecture per week for a total of twelve lectures. The recordings of the lecture will be released
later in the week. In addition, we will offer office hours, every Friday from 09:00-12:00, where you can ask questions.

We will have a mid-term exam that covers the theoretical part of the lecture. You can take an oral re-exam at the end of the course.
Instead of an end-term exam, you will work on a graded practical project where you verify protocols with the Tamarin Prover.

Course Language: English

Registration: closes at the 02.05.! (Once you are registered here, don't forget to register in the LSF as soon as it opens.)
You have to be registered in the LSF by the 17.08.2022 to take the final project and pass the course.

When: Wednesday, 10:00 AM

Where: (all links also appear in the calendar events)

Zoom (Classes): Zoom
Discord (Office Hours): here

Official mid-term exam date : 08.06.2022, 10:00-11:30 (E9.1. Lecture Hall)
Official project start : 13.07.2022 (tentative)
Official project deadline : 24.08.2022 (tentative)

The assignments and the project are made to be solved in teams of 2.
This course can only accommodate up to 30 students. Students will be admitted on a first-come first-served basis.

Assignments and Projects

Bi-Weekly Exercise Sheets (4 in total)

6 week project (in parallel to office hour sessions)

Passing Criteria and Grading

To pass:

midterm: pass
50% in exercise sheets
pass project and oral exam of project

Grading:

midterm: 25%
project & oral exam: 75%
oral exam - present your work and answer questions.

Students can get a better grade if they present the project well.

Grade can go down, if they :

let their partner do the majority of the work
are not able to answer several (minimal) questions about the project.

Students can also fail the project, if we are convinced that they did not contribute in anyway in the project.

Formal analysis of real-world security protocols Cas Cremers