02244 Logic for Security (Spring 2023)

The course is taught in F2A: Mondays at 13.00 – 17.00; it starts January 30st 2023.

Location: building 116 auditorium 082 for the lecture; and afterwards exercises in the rooms 010, 042, 044 in the same building.

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 (not part of the exam).

Slides and additional materials will be made available on DTU Learn

Track 1: Security Protocols



 Jan 30

 Modeling Protocols: Alice & Bob & Dolev & Yao

 Feb 6

 Symbolic Analysis: The Lazy Intruder

 Announcement of mandatory assignment 1.

 Feb 13

 Secure Implementation and Typing

 Feb 20

 Channels and Protocol Composition

 Feb 27

 Modeling Privacy Properties

 Mar 6

 Abstract Interpretation

 Mar 13

 Hand-in of mandatory assignment 1 at noon

 Student presentations

 Verifying Protocols in Isabelle/HOL

Track 2: Access Control and Information Flow



 Mar 20


 Information Flow Analysis 1: Denning's Approach

 Announcement of mandatory assignment 2

 Mar 27

 Information Flow Analysis 2: Volpano's Approach

 Apr 3
 Apr 10

 Easter Holidays

 Apr 17

 Information Flow Analysis 3: Meyer's Approach

 Apr 24

 Security Conditions and Side-Channels

 May 1

 Verifying Cryptography in Isabelle/HOL: Zero Knowledge and all that 

 May 8

 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 13 at 12.00.

The second project must be handed in by May 8 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.