— |
cours:c-2-30f [2011/07/13 11:24] (current) hubertcomon created |
| + | |
| + | [[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, |
| + | 15th 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 |
| + | 2006. 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 |
| + | |
| | | |