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

Date	Topic
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

Date	Topic
Mar 20	Introduction  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.