Cryptographic protocols: formal and computational proofs
This page contains lecture materials for Karthikeyan Bhargavan's lectures for the MPRI course 2.30: Protocoles cryptographiques : preuves formelles et calculatoires / Cryptographic protocols: formal and computational proofs.
The links below will be updated as the course progresses; materials provided for future lectures should only be considered as a rough guide.

Lecture 1 (18 Sept 2013): Introduction to Cryptographic Protocols.
We discussed some cryptographic protocols, described them using an informal notation, and discussed symbolic and computational attacks on them. We learnt how to model protocols in a small process calculus, using NeedhamSchroeder as an example.
slides in pdf (some exercises)
poly in pdf (some exercises)
(Extra: For more protocols to attack see these slides used in this course) 
Lecture 2 (25 Sept 2013): Proofs in the Symbolic Model I
We discussed the syntax and semantics of the applied pi calculus. We learnt one symbolic technique for proving syntactic secrecy goals.
slides in pdf (some exercises)
poly in pdf (some exercises)
Additional reading: Applied pi calculus tutorial 
Lecture 3 (2 Oct 2013): Proofs in the Symbolic Model II
We studied a detailed case study of Web Services Security protocols and their modeling and proofs in the applied pi calculus.
We began to study the complexity of automated verification of protocols in bounded sessions.
slides in pdf (some exercises)
poly in pdf (some exercises)

Lecture 4 (9 Oct 2013): Proofs in the Symbolic Model III
We studied the decidability of bounded session verification.
We proved the undecidability of secrecy in the applied pi calculus
We studied a security type system for the applied pi calculus, and concluded with some applications of symbolic protocol analysis
slides in pdf (some exercises)
poly in pdf (some exercises)

Revisions (20 Nov 2013)
We revised material from the first four lectures and did exercises
slides in pdf (some exercises)

Lecture 5 (22 Jan 2014): Verifying protocol implementations
Lecture 6 (29 Jan 2014): Verifying protocol implementations
We discussed the differences between protocol models and their implementations.
We studied the RCF language and type system.
We used RCF to symbolically verify the securit of some programs, including an authentication protocol.
slides in pdf (some exercises)
Additional material: RCF a compact definition of the type system, plus exercises.
 Principles and Applications of Refinement Types a tutorial on the type system.
 Cryptographic Verification by Typing for a Sample Protocol Implementation, a tutorial on verification using F7.

NO LECTURE (5 Feb 2014)

Lecture 7 (12 Mar 2014): Computational verification of protocol implementations.
We learnt how to use types to model and verify protocol code in the computational model. We began a case study of the TLS protocol and its implementation.
slides in pdf (some exercises)

Lecture 8 (19 Mar 2014): Verifying protocol implementations
We finished the TLS case study and compared the verification of TLS using F7 with other verifications using ProVerif and CryptoVerif.
slides in pdf (exercise on last slide, to hand in by Mon 24/02)

Revisions (26 Mar 2014)
Exercises and solutions
Further reading (not required for lectures):
 Secrets and Lies: Digital Security in a Networked World, Bruce Schneier. Wiley, 20002004.
An enjoyable and easytoread book about practical issues in securing computer systems.  Handbook of Applied Cryptography, Menezer, van Oorschot, and Vanstone. CRC Press, 19962001.
Comprehensive guide to cryptographic algorithms (chapters available online)  Modern Cryptography: Theory and Practice, Wenbo Mao. Prentice Hall, 2003
Textbook on cryptographic schemes and protocols, includes some discussion of formal methods.  Communicating and Mobile Systems: The Pi Calculus, Robin Milner.
 The PiCalculus: A Theory of Mobile Processes, Davide Sangiorgi.