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/08/01 10:15]
blanchet [Planning provisoire / Preliminary schedule]
cours:c-2-30 [2019/12/04 22:13] (current)
blanchet [Planning provisoire / Preliminary schedule]
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 44: Line 42:
 ===1. Symbolic verification (D. Baelde)=== ===1. Symbolic verification (D. Baelde)===
  
-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.+See [[http://www.lsv.fr/~baelde/secu|the teacher's page]] for slides and lecture notes.
  
   * Introduction to protocols, security properties, and attacks.   * Introduction to protocols, security properties, and attacks.
Line 72: Line 70:
 ==== Planning provisoire / Preliminary schedule ==== ==== Planning provisoire / Preliminary schedule ====
  
-|Sept. 11| D. Baelde| | +|Sept. 11| D. Baelde| Intro 
-|Sept. 18| D. Baelde| | +|Sept. 18| D. Baelde| Formal semantics 1 
-|Sept. 25| D. Baelde| | +|Sept. 25| D. Baelde| Formal semantics 2 + Proverif intro 
-|Oct.   2| D. Baelde| | +|Oct.   2| D. Baelde| Deduction, symbolic semantics 
-|Oct.   9| D. Baelde| | +|Oct.   9| D. Baelde| Deducibility constraints 
-|Oct.  16| D. Baelde| | +|Oct.  16| D. Baelde| Unbounded verification in Proverif 
-|Oct.  23| D. Baelde| |+|Oct.  23| D. Baelde| Equivalences |
 |Oct.  30| No course| | |Oct.  30| No course| |
-|Nov.   6| D. Baelde| | +|Nov.   6| D. Baelde| Computational security 
-|Nov.  13| D. Baelde|Revisions+|Nov.  13| D. Baelde| Bana-Comon logic 
-|Nov.  20 or 27| D. Baelde|Exam|+|Nov.  20| D. Baelde| Revisions | 
 +|Nov.  27| D. Baelde|Exam|
  
-|Dec.   4| B. Blanchet| |+|Dec.   4| B. Blanchet| [[https://prosecco.gforge.inria.fr/personal/bblanche/MPRI/2019-20/1-computational.pdf|A bit of computational crypto]] [[https://prosecco.gforge.inria.fr/personal/bblanche/MPRI/2019-20/cryptoverif.pdf|CryptoVerif]] [[https://prosecco.gforge.inria.fr/personal/bblanche/MPRI/2019-20/enc-then-MAC.cv|enc-then-MAC.cv]] |
 |Dec.  11| B. Blanchet| | |Dec.  11| B. Blanchet| |
 |Dec.  18| B. Blanchet| | |Dec.  18| B. Blanchet| |
 
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