Responsable / Teacher in charge: Bruno Blanchet (Inria, Prosecco team).

• Bruno Blanchet (24h)
• Adrien Koutsos (12h)
• Aymeric Fromherz (12h)

First lecture: Wednesday Sept. 18th at 16:15 - Room 1004 in Sophie Germain Building.

Ce cours s'adresse à la fois aux étudiants intéressés par la logique, la concurrence, la sémantique et à ceux intéressés par la cryptographie. En effet, il étudie les protocoles cryptographiques en utilisant des outils formels (calculs de processus, sémantique, typage, logique, ...).

Les protocoles cryptographiques sont des programmes distribués qui visent à sécuriser des communications et transactions en utilisant des primitives cryptographiques. La conception des protocoles cryptographiques est difficile: de nombreuses erreurs ont été découvertes dans des protocoles après leur publication. Il est donc particulièrement important de pouvoir obtenir des preuves que ces protocoles sont sûrs.

Deux modèles des protocoles ont été considérés: le modèle symbolique et le modèle calculatoire. Cette année, nous considérerons seulement le modèle calculatoire, qui est le plus précis et qui est utilisé dans les preuves manuelles des cryptographes. Nous présenterons les techniques de preuves associées. Nous considérerons aussi leur mise en oeuvre, en montrant des outils de preuve automatique ou interactive dans ce modèle, et en les appliquant à la vérification de programmes qui implémentent des primitives ou protocoles cryptographiques.

Ce cours sera l'occasion d'adapter et d'utiliser des outils formels, comme les calculs de processus, la sémantique, le typage et la logique, au cas particulier de l'étude des protocoles cryptographiques.

This course targets both students interested in logic, concurrence, semanticsm and those interested in cryptography. Indeed, it studies cryptographic protocols using formal tools (process calculi, semantics, typing, logic, ...).

Cryptographic protocols are distributed programs which aim at securing communications and transactions by the means of cryptographic primitives. The design of cryptographic protocols is difficult: numerous errors have been discovered in protocols after their publication. It is therefore particularly important to be able to obtain proofs that protocols are secure.

Two models of the protocols have been considered: the formal model and the computational model. This year, we will only consider the computational model, which is the most precise and the one used in the manual proofs of cryptographers. We shall present the associated proof techniques. We shall also consider their implementation, by showing automatic or interactive proof tools in this model, and by applying them to the verification of programs that implement cryptographic primitives or protocols.

This course will be an opportunity to adapt and use formal tools, such as process calculi, semantics, and logic to the particular case of the study of cryptographic protocols.

• Security proofs in the computational model
• Game-based proofs and public-key encryption
• Signatures
• Protocols

• The tool CryptoVerif
• Small example: Full Domain Hash signature scheme
• Practical exercises using CryptoVerif

• Logical modeling of protocol security
• Capturing cryptographic arguments as logical reasoning rules
• Example: unlinkability of the Private Authentication protocol
• Reasoning about correspondence properties: the local logic
• Application: authentication of the Basic Hash protocol

• The F* tool (https://www.fstar-lang.org): verifying purely-functional and effectful programs
• Non-interference and Side-Channel Attacks
• Verifying C and assembly implementations with Low* and Vale
• Combining cryptographic security and verified implementations: the Noise* example

Exam conditions:

• First half: 3 hours written exam, at the same time and in the same room as the course
• Second half: 3 hours written exam, at the same time and in the same room as the course

The second session exam (“rattrapage”) will be an oral exam, at the request of the students.

The lecture notes (or slides when relevant) are in English.

The lecture will be in English as soon as one non-French speaking student attends. Otherwise, it will be given in French.

The slides will be made available online on the course web page.

On s'appuiera sur les pré-requis généraux du MPRI: probabilités, complexité (particulièrement dans la 1ère moitié), sémantique, logique du 1er ordre, programmation fonctionnelle, typage (particulièrement dans la 2e moitié).

We will rely on the general prerequisites of the MPRI: probabilities, complexity (especially in the first half), semantics, first-order logic, functional programming, typing (especially in the second half).

Références pour la première moitié: / References for the first half:

• probabilities: Cormen, Leiserson, Rivest, Introduction to algorithms, chap 6.
• basic number theory: Dan Boneh's crypto course, Appendix A.

Quelques ouvrages de référence en logique: / A few reference books in logic:

• (advised, french) Logique: Fondements et Applications, Schwarzentruber & Pinchinat & Le Barbenchon, Dunod, Jan. 2022
• Logique mathématique, Cori & Lascar, Dunod, Febr. 2021
• Introduction à la logique, David, Nour & Raffali, Dunod, Jan. 2004
• (english) Proof Theory and Automated Deduction, Goubault-Larrecq & Mackie, Springer, May 1997

Techniques en cryptographie et cryptoanalyse / Techniques in Cryptography and Cryptanalysis (2-12-1) Les preuves de sécurité dans le modèle calculatoire seront utilisées dans le cours 2-12-1. Le cours 2-30 sera donc une introduction essentielle pour le cours 2-12-1. Computational security proofs will be used in course 2-12-1. Course 2-30 will therefore be a useful introduction for course 2-12-1.

Algorithmes arithmétiques pour la cryptologie / Algorithmic number theory for cryptology (2-12-2),
Systèmes polynomiaux, calcul formel et applications / Polynomial systems, formal computation, and applications (2-13-1)
and Codes correcteurs d'erreurs et applications à la cryptographie / Error correcting codes and applications to cryptography (2-13-2): These 3 courses study the validity of some algorithmic assumptions used in security proofs.

Programmation fonctionnelle et systèmes de types / Functional programming and type systems (2-4),
Preuve de programmes / Proofs of programs (2-36-1),
Assistants de preuves / Proof assistants (2-7-2) These 3 courses can make learning F* easier as well as allow you to gain a deeper understanding of its foundations. In particular, course 2-4 provides a very useful introduction to functional programming and type systems, which are key concepts in F*.

M. Abadi and B. Blanchet. Analyzing security protocols with secrecy types and logic of programs. Journal of the ACM, 52(1):102–­146, Jan. 2005.

M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), pages 104–­115, London, United Kingdom, Jan. 2001. ACM Press.

D. Ahman, C. Hriţcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, N. Swamy. Dijkstra Monads for Free, In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). To appear, January 2017.

M. Arapinis, S. Delaune, and S. Kremer. From one session to many : Dynamic tags for security protocols. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, pages 128-­142, 2008.

D. Baelde, S. Delaune, C. Jacomme, A. Koutsos, S. Moreau. An Interactive Prover for Protocol Verification in the Computational Model. IEEE Symposium on Security and Privacy, S&P 2021. Paper.

G. Bana, H. Comon-Lundh. A Computationally Complete Symbolic Attacker for Equivalence Properties. ACM CCS 2014. Paper.

B. Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, pages 140­–154, Oakland, California, May 2006. Extended version available as ePrint Report 2005/401.

B. Blanchet and D. Pointcheval. Automated security proofs with sequences of games. In C. Dwork, editor, Advances in Cryptology ­ CRYPTO 2006, pages 537–­554, Santa Barbara, CA, Aug. 2006.

H. Comon-Lundh. Soundness of abstract cryptography. Lecture notes, Part 1. Available here, 2007.

H. Comon-Lundh, V. Cortier, and E. Zalinescu. Deciding security properties of cryptographic protocols. Application to key cycles. Transaction on Computational Logic, 2009. Available here.

H. Comon, A. Koutsos. Formal Computational Unlinkability Proofs of RFID Protocols. 30th IEEE Computer Security Foundations Symposium, CSF 2017. Paper.

D. Pointcheval. Advanced Course on Contemporary Cryptology, chapter Provable Security for Public-Key Schemes, pages 133­–189. Advanced Courses CRM Barcelona. (248 pages).

V. Shoup. Sequences of games : a tool for taming complexity in security proofs. Manuscript. Available here.

N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoue, S. Zanella-Béguelin. Dependent Types and Multi-Monadic Effects in F*, In 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2016.

Some more references on attacks and verification of TLS can be found here: https://mitls.org/pages/publications