Formal analysis of real-world security protocols Cas Cremers

News

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.

 

Formal analysis of real-world security protocols  Tamarin_logo

 

 

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 (tentative)
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 :

  1. let their partner do the majority of the work
  2. 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.

 

 



Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators