The course is taught in F2A: Mondays at 13.00 – 17.00; it starts January 29th 2024.
Location: building 308 auditorium 12 for the lecture; and afterwards exercises in databars 308-017,101,117,127.
Overview:
The course covers two main topics:
1. Security Protocols: This part is about formally defining security protocols, their goals, and an intruder. We then look at automated techniques for analysing security protocols. In a final part of the course we look at privacy and a large case study.
2. Information Flow: This part covers techniques to describe policies of who-should-have-access-to-what (access control) and who-may-learn-what (information flow) and goes into techniques for ensuring that the information flow policies are enforced. We will conclude this track with a more advanced look at relating cryptography and formal verification.
Slides and additional materials will be made available on DTU Learn
Track 1: Security Protocols
|
Date |
Topic |
|
|
Jan 29 |
Modeling Protocols: Alice & Bob & Dolev & Yao |
|
|
Feb 5 |
Symbolic Analysis: The Lazy Intruder Announcement of
mandatory assignment 1. |
|
|
Feb 12 |
Secure Implementation and Typing |
|
|
Feb 19 |
Channels and Protocol Composition |
|
|
Feb 26 |
Modeling Privacy Properties |
|
|
Mar 4 |
Abstract Interpretation |
|
|
Mar 11 |
Hand-in of mandatory
assignment 1 at noon Student presentations Verifying Protocols in Isabelle/HOL |
|
Track 2: Access Control and Information Flow
|
Date |
Topic |
|
|
Mar 18 |
Introduction Information Flow Analysis 1: Denning's Approach Announcement of mandatory assignment 2 |
|
|
Mar 25 |
Easter Holidays |
|
|
Apr 8 |
Information Flow Analysis 2: Volpano's Approach |
|
|
Apr 15 |
Information Flow Analysis 3: Myers' Approach |
|
|
Apr 22 |
Security Conditions and Side-Channels |
|
|
Apr 29 |
Verifying Cryptography in Isabelle/HOL: Zero Knowledge and all that |
|
|
May 6 |
Hand-in of mandatory assignment 2 at noon. Student Presentations Conclusion and Outlook |
|
Mandatory assignments: Students must write two reports about the projects
described above. It is encouraged to work in
groups, but maximum 3 persons per group.
Each report must indicate which students are part of the group,
and which group member is responsible for which
sections. Moreover, it must indicate which resources have been
used to perform the work. This includes text books, research papers,
information found on the web, detailed suggestions from teachers, and results
of discussions or cooperation with other students.
The first project must be
handed in by March 11 at 12.00.
The second project must be
handed in by May 6 at 12.00.
Lecturer: Sebastian Mödersheim
| email
Textbooks/Course materials:
Several papers will be used
in the course; no book is required; material will become available on
DTU Learn/DTU
Inside.