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

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cours:c-2-30 [2019/01/23 10:43]
baelde [Planning provisoire / Preliminary schedule]
cours:c-2-30 [2019/10/16 15:08] (current)
baelde [Planning provisoire / Preliminary schedule]
Line 4: Line 4:
 [[http://prosecco.gforge.inria.fr/personal/bblanche/|Bruno Blanchet]] (Inria, Prosecco team). [[http://prosecco.gforge.inria.fr/personal/bblanche/|Bruno Blanchet]] (Inria, Prosecco team).
  
-==== Intervenants en 2018-2019 / Teachers for 2018-2019 ==== +==== Intervenants en 2019-2020 / Teachers for 2019-2020 ====
-  * David Pointcheval (12h) +
-  * Bruno Blanchet (12h)+
   * David Baelde (24h)   * David Baelde (24h)
 +  * Bruno Blanchet (12h)
 +  * Karthikeyan Bhargavan (12h)
  
-First lecture: Wednesday Sept. 12th at 16:15 - Room 1003 in Sophie Germain Building.+First lecture: Wednesday Sept. 11th at 16:15 - Room 1014 in Sophie Germain Building.
  
  
Line 21: Line 21:
  
 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. 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.
- 
-Des [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/poly.pdf|notes de cours]] inachevées mais pouvant être utiles. 
  
 //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.// //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.//
Line 42: Line 40:
 ==== Programme du cours / Course program ==== ==== Programme du cours / Course program ====
  
-===1. Computational cryptography (D. Pointcheval)===+===1. Symbolic verification (D. Baelde)=== 
 + 
 +See [[http://www.lsv.fr/~baelde/secu|the teacher's page]] for slides and lecture notes. 
 + 
 +  * Introduction to protocols, security properties, and attacks. 
 +  * Protocol modeling in the applied pi-calculus, undecidability results. 
 +  * Verification for a bounded number of sessions: decision procedures for deducibility and equivalence. 
 +  * The ProVerif tool: verification of secrecy, correspondences, and equivalences. 
 +  * Composition and/or typing results depending on time and demand. 
 + 
 +===2. Computational cryptography (D. Baelde)===
   * Security proofs in the computational model   * Security proofs in the computational model
   * Game-based proofs and encryption   * Game-based proofs and encryption
Line 48: Line 56:
   * Protocols   * Protocols
  
-===2. Mechanizing computational security proofs (B. Blanchet)===+===3. Mechanizing computational security proofs (B. Blanchet)===
   * The tool CryptoVerif   * The tool CryptoVerif
   * Small example: Full Domain Hash signature scheme   * Small example: Full Domain Hash signature scheme
Line 54: Line 62:
   * Practical exercises using CryptoVerif   * Practical exercises using CryptoVerif
  
-===3. Symbolic verification (D. Baelde)=== +===4. Verification of protocol implementations (K. Bhargavan)===
- +
-This part is based on the above-mentionned [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/poly.pdf|lecture notes]], with variations. The [[http://www.lsv.fr/~baelde|slides]] of the lectures are available for reference. +
- +
-  * Introduction to protocols, security properties, and attacks. +
-  * Protocol modeling in the applied pi-calculus, undecidability results. +
-  * Verification for a bounded number of sessions: decision procedures for deducibility and equivalence. +
-  * The ProVerif tool: verification of secrecy, correspondences, and equivalences. +
-  * Composition and/or typing results depending on time and demand. +
- +
- +
-/** +
-===3. Verification of protocol implementations (K. Bhargavan)===+
   * Attacks on real-world crypto protocols such as TLS and IPsec   * 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    * 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.          * 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)   * On the formal verification of a complete HTTPS stack (https://project-everest.github.io)
-**/+
 ==== Planning provisoire / Preliminary schedule ==== ==== Planning provisoire / Preliminary schedule ====
 +
 +|Sept. 11| D. Baelde| Intro |
 +|Sept. 18| D. Baelde| Formal semantics 1 |
 +|Sept. 25| D. Baelde| Formal semantics 2 + Proverif intro |
 +|Oct.   2| D. Baelde| Deduction, symbolic semantics |
 +|Oct.   9| D. Baelde| Deducibility constraints |
 +|Oct.  16| D. Baelde| Unbounded verification in Proverif |
 +|Oct.  23| D. Baelde| Equivalences |
 +|Oct.  30| No course| |
 +|Nov.   6| D. Baelde| Computational security |
 +|Nov.  13| D. Baelde| Bana-Comon logic |
 +|Nov.  20| D. Baelde| Revisions |
 +|Nov.  27| D. Baelde|Exam|
 +
 +|Dec.   4| B. Blanchet| |
 +|Dec.  11| B. Blanchet| |
 +|Dec.  18| B. Blanchet| |
 +|Jan.   8| B. Blanchet| |
 +|Jan.  15| K. Bhargavan| |
 +|Jan.  22| K. Bhargavan| |
 +|Jan.  29| K. Bhargavan| |
 +|Feb.   5| K. Bhargavan| |
 +|Feb.  12| B. Blanchet|Revisions|
 +|Feb.  19| K. Bhargavan|Revisions|
 +|Feb.  26 or Mar. 4|B. Blanchet/K. Bhargavan|Exam| 
 +
 +
 +
 +/** 2018-2019
  
 |Sept. 12 | D. Pointcheval| [[http://www.di.ens.fr/~pointche/enseignement/mpri2/cm1.pdf|Les preuves de sécurité dans le modèle calculatoire]]| |Sept. 12 | D. Pointcheval| [[http://www.di.ens.fr/~pointche/enseignement/mpri2/cm1.pdf|Les preuves de sécurité dans le modèle calculatoire]]|
Line 101: Line 126:
 |Feb. 27 | D. Baelde| Exam | |Feb. 27 | D. Baelde| Exam |
  
- +* 2014-2015
- +
- +
- +
-/** 2014-2015+
 |Sept. 17|S. Delaune| Introduction [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/intro.pdf|slides]] - Intruder deduction problem [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/feuille-cours1.pdf|feuille defintions + exercices]]| |Sept. 17|S. Delaune| Introduction [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/intro.pdf|slides]] - Intruder deduction problem [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/feuille-cours1.pdf|feuille defintions + exercices]]|
 |Sept. 24|S. Delaune| Modelling protocols and their security properties [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/slides-cours2.pdf|slides]] - [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/feuille-cours2.pdf|exercices]]| |Sept. 24|S. Delaune| Modelling protocols and their security properties [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/slides-cours2.pdf|slides]] - [[http://www.lsv.ens-cachan.fr/~delaune/MPRI14-15/feuille-cours2.pdf|exercices]]|
 
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