Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

Protocoles cryptographiques: preuves formelles et calculatoires (24h, 3 ECTS)

Intervenants du cours 2008-2009 :

1. Bruno Blanchet (6h)
2. Stéphanie Delaune (9h)
3. 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.

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).

1. Modèle formel, à base de termes; notion d'indistinguabilité formelle sur les termes.
2. Modèle calculatoire, indistinguabilité.
3. 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.

1. Modèle formel: indécidabilité dans le cas général, résultat de décidabilité pour un nombre borné de sessions [8].
2. Modèle formel: preuves automatiques dans le cas d'un nombre non-borné de sessions, pour le cas du secret uniquement, outil Proverif [1].
3. Modèle formel: typage cryptographique pour les propriétés d'authenticité [6,7].
4. Modèle calculatoire: typage cryptographique pour l'indistinguabilité.
5. 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

1. par compilation vers Proverif et Cryptoverif [4];
2. ou directement par le typage [3].

Planning des séances

Langues du cours :

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 :

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 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

• Année 2008-2009
• Année 2007-2008

Équipe pédagogique