Mini course on formal techniques for security protocols

Here you may find some material relative to the VMCAI 2019 summer school.

Security protocols aims at securing communications over untrusted networks such as Internet. Their design is notoriously error-prone, with flaws discovered years later. Formal methods have been successful in reasoning about the security of protocols and detect attacks. Automatic tools have been designed and applied to many protocols, from academic ones to deployed protocols such as SSL or Kerberos. In these lectures, we explain how security protocols can be modeled in symbolic models such as Horn clauses (a fragment of first-order logic) or applied-pi calculus (a process algebra). We describe and discuss decision techniques to automatically verify properties such as authentication or confidentiality.

Slides of the course

Lab session: During the lab session, you will learn how to use ProVerif to analyse protocols.