Steve Kremer - Formal Modeling and Automated Analysis of Security ProtocolsSecurity 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.