02244 Logic for Security (Spring 2026)

The course is taught in F2A: Mondays at 13.00 – 17.00; it starts February 2nd 2026.

Location: building 308 auditorium 12 for the lecture; and afterwards exercises in rooms 308-001,009,017,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
Feb 2	Modeling Protocols: Alice & Bob
Feb 9	Modeling the Intruder: Dolev & Yao  Announcement of mandatory assignment 1.
Feb 16	Symbolic Analysis: The Lazy Intruder
Feb 23	Secure Implementation and Typing
Mar 2	Channels and Protocol Composition
Mar 9	Modeling Privacy Properties
Mar 16	Hand-in of mandatory assignment 1 at noon  Student presentations  Abstract Interpretation  Verifying Protocols in Isabelle/HOL

Track 2: Access Control and Information Flow

Date	Topic
Mar 23	Introduction  Information Flow Analysis 1: Denning's Approach  Announcement of mandatory assignment 2
Mar 30  Apr 6	Easter Holidays
Apr 13	Information Flow Analysis 2: Volpano's Approach
Apr 20	Information Flow Analysis 3: Myers' Approach
Apr 27	Information Leakage
May 4	Verifying Cryptography in Isabelle/HOL: Zero Knowledge and all that
May 11	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 16 at 12.00 (noon).

The second project must be handed in by May 11 at 12.00 (noon).

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.