Sécurité des protocoles
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
Biography
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.