Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Protocoles cryptographiques : preuves formelles et calculatoires / Cryptographic protocols: formal and computational proofs (48h, 6 ECTS)

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

Intervenants en 2020-2021 / Teachers for 2020-2021

  • Hubert Comon-Lundh (12h)
  • Vincent Cheval (12h)
  • David Pointcheval (12h)
  • Karthikeyan Bhargavan (12h)

First lecture: Tuesday Sept. 15th at 12:45 - Room 1013 in Sophie Germain Building.

Objectifs / Goals of the course

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. Nous présenterons ces deux modèles, les techniques de preuves associées, et des résultats qui font le lien entre eux. Nous considérerons aussi leur mise en oeuvre, en montrant un outil de preuve automatique pour chaque modèle, et en les appliquant à la vérification de programmes qui implémentent des 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.

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. We shall present these two models, the associated proof techniques, and results that relate them. We shall also consider their implementation, by showing an automatic proof tool for each model, and by applying them to the verification of programs that implement cryptographic 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.

Programme du cours / Course program

1. Symbolic verification (H. Comon-Lundh and V. Cheval)

  • Introduction to protocols, security properties, and attacks.
  • Protocol modeling in the applied pi-calculus
  • Semantics: symbolic and computational semantics
  • Indistinguishability properties
  • The ProVerif tool: verification of secrecy, correspondences, and equivalences.
  • Computational soundness of static equivalence

2. Computational cryptography (D. Pointcheval)

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

3. Verification of protocol implementations (K. Bhargavan)

  • Attacks on real-world crypto protocols such as TLS and IPsec
  • The F* tool (https://www.fstar-lang.org): verifying purely-functional and effectful programs
  • Verifying simple cryptographic protocol implementations in F*: signatures, MACs, stateful encryption, RPC, encrypt-then-mac, etc.
  • On the formal verification of a complete HTTPS stack (https://project-everest.github.io)

Planning provisoire / Preliminary schedule

Sept. 15 H. Comon-Lundh
Sept. 22 H. Comon-Lundh
Sept. 29 V. Cheval
Oct. 6 V. Cheval
Oct. 13 V. Cheval
Oct. 20 V. Cheval
Oct. 27 H. Comon
Nov. 3 H. Comon IND-CPA encryption schemes and computational soundness of static equivalence
Nov. 10 H. Comon-Lundh Revisions
Nov. 17 V. Cheval Revisions
Dec. 1H. Comon-Lundh/V. Cheval Exam
Dec. 8 D. Pointcheval Provable Security in the Computational Model
Dec. 15 D. Pointcheval The Case of Public Key Encryption
Jan. 5 D. Pointcheval The Case of Signatures
Jan. 12 D. Pointcheval Application to Authenticated Key Exchange
Jan. 19 K. Bhargavan
Jan. 26 K. Bhargavan
Feb. 2 K. Bhargavan
Feb. 9 K. Bhargavan
Feb. 16 D. Pointcheval Revisions
Feb. 23 K. Bhargavan Revisions
Mar. 2 or 9 D. Pointcheval/K. Bhargavan Exam

The exam 2020 (first part of the module) will take place on Dec 1rst 12h45-15h45. The exam will be sent by mail to the registered students. Students are allowed to access any online resource, but should complete their exam alone. A pdf file containing their solution is expected by mail at 15:45 (and until 16:00 for technical reasons).

Langue / Language policy

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

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

Supports de cours / Lecture notes

You can find here some material related to the class: The page of the class 2.30 by H. Comon

Pré-requis / Prerequisites

Pas de pré-requis particulier, mais on s'appuiera sur les pré-requis généraux du MPRI (sémantique, logique, typage, ...).

No specific prerequisites. We will however rely on the general prerequisites of the MPRI (semantics, logic, typing...).

Cours liés / Related courses

Concurrence / Concurrency (2-3): Il est recommandé de suivre le cours 2-3, car les modèles présentés dans la 2e partie du cours sont des modèles de la concurrence (même s'ils sont différents de ceux du cours 2-3). It is recommended to attend course 2-3, since the formal models presented in the 2nd half of the course are models of concurrency (although different from those of course 2-3).

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.

Bibliographie / Bibliography

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.

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. To appear. A preliminary verion is available here.

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

Equipe pédagogique / Possible lecturers

David Baelde MCF ENS Cachan - LSV & INRIA
Karthikeyan Bhargavan DR INRIA
Bruno Blanchet DR INRIA
Vincent Cheval CR INRIA
Hubert Comon-Lundh PU ENS Cachan - LSV
David Pointcheval DR ENS Paris - DIENS
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA