This is the live page of David Baelde's part of the MPRI 230 course, for year 20192020.
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 selfcontained 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 (legacy notes, chapter 3, exercises p. 42; slides)
 Proverif: translation, resolution (slides, exercises)
 Equivalences: semantics, brief look at verification techniques (slides)
 Computational security
 ComonBana logic
Final examination
Try the 201718 or 201819 exam as an exercise.