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-1 [2011/07/12 19:26] (current)
Line 1: Line 1:
 +
 +===== Protocoles cryptographiques: preuves formelles et calculatoires (24h, 3 ECTS) =====
 +Responsables : 
 +[[http://www.lsv.ens-cachan.fr/~delaune/|Stéphanie Delaune]] (LSV, ENS Cachan & CNRS & INRIA).
 +et
 +[[http://research.microsoft.com/~fournet/|Cédric Fournet]] (MSR Cambridge & INRIA-MSR)
 +===== Intervenants du cours 2008-2009 :  =====
 +  -  Bruno Blanchet (6h
 +  -  Stéphanie Delaune (9h
 +  -  Cédric Fournet (9h
 +
 +===== 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 formel 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. Introduction. Qu'est-ce qu'un protocole cryptographique ? Exemples de protocoles et d'attaques.
 +
 +2. Cas passif. On s'interessera tout d'abord au cas plus simple où l'attaquant peut écouter les messages transmis, mais pas envoyer ses propres messages (attaquant passif).
 +
 + a. Modèle formel, à base de termes; notion d'indistinguabilité formelle sur les termes.
 + a. Modèle calculatoire, indistinguabilité.
 + a. Lien entre les deux modèles: moyennant des hypothèses adéquates, la sécurité dans le modèle formel implique la sécurité dans le modèle calculatoire (résultat d'Abadi et Rogaway [2]).
 +
 +3. Cas actif. On traite ici du cas où l'attaquant peut à la fois écouter les messages transmis et envoyer ses propres messages.
 +
 + a. Modèle formel: indécidabilité dans le cas général, résultat de décidabilité pour un nombre borné de sessions [8].
 + a. Modèle formel: preuves automatiques dans le cas d'un nombre non-borné de sessions, pour le cas du secret uniquement, outil Proverif [1].
 + a. Modèle formel: typage cryptographique pour les propriétés d'authenticité [6,7].
 + a. Modèle calculatoire: typage cryptographique pour l'indistinguabilité.
 + a. Automatisation directe des preuves calculatoires, outil Cryptoverif [5].
 +
 +4. Modèles et implémentations. On montre enfin comment appliquer ces techniques à la vérification du code (en ML) qui implémente des protocoles cryptographiques
 +
 + a. par compilation vers Proverif et Cryptoverif [4];
 + a. ou directement par le typage [3].
 +
 +
 +===== 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>
 +**/
 +/**|26/09|B. Blanchet (remplace S. K.)|[[http://www.lsv.ens-cachan.fr/~kremer/c-2-30-1-b.pdf|Indistinguabilité; modèle calculatoire; lien entre les deux modèles (cas passif)]]|
 +|03/10|S. Kremer| [[http://www.lsv.ens-cachan.fr/~kremer/c-2-30-1-c.pdf|Adversaire actif; indécidabilité dans le cas général; nombre borné de sessions; résolution de systèmes de contraintes]] |
 +|10/10|S. Kremer| [[http://www.lsv.ens-cachan.fr/~kremer/c-2-30-1-d.pdf|Modèle calculatoire pour adversaire actif; résultat de correction : propriétés de trace et secret de nonce]] |
 +|17/10|cours annulé| |
 +|24/10|B. Blanchet| [[http://www.di.ens.fr/~blanchet/MPRI/2007-08/proverif.pdf|Vérificateur ProVerif (jusqu'a page 48)]] |
 +|31/10|C. Fournet| [[http://research.microsoft.com/~fournet/talks/Verified-Implementations-MPRI-Oct07.pdf|Vérification des protocoles et de leurs implémentations : Applications aux services web]] |
 +|07/11|B. Blanchet| [[http://www.di.ens.fr/~blanchet/MPRI/2007-08/proverif.pdf|Vérificateur ProVerif (pages 49 et suivantes)]] |
 +|14/11|B. Blanchet (rattrapage 17/10)| [[http://www.di.ens.fr/~blanchet/MPRI/2007-08/cryptoverif.pdf|Vérificateur CryptoVerif]] |
 +|21/11|examen| |
 +**/
 +===== Langues du cours :  =====
 +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.
 +
 +/** Les transparents seront en anglais.**/
 +
 +Le sujet d'examen sera en français et en anglais.
 +
 +Les étudiants seront autorisés à rédiger leur examen en français ou anglais.
 +
 +===== Supports de cours : =====
 +Les transparents seront mis en ligne sur la page web du cours.
 +
 +/** et
 +des exemplaires seront distribués aux étudiants. 
 +**/
 +
 +
 +/**
 +Des exercices facultatifs seront proposés pour faciliter l'assimilation des notions introduites.
 +**/
 +===== Pré-requis =====
 +
 +Pas de pré-requis.
 +
 +===== Cours liés =====
 +
 +Cryptologie (2-12): Certains points comme les preuves de sécurité dans le 
 +modèle calculatoire sont à la charnière des deux cours.
 +Ainsi, les preuves de sécurité manuelles dans le modèle calculatoire
 +sont abordées dans le cours 2-12, et ce cours le complète en présentant 
 +des techniques automatiques. Ce cours n'est cependant pas un cours 
 +de cryptologie et fait largement appel à des notions de logique et
 +de sémantique.
 +
 +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 et B. Blanchet.
 +Analyzing security protocols with secrecy types and logic programs.
 +//Journal of the ACM//, 52(1):102--146, Jan. 2005.
 +
 +[2] M. Abadi et P. Rogaway.
 +Reconciling two views of cryptography (the computational soundness of
 +  formal encryption).
 +//Journal of Cryptology//, 15(2):103--127, 2002.
 +
 +[3] 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.
 +
 +[4] K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable implementations
 + of security protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW'06),
 + pages 139­152, June 2006.
 +
 +[5] 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]].
 +
 +[6] C. Fournet, A. D. Gordon, and S. Maffeis. A type discipline for authorization policies.
 + In European Symposium on Programming (ESOP'05), volume 3444 of Lecture Notes on
 + Computer Science, pages 141­156. Springer, 2005.
 +
 +[7] A. Gordon and A. Jeffrey. Authenticity by typing for security protocols. Journal of Computer
 + Security, 11(4) :451­521, 2003.
 +
 +[8] M. Rusinowitch et M. Turuani.
 +Protocol insecurity with finite number of sessions is NP-complete.
 +//Theoretical Computer Science//, 299(1--3):451--475, Avr. 2003.
 +
 +
 +===== Les années précédentes =====
 +   * [[2009-2010-C-2-30-1|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|
 +
 +
 +------
 +   * Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.BrunoBlanchet, %MAINWEB%.SteveKremer, %MAINWEB%.CedricFournet, %MAINWEB%.StephanieDelaune
 +
  
 
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