This is the live page of David Baelde's part of the MPRI 2-30 course, for year 2019-2020.
All sessions take place in room 1014 of the Sophie Germain building.
Lecture notes
Here are my lecture notes for this course.
These notes mostly aim at providing a self-contained account of the semantical aspects of the course, and detailing a few points that are not covered in legacy lecture notes. For some of the course's content, the reference will still be these legacy notes.
Agenda & teaching material
- General introduction to security protocols and formal methods
- Symbolic model, internal reduction semantics, secrecy
-
Labelled transition system + intro to ProVerif
- end of chapter 1 of lecture notes
- slides for ProVerif
- code samples including template for NSPK exercise for next time (see slides for instructions)
-
Deduction, symbolic semantics
- lecture notes, sections 2.1 & 2.2
- exercises: prepare at least first three for next time
- solution for nspk.pv exercise (with protocol fixed)
- code sample for correspondences
-
Deducibility constraints
- Slides
- Proofs for very similar system in legacy notes, chapter 3
- Exercises p. 42 of legacy notes
- Exercise 3, questions 1-2, exam 2018/2019
-
Proverif: translation, resolution (slides,
exercises)
- Exercise 2 in 2017/2018 exam (resolution)
- Exercise 3 in 2017/2018 exam (blind tokens & unlinkability)
- Exercise 3, question 3, 2018/2019 exam (resolution example)
- LAK exercise (model, authentication)
-
Equivalences (slides)
- Exercise 1 in 2017/2018 exam (alternative definitions)
- Exercise 1 in 2018/2019 exam (composition for offline guessing)
- Exercise 2 in 2018/2019 exam (static equiv. counter-examples)
- LAK exercise (unlinkability)
- Computational security: definitions and examples + beginning of Comon-Bana logic (slides)
-
Comon-Bana logic (slides)
- Exercise 2 in 2018/2019 exam
Final examination
Here are the 2017-18, 2018-19 and 2019-20 exams (updated to correct mistakes).