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-30f [2011/07/13 11:24] (current)
hubertcomon created
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,
 + 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
 +
  
 
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