Differences

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

@@ Line 1: / Line 1: @@
+[[C-2-30en|Anglais / English]]
+===== Protocoles cryptographiques: preuves formelles et calculatoires (48h + 12h TD, 6 ECTS) =====
+Responsables :
+[[http://www.di.ens.fr/~blanchet/|Bruno Blanchet]] (LIENS, ENS Paris & CNRS & INRIA)
+et
+[[http://www.lsv.ens-cachan.fr/~delaune/|Stéphanie Delaune]] (LSV, ENS Cachan & CNRS & INRIA)
+===== Intervenants du cours 2010-2011 :  =====
+  -  Stéphanie Delaune (12h + 3h TD
+  -  Steve Kremer (12h + 3h TD
+  -  David Pointcheval (12h + 3h TD
+  -  Bruno Blanchet (12h + 3h TD
+===== Motivations et objectifs du cours =====
+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.
+/**
+Ce sujet de recherche qui a démarré dans les années 90 a maintenant
+atteint sa maturité et peut faire l'objet d'un cours. Aujourd'hui les
+principales équipes de recherche en France sont l'équipe CASSIS, LORIA
+(Véronique Cortier, Michaël Rusinowitch), le LACL (Danièle Beauquier),
+le LIENS, ENS Paris (Bruno Blanchet, David Pointcheval), l'équipe
+SECSI, LSV, ENS Cachan (Hubert Comon-Lundh, Jean Goubault-Larrecq,
+Steve Kremer), et Verimag (Yassine Lachnech) et dans le monde
+l'équipe de Martín Abadi (MSR Silicon Valley et UC Santa Cruz), de
+David Basin (ETH Zurich), de Cédric Fournet et Andrew
+Gordon (MSR Cambridge), de Gavin Lowe (Oxford University), et de
+John Mitchell (Stanford University).
+**/
+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.
+===== Description du cours =====
+**1. Modèles des protocoles et des propriétés de sécurité**.
+	a. Exemples (informels) de protocoles et de propriétés de sécurité.
+	a. Formalisations des protocoles; exemples d'interprétations: calculatoire et symbolique.
+	a. Introduction à un fragment du pi-calcul appliqué; exemples de formalisation de protocoles.
+	a. Exemples de primitives cryptographiques; formalisation de leurs propriétés algébriques.
+	a. Propriétés de sécurité; secret (faible et fort), authenticité, attaques par devinette, propriétés d'indistinguabilité.
+ //Exercices//: modélisation en pi-calcul appliqué, recherche d'attaques simples.
+**2. Preuves de protocoles dans le modèle symbolique**
+	a. Problème de déductibilité: le cas d'un attaquant passif. Le problème est complet pour PTIME pour les systèmes locaux.
+	a. Indécidabilité de la sécurité dans le cas d'un attaquant actif.
+	a. Cas d'un nombre borné de sessions. Contraintes de déductibilité et algorithmes de décision pour les propriétés de traces.
+	a. Résultats de combinaison; modularité de la sécurité pour certaines classes de protocoles.
+	a. Algorithmes de décision pour l'équivalence statique.
+ //Exercices//: Extension à d'autres primitives cryptographiques (les résultats ne sont présentés dans le cours que sur un exemple.
+**3. Liens entre les modèles calculatoire et symbolique**
+	a. Full abstraction de l'équivalence statique: le théorème d'Abadi & Rogaway.
+	a. Exemples d'extensions à d'autres primitives, avec d'autres hypothèses; attaquant adaptatif.
+	a. Énoncé des résultats dans le cas actif: trace mapping et full abstraction de l'équivalence observationnelle.
+//Exercices//: Voir [8]: les pièges et les limites de la méthode. Aussi: des exemples d'attaque calculatoire sur des protocoles prouvés sûrs (dans le monde symbolique), montrant que les diverses hypothèses sont nécessaires.
+**4. Preuves dans le modèle calculatoire**
+	a. Indistinguabilité et accessibilité dans le modèle calculatoire; sécurité sémantique, non-malléabilité, relations.
+	a. Sécurité prouvée calculatoire: approche directe; hypothèses algorithmiques, preuves par réduction, techniques classiques (hybrides, rembobinage etc...)
+	a. Sécurité prouvée calculatoire: approche par jeux; méthodologie générale, exemples, interprétation de résultats
+	a. Sécurité des protocoles interactifs (fonctionnalité idéale); méthodologie, illustration sur la mise en accord de clé authentifiée.
+//Exercices//: réductions entre hypothèses algorithmiques, notions de sécurité, primitives simples. Analyse de sécurité de primitives.
+/**Supports de cours (Transparents et Articles) et exercices accessibles sur la [[http://www.di.ens.fr/~pointche/enseignement/mpri/|page web]]**/
+**5. Automatisation des preuves de protocoles**
+	a. Dans le modèle symbolique: outil ProVerif
+    * Formalisation en clauses de Horn; le démonstrateur ProVerif.
+    * Bi-processus et formalisation des propriétés d'équivalence.
+	a. Dans le modèle calculatoire: outil CryptoVerif
+    * Automatisation des preuves par jeux; survol de la méthode, calcul de processus utilisé pour représenter les jeux, transformation de jeux (transformations syntaxiques et transformations provenant d'hypothèses calculatoires), preuves de propriétés sur le jeu final.
+    * Introduction et démonstration de l'outil CryptoVerif.
+//Exercices//: Modélisation en clauses de Horn de protocoles et utilisation de Proverif sur des exemples concrets.  Manipulation de CryptoVerif.
+/**
+**4. Sécurité des protocoles et de leurs implantations par typage**
+	a. Types pour l'authenticité.
+   * Modèles; en particulier modélisation des protocoles et de l'adversaire comme des programmes en ML.
+   * Le langage RCF, un mini-ML avec des types étendus pour la sécurité. Syntaxe, sémantique et sureté des expressions.  Exemple: contrôle d'accès.
+   * Modélisation des primitives cryptographiques; principaux et corruption partielle; typage et adversaires actifs. Exemple: protocoles avec authentification et corrélation (MACs).
+   * L'outil de vérification par typage F7; exemples.
+   * Application: une implantation vérifiée de TLS.
+		b. Contrôle des flots d'information dans les programmes.
+   * Politiques de sécurité; treillis des niveaux d'intégrité et de confidentialité.
+   * Non-interférence, programmation et typage.
+   * Traduction typée vers RCF.
+   * Déclassification, corruption partielle et robustesse.
+		c. Contrôle des flots d'information dans les protocoles cryptographiques.
+   * Flots d'information dans le modèle calculatoire.
+   * Typage pour la cryptographie calculatoire.
+   * Application: compilation typée des politiques de sécurité.
+//Exercices//: exemples de petits protocoles vérifiables par typage; utilisation de F7.
+**/
+/**
+===== Planning des séances =====
+|Séance du 17/09 | S. Delaune | [[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance1/intro.pdf|Introduction aux protocoles]] |[[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance1/feuille-definitions.pdf|Quelques Définitions]] |[[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance1/feuille-exercices.pdf|Feuille d'exercices]] ||
+|Séance du 24/09 | S. Delaune | [[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance2/cours2.pdf|Feuille Cours + Exercices]]||||
+|Séance du 01/10 | S. Delaune | [[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance3/preuves.pdf|Preuves Cours 2]] | [[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance3/article.pdf|Article]] |[[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance3/slides.pdf|Slides]] |[[http://www.lsv.ens-cachan.fr/~delaune/enseignement/MPRI2008/Seance3/feuille-exercices.pdf|Feuille d'exercices]] |
+|Séance du 08/10 | C. Fournet | [[http://msr-inria.inria.fr/projects/sec/mpri/RCF-handout.pdf|RCF: Définitions et Exercices (Cours 4 et 5)]]| [[http://msr-inria.inria.fr/projects/sec/mpri/MPRI-cours-4.pdf|Slides Cours 4]]|
+|Séance du 15/10 | C. Fournet | [[http://research.microsoft.com/f7|F7, avec le code des exemples]]||||
+|Séance du 22/10 | B. Blanchet | [[http://www.di.ens.fr/~blanchet/MPRI/2008-09/proverif4.pdf|Transparents]] | [[http://www.di.ens.fr/~blanchet/MPRI/2008-09/exercice.pdf|Exercice]] | [[http://www.di.ens.fr/~blanchet/publications/AbadiBlanchetJACM7037.html|Article]] ||
+|Séance du 29/10 | B. Blanchet | [[http://www.di.ens.fr/~blanchet/MPRI/2008-09/cryptoverif4.pdf|Transparents]] | [[http://www.di.ens.fr/~blanchet/publications/BlanchetTDSC07.html|Article]] |||
+|Séance du 5/11 | C. Fournet | [[http://msr-inria.inria.fr/projects/sec/mpri/MPRI-Fournet.pdf|Slides 8/10, 15/10, et 5/11]]; corrigés des exercices 1, 2 [[http://msr-inria.inria.fr/projects/sec/mpri/ex//1//2.fs7|(fs7)]] [[http://msr-inria.inria.fr/projects/sec/mpri/ex//1//2.fs|(fs)]] et 4 [[http://msr-inria.inria.fr/projects/sec/mpri/ex_4.fs7|(fs7)]] [[http://msr-inria.inria.fr/projects/sec/mpri/ex_4.fs|(fs)]]||
+|Séance du 12/11 | Examen | ||||
+**/
+/** <font color="#FF0000">On commencera la prochaine séance par la correction de l'exercice 3 (exercice posé à l'examen de l'an dernier)
+</font>
+**/
+===== Langues du cours :  =====
+Les supports de cours seront en anglais.
+Le cours sera a priori en français.
+Cependant, s'il est suivi par des étudiants non francophones et en accord avec l'ensemble des étudiants qui le suivent, ce cours pourra aussi être en anglais.
+La première partie du cours sera donnée par Stéphanie Delaune et Steve Kremer
+et sanctionnée par un examen partiel. La deuxième partie du cours
+sera donnée par David Pointcheval et Bruno Blanchet et sanctionnée par un examen.
+En principe, les deux parties de cours ne peuvent pas  être validées
+séparément et la note finale du module sera obtenue par une
+moyenne de chacune des deux parties.
+===== Supports de cours : =====
+Les transparents et les notes de cours seront mis en ligne sur la page web du cours.
+Des exercices seront proposés pour faciliter l'assimilation des notions introduites.
+[[http://www.lsv.ens-cachan.fr/~kremer/Cours/MPRI1011/poly-mpri-2-30-draft.pdf|Notes de cours (draft)]]
+===== Pré-requis =====
+Pas de pré-requis particulier, mais on s'appuiera sur les pré-requis
+généraux du MPRI (sémantique, logique, typage, ...).
+===== Cours liés =====
+Cryptanalyse (2-12-1): Le cours 2-12-1 présente l'aspect complémentaire aux
+preuves de sécurité, à savoir les attaques sur les primitives cryptographiques,
+ainsi que sur les modèles de sécurité.
+Théorie algorithmique des nombres pour la cryptologie (2-12-2),
+Systèmes polynomiaux, calcul formel et applications (2-13-1)
+et Codes correcteurs d'erreurs et applications à la cryptographie (2-13-2): ces 3 cours
+étudient la validité d'un certain nombre d'hypothèses algorithmiques utilisées dans les preuves de
+sécurité.
+Concurrence (2-3): Il est vivement conseillé de suivre le cours 2-3, car les
+modèles formels présentés ici sont des modèles de la concurrence (bien
+que différents de ceux du cours 2-3).
+===== Bibliographie =====
+[1] M. Abadi and B. Blanchet. Analyzing security protocols with secrecy types and logic
+	 programs. //Journal of the ACM//, 52(1):102--146, Jan. 2005.
+[2] 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.
+[3] M. Arapinis, S. Delaune, and S. Kremer. From one session to many : Dynamic tags for se-
+	 curity protocols. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning,
+th International Conference, LPAR 2008, pages 128-142, 2008.
+[4] J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types
+	 for secure implementations. In 21st IEEE Computer Security Foundations Symposium
+	 (CSF'08), June 2008.
+[5] K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In ACM Conference on Computer and Communications Security,
+	 pages 459--468, 2008.
+[6] B. Blanchet. A computationally sound mechanized prover for security protocols. In
+	 IEEE Symposium on Security and Privacy, pages 140--154, Oakland, California, May
+. Extended version available as [[http://eprint.iacr.org/2005/401|ePrint Report 2005/401]].
+[7] 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.
+[8] H. Comon-Lundh. Soundness of abstract cryptography. Lecture notes, Part 1. Available
+	  [[http://staff.aist.go.jp/h.comon-lundh/|here]], 2007.
+[9] 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  [[http://arxiv.org/abs/0708.3564|here]].
+[10] C. Fournet and T. Rezk. Cryptographically sound implementations for typed information-flow security. In 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pages 323--335, 2008.
+[11] D. Pointcheval. Advanced Course on Contemporary Cryptology, chapter Provable Security for Public-Key Schemes, pages 133--189. Advanced Courses CRM Barcelona. (248 pages).
+[12] V. Shoup. Sequences of games : a tool for taming complexity in security proofs.
+	  Manuscript. Available [[http://www.shoup.net/papers/games.pdf|here]].
+===== Les années précédentes =====
+   * [[2009-2010-C-2-30|Année 2009-2010]]
+   * [[2008-2009-C-2-30-1|Année 2008-2009]]
+   * [[2007-2008-C-2-30-1|Année 2007-2008]]
+===== Équipe pédagogique =====
+|B. Blanchet|CR|ENS Paris|LIENS|
+|H. Comon-Lundh|PU|ENS Cachan|LSV|
+|S. Delaune|CR|ENS Cachan|LSV|
+|C. Fournet| MSR Cambridge & INRIA-MSR|||
+|S. Kremer|CR|ENS Cachan|LSV|
+|D. Pointcheval|DR|ENS Paris|LIENS|
+------
+   * Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.BrunoBlanchet, %MAINWEB%.SteveKremer, %MAINWEB%.CedricFournet, %MAINWEB%.StephanieDelaune, %MAINWEB%.HubertComonLundh, %MAINWEB%.DavidPointcheval