Tutorial Speaker
Véronique Cortier is a CNRS research director at Loria in Nancy, France. She belongs to the Inria group Pesto. Véronique Cortier obtained her PhD in Computer Science at ENS Cachan in March 2003. She is a specialist in network security protocols, her work includes the development of Belenios, an open source voting system.
Abstract
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 this tutorial, 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.
To practice the modeling and analysis of protocols, we use the automatic
tool ProVerif.
Note: We encourage attendees to install the ProVerif tool before
attending the tutorial, in case the network would not be reliable. The
ProVerif tool can be downloaded and installed from the webpage of the
tool http://prosecco.gforge.inria.fr/personal/bblanche/proverif/