Formal modeling and verification of security protocols

Teaching goals

The objective of this course is to provide students with an in-depth knowledge regarding methods and tools for the specification, design, and symbolic verification of security protocols in various domains.

Course description

  • Introduction to cryptography (if necessary): symmetric and asymmetric cryptography, hash functions
  • Formal ways of specifying a protocol: Alice & Bob notation, message sequence charts, Horn clauses, constraint systems, applied pi calculus
  • Attacker models: passive and active attackers, Dolev-Yao adversary, knowledge inference
  • Formal specification of security properties: weak and strong secrecy, indistinguishability property, authentication (aliveness, agreement, synchronization), anonymity
  • Man-in-the-middle attacks
  • Protocol verification with a bounded number of sessions: constraint systems
  • Protocol verification with an unbounded number of sessions: Horn Clauses
  • Symbolic versus computational models for protcol verification
  • Tools for automatic verification of security protocols: ProVerif, Scyther

Skills to acquire

  • Specify a protocol in a suitable formal framework
  • Formally define the security property against which the protocol should be checked
  • Select an appropriate verification tool to analyze the protocol
  • Detect logical flaws in improperly designed or implemented protocols


Barbara FILA is an associate professor (Maître de conférences) at Institut National des Sciences Appliquées (INSA Rennes) and a researcher at the Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) in Rennes. She is a member of the Security and Privacy (SPICY) project-team.

This site uses cookies to improve your user experience and to achieve audience statistics.
I acceptI refuseKnow more