Formal Security Analysis of Cryptographic Protocol Code
Developing formal proofs of correctness for security-critical software has been a long-cherished goal both for cryptographers and for the program verification community. Recent advances in the state of automated theorem-proving has brought this goal within reach. In this course, we shall learn how to use a special-purpose cryptographic prover to verify the security of protocol implementations written in the functional programming language F#, a dialect of OCaml. The course proceeds in two parts.
- We begin by studying the syntax and semantics of a concurrent call-by-value lambda calculus, called F, a subset of F#. We formalize the notion of an attacker against F programs and learn how to specify protocol security goals, such as authentication and secrecy. Through small protocol examples, we learn how to prove these security goals by reasoning about the traces of an F program when composed with an arbitrary attacker.
- We then study the syntax and semantics of the applied pi-calculus, a variant of the pi-calculus designed specifically for the modelling and proof of cryptographic protocols. We study a translation from F programs to applied pi-calculus processes and formalize the correctness of this translation. We learn how to automatically verify the security of F programs by translating them using the compiler FS2PV and then verifying the resulting processes using the cryptographic prover ProVerif. We evaluate the strengths and weaknesses of this technique over large verification case studies of standard protocols, such as TLS.
Verification tools used in this course:
- ProVerif: A Cryptographic Protocol Verifier for the Applied Pi-Calculus
- FS2PV: A Cryptographic Protocol Verifier for F#
- Verifying Web Services Security, Karthikeyan Bhargavan, Bertinoro, June 2009. [slides]