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 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é.
Exemples (informels) de protocoles et de propriétés de sécurité.
Formalisations des protocoles; exemples d'interprétations: calculatoire et symbolique.
Introduction à un fragment du pi-calcul appliqué; exemples de formalisation de protocoles.
Exemples de primitives cryptographiques; formalisation de leurs propriétés algébriques.
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
Problème de déductibilité: le cas d'un attaquant passif. Le problème est complet pour PTIME pour les systèmes locaux.
Indécidabilité de la sécurité dans le cas d'un attaquant actif.
Cas d'un nombre borné de sessions. Contraintes de déductibilité et algorithmes de décision pour les propriétés de traces.
Résultats de combinaison; modularité de la sécurité pour certaines classes de protocoles.
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
Full abstraction de l'équivalence statique: le théorème d'Abadi & Rogaway.
Exemples d'extensions à d'autres primitives, avec d'autres hypothèses; attaquant adaptatif.
É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
Indistinguabilité et accessibilité dans le modèle calculatoire; sécurité sémantique, non-malléabilité, relations.
Sécurité prouvée calculatoire: approche par jeux; méthodologie générale, exemples, interprétation de résultats
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.
5. Automatisation des preuves de protocoles
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.
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.
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.
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 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
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 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 here.
