Formal Proofs of Security Protocols

MPRI M2, 2019-2020

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

  1. General introduction to security protocols and formal methods
  2. Symbolic model, internal reduction semantics, secrecy
  3. 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)
  4. Deduction, symbolic semantics
  5. Deducibility constraints (legacy notes, chapter 3, exercises p. 42; slides)
  6. Proverif: translation, resolution (slides, exercises)
  7. Equivalences: semantics, brief look at verification techniques (slides)
  8. Computational security
  9. Comon-Bana logic

Final examination

Try the 2017-18 or 2018-19 exam as an exercise.