CryptoVerif:  Mechanizing Game-Based Proofs of Security Protocols

by Bruno Blanchet

Some background in cryptography would help, though I plan to recall most useful notions.

Here are two useful references:

- Mihir Bellare and Chanathip Namprempre. Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition Paradigm. Journal of Cryptology, volume 21, pages 469-491, 2008. https://eprint.iacr.org/2000/025

- M. Bellare and P. Rogaway. Random Oracles Are Practical: a Paradigm for Designing Efficient Protocols. In CCS’93, pages 62–73. ACM Press, 1993. https://cseweb.ucsd.edu/~mihir/papers/ro.pdf, Section 4 and Appendix B.

* References that cover most of what Bruno plans to present during the school:

- Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols. In Tobias Nipkow, Olga Grumberg, and Benedikt Hauptmann, editors, Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 1-25. IOS Press, May 2012. https://bblanche.gitlabpages.inria.fr/publications/BlanchetMOD11.html

- Bruno Blanchet and David Pointcheval. Automated Security Proofs with Sequences of Games. In Cynthia Dwork, editor, CRYPTO'06, volume 4117 of Lecture Notes in Computer Science, pages 537-554, Santa Barbara, CA, August 2006. Springer. https://eprint.iacr.org/2006/069

* The tool CryptoVerif is available at https://cryptoverif.inria.fr