Steve Kremer - Formal Modeling and Automated Analysis of Security Protocols

Security protocols are concurrent programs that use cryptographic primitives, such as encryption, to guarantee some security properties, e.g. the confidentiality of a credit card number. History has shown that even, when these programs are relatively small, they are extremely tricky to get right. One successful approach has been the use of automated, symbolic methods to analyze these protocols. These methods build on techniques from model-checking, automated reasoning and concurrency theory.
In the first part of this course we will see how to model security protocols and their properties using dedicated process calculi that support cryptographic primitives. In the second part, we show how verification of security properties in these process calculi can be automated. Finally, if time allows, we briefly discuss how these techniques can be applied to the analysis of challenging examples such as e-voting protocols and hardware security modules.
The course will also contain a practical session where students will be introduced to the use of a protocol verification tool, e.g., ProVerif.

Readings:

  • Cryptographic protocols: Formal and Computational Proofs. Lecture notes by Bruno Blanchet, Hubert Comon-Lundh, Stephanie Delaune, Cedric Fournet, Steve Kremer and David Pointcheval (pdf).
  • Stephanie Delaune, Steve Kremer, Mark Ryan. Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster. Towards Trustworthy Elections 2010: 289-309.
  • Steve Kremer and Robert Kunnemann. Automated Analysis of Security Protocols with Global State. In Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P'14), IEEE Computer Society Press, San Jose, CA, USA, May 2014.