Formal Security Analysis of Cryptographic Protocol Code

For IIT Delhi Course Schedule and Lecture Materials, click here.

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.

  1. 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.
  2. 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.
By the end of the course, the student will have been exposed to the theory underlying the security analysis of distribured programs and gained some experience in the use of a leading security verification tool. The course will be accessible to students with some background in programming language theory, specifically some working knowledge of the syntax and semantics of foundational calculi such as the lambda calculus and pi calculus, and some basic type theory.

Verification tools used in this course:

Related courses: