Sécurité des protocoles cryptographiques

Protocoles cryptographiques

   Un protocole cryptographique est un ensemble de programmes susceptibles de communiquer sur le réseau afin de réaliser une certaine fonctionnalité (cryptographique). Dans la typologie habituelle, chaque programme correspond à un rôle du protocole. Les agents, c’est-à-dire les machines ou les personnes susceptibles de mettre en œuvre le protocole peuvent jouer plusieurs rôles simultanément. Lorsqu’un agent honnête endosse un rôle, une instance du programme correspondant au rôle, appelée également processus, s’exécute sur la machine de l’agent en utilisant ses différentes données personnelles, par exemple son identité et les clés secrètes qu’il détient. À l’inverse, les agents malhonnêtes ne sont pas obligés de suivre un rôle du protocole. Dans la suite du document, nous nous plaçons dans le scénario où un ou plusieurs agents malhonnêtes sont utilisés par un attaquant global contrôlant le réseau de communication. Dans la plupart des protocoles, les processus sont groupés naturellement en sessions : chaque session correspond à une instance de la fonctionnalité désirée du protocole

Enjeux de l’analyse automatique de protocoles

   L’exemple précédent illustre la difficulté de concevoir un protocole cryptographique. En particulier, des attaques comme celle décrite plus haut s’avèrent particulièrement difficiles à déceler sur des protocoles complexes du fait de l’interaction possible entre différentes sessions en parallèle. En outre, les propriétés de sécurité en elles-mêmes étant rarement modulaires (i.e. la composition de plusieurs mécanismes sûrs n’est pas forcément sûre), prouver la correction d’un protocole directement à la main peut s’avérer extrêmement ardu. Ainsi, de nombreux travaux visent depuis une vingtaine d’années à élaborer des outils d’analyse de protocoles cryptographiques (voir paragraphe suivant). Étant donnée la difficulté du problème, ces analyses sont généralement menées dans des modèles dits symboliques (ou encore logiques, formels), formulés de manière abstraite vis-à-vis de l’implémentation des primitives cryptographiques. Le prix à payer pour cette abstraction est que certaines attaques sont susceptibles d’échapper à l’analyse : celles tirant justement parti des algorithmes choisis pour chaque primitive. Pourtant, de telles attaques sont prises en compte dans le formalisme standard utilisé pour les preuves de sécurité (manuelles) en cryptographie. Partant de ce constat, un effort important de recherche a débuté il y a quelques années [LMMS98, AR02] dans le but de développer des outils de preuve valables dans le formalisme cryptographique standard, et si possible toujours automatiques. Une manière d’atteindre ce but est par exemple de justifier les outils symboliques existants, c’est-à-dire de montrer que l’absence d’attaques logiques sur un protocole implique l’existence d’une preuve de sécurité dans le modèle cryptographique.

Recherche d’attaques logiques

   Une première famille regroupe les méthodes de recherche d’attaques en un nombre borné de sessions. Les premiers outils, fondés sur la vérification de modèle (model-checking) [Low96, MMS97], consistaient à explorer l’ensemble de l’espace des attaques possibles, pour un nombre borné de sessions et pour des messages de taille bornée. A. Huima [Hui99a] suggéra le premier que borner la taille des messages n’était pas nécessaire pour peu que l’on utilise un algorithme de résolution de contraintes symboliques ad hoc. Depuis cette voie a été largement explorée [AL00, MS01, Bor01], notamment avec la prise en compte récente de primitives ayant des propriétés algébriques comme le OU exclusif ou l’exponentiation modulaire à la DiffieHellman [BB05, DJ04a, CKRT03a, MS03, CKRT03b, CLS03, DLLT06, GRV05, CR05]. D’autres travaux ont été également entrepris afin de prendre en compte des propriétés de sécurité fines comme la résistance aux attaques par dictionnaire [CMAFE03, DJ04b], les équivalences de processus (finis) [DSV03], et les propriétés de jeux liées à la signature de contrat électronique [KR02, KK05].

Preuve symbolique

   Une seconde famille d’approches regroupe les méthodes de preuve symbolique. Ces méthodes s’appliquent à un nombre non borné de sessions au prix d’un algorithme approché, c’est-à-dire susceptible de refuser un protocole sans faille logique. Cette approximation est rendue nécessaire par l’indécidabilité du problème en général [EG83]. Tandis que les premières méthodes reposaient sur un assistant de preuve [Pau98, Bol97], d’autres techniques manuelles ont été proposées depuis, notamment à base de systèmes de type dans une algèbre de processus [Aba99], d’une logique spécialisée [BAN90, DMP03] ou d’autres formalismes [THG99]. Enfin, de nombreux outils de preuve automatiques ont été élaborés, reposant sur des techniques diverses, notamment :
– la recherche d’invariants inductifs [Mea99, CMR01],
– de l’analyse du flot de contrôle (control flow analysis) [BDNN02, ZD06],
– les automates d’arbre [Mon03, Gou00, CCM01, ZD06], et
– les clauses de Horn [Bla01, Gou04, AB05a, GRV05] avec plus récemment une extension aux propriétés d’équivalence observationnelle dans un langage de processus cryptographique [BAF05]. Le cadre symbolique dispose donc d’un nombre important d’outils d’analyse automatiques. Bien que le problème soit indécidable dans le cas général (et souvent (co-)NP-complet pour un nombre borné de sessions), les analyseurs les plus efficaces montrent de bonnes performances pratiques : par exemple Proverif [Bla01, BAF05] répond le plus souvent en quelques secondes. Les principales limites de l’approche symbolique résident sans surprise dans l’abstraction réalisée au moment de la modélisation :
– d’une part, il reste difficile de modéliser les protocoles qui ne sont pas conçus de manière modulaire, c’est-à-dire pour lesquels on en peut pas voir les primitives comme des « boîtes noires » ;
– d’autre part, il s’avère qu’un protocole sans faille logique n’est pas nécessairement sûr d’un point de vue cryptographique, à plus fortes raisons si des primitives cryptographiques de sécurité insuffisante sont employées. Ce dernier constat est à l’origine d’un nombre important de travaux sur la justification calculatoire de modèles symboliques.

Indistinguabilité entre données (cas passif)

    Le résultat de M. Abadi et de P. Rogaway [AR00, AR02] constitue le premier exemple de critère logique possédant une justification cryptographique. Considérant des termes construits sur une signature comprenant la paire, le chiffrement symétrique, des données privées (les clés) et des constantes, les auteurs montrent que si deux termes vérifient un certain critère formel alors les données concrètes ainsi représentées sont indistinguables par tout attaquant polynomial. Ce résultat a depuis été étendu de différentes manières : par une étude de la complétude [MW04a], par du chiffrement déterministe [Lau02], par différentes variantes de chiffrement (révélant la taille des messages ou les clés utilisées, ou encore à base de One-Time Pad) [ABS05], par les clés composées [LC03] et enfin par les cycles de chiffrement [AHBS05].

Formalismes logiques spécifiques

   Dans une perspective différente, d’autres travaux tentent de formaliser directement les raisonnements cryptographiques dans un cadre logique original. Ainsi,l’algèbre de processus probabilistes de P. Lincoln et al. [LMMS98] a donné lieu à plusieurs raffinements successifs par P. Mateus et al. [MMS03], J. Mitchell et al. [MRST01] et A. Ramanathan et al. [RMST04]. Dans le même but, A. Datta et al. [DDM+05] proposent une logique dédiée à la preuve de protocoles et justifiée au niveau cryptographique. Toutefois, ces différents formalismes logiques ne disposent pas d’outil automatique à l’heure actuelle.

Attaques par dictionnaire et propriétés d’équivalence

    En 2003, lorsque cette thèse a débuté, plusieurs modèles symboliques distincts coexistaient pour les attaques par dictionnaire [Low04, Coh02, CMAFE03, DJ04b]. Bien que reposant sur des intuitions similaires décrites par G. Lowe [Low04], ces définitions s’avéraient mutuellement incomparables, sans qu’il semblât alors possible de les départager et encore moins de les généraliser à des primitives cryptographiques avec propriétés algébriques, comme par exemple le OU exclusif. Au cours de l’année suivante, le cadre général du pi-calcul appliqué [AF01] suscita une nouvelle modélisation symbolique des attaques par dictionnaire reposant sur la notion d’équivalence statique [AF01] et due indépendamment à Fournet [Fou02] et à R. Corin, J. Doumen et S. Etalle [CDE04]. L’intérêt de cette définition était de proposer pour la première fois un critère général, paramétré par le choix d’une signature et d’une théorie équationnelle. Toutefois, l’article original de R. Corin et al. [CDE04] ne mentionne que le cas d’un intrus passif. De plus, cette définition ne bénéficiait initialement d’aucun outil d’analyse. Plus récemment, B. Blanchet, M. Abadi et C. Fournet [BAF05] ont formulé un critère approché pour la sécurité contre les attaques par dictionnaire dans le « nouveau » formalisme équationnel. Ce critère est valable dans le cas actif, pour un nombre non borné de sessions. L’implémentation, dans l’outil Proverif [Blab], montre de bonnes performances pratiques malgré la possibilité de non terminaison. À cette époque, l’existence d’un algorithme de décision (i.e. exact) pour les attaques par dictionnaire en un nombre borné de sessions selon la nouvelle définition générale (par exemple pour les théories équationnelles usuelles du chiffrement) restait donc un problème ouvert— le cas passif étant quant à lui subsumé par les travaux d’Abadi et Cortier [AC04]. Dans cette optique, une première contribution de cette thèse est de clarifier la notion d’attaque par dictionnaire dans le cas d’un intrus actif, en s’inspirant de la définition générale de R. Corin et al. [CDE04] et du critère proposé par B. Blanchet et al. [BAF05]. Dans le chapitre 3, nous proposons en effet un langage proche du picalcul appliqué étendu par des phases [BAF05], permettant (entre autres) d’énoncer la résistance aux attaques par dictionnaire de manière naturelle. En particulier, nous montrons que, dans ce cadre, la notion d’attaque par dictionnaire ne dépend pas du choix de l’équivalence observationnelle pour le langage (parmi les notions usuelles). Dans le même chapitre, nous donnons ensuite une sémantique symbolique à ce langage de processus, et montrons que le problème de la résistance aux attaques par dictionnaire pour un nombre borné de sessions se ramène à celui de la résolution de systèmes de contraintes symboliques bien choisis — en l’occurrence à base d’unification équationnelle du second ordre. Nous nous efforçons de résoudre ces systèmes de contraintes dans le chapitre 4 pour la famille des théories sous-terme-convergentes (définie au chapitre 2). Une première version de l’algorithme de résolution détaillé ici a été présentée à la conférence CCS’05 [Bau05]. Ensemble, les résultats des chapitres 3 et 4 décrivent ainsi la première procédure exacte, dans un cadre général, pour décider la sécurité contre les attaques par dictionnaire en un nombre borné de sessions. Plus exactement, nous montrons que ce problème est dans co-NP pour toute théorie sous-terme-convergente (finiment présentée). Soulignons que cette procédure s’applique à davantage de propriétés de sécurité. Outre les propriétés habituelles de secret simple et d’authentification, nous traitons en effet le cas d’une équivalence observationnelle à base de bi-processus inspirée de [BAF05] et généralisant la définition des attaques par dictionnaire. Cette équivalence implique en particulier les équivalences observationnelles définissables de la manière usuelle dans une algèbre de processus.

Table des matières

1 Introduction 
1.1 Cryptographie et protocoles cryptographiques 
1.1.1 Primitives et fonctionnalités
1.1.2 Protocoles cryptographiques
1.2 Analyse symbolique de protocoles
1.3 Lien entre modèles logiques et cryptographie 
1.4 Contributions et contenu de la thèse
2 Préliminaires 
2.1 Termes du premier ordre 
2.2 Substitutions
2.3 Théories équationnelles et systèmes de réécriture 
2.4 Problèmes équationnels et complexité 
2.5 Remplacements modulo E et symboles libres 
2.6 Présentation canonique d’une théorie convergente
2.7 Théories sous-terme-convergentes
I Sécurité logique des protocoles cryptographiques 
3 Spécification de protocoles cryptographiques 
3.1 Syntaxe et sémantique opérationnelle
3.1.1 Syntaxe
3.1.2 Sémantique à petits pas
3.1.3 Expressivité du langage
3.1.4 Équivalences observationnelles usuelles (∼=bf, ∼=b, ∼=may)
3.1.5 Bi-processus et équivalence associée ∼=diff
3.1.6 Relations entre équivalences observationnelles
3.2 Propriétés de sécurité
3.2.1 Secret simple
3.2.2 Authentification
3.2.3 Attaques par dictionnaire
3.2.4 Secret fort
3.2.5 Divulgation des secrets de longue durée
3.2.6 Codage des propriétés de sûreté dans ∼=diff
3.3 Sémantique ouverte 
3.3.1 Définition
3.3.2 Correction et complétude
3.4 Sémantique symbolique
3.4.1 Systèmes de contraintes symboliques
3.4.2 Définition
3.4.3 Correction et complétude
3.5 Décidabilité de la diff-équivalence pour les processus finis
3.5.1 Réduction vers la S-équivalence (ou la satisfiabilité)
3.5.2 Bornes inférieures de complexité
3.6 Conclusion 
4 Résolution des systèmes de contraintes de l’intrus 
4.1 Procédure de décision 
4.1.1 Systèmes de contraintes étendus
4.1.2 Principe de la procédure
4.1.3 Règles de transformation des systèmes de contraintes
4.1.4 Plan de la preuve
4.2 Correction des règles de transformation 
4.3 Résultats préliminaires 
4.3.1 Étude des règles de pré-résolution
4.3.2 Pré-ordre de stratification
4.3.3 Invariant de stratification
4.3.4 Évolution des relations ⊲⊳Ψ et ⊲Φ,C
4.3.5 Étude des dérivations standard
4.4 Complétude des dérivations standard 
4.4.1 Mesure de terminaison sémantique
4.4.2 Réduction des solutions d’un système
4.4.3 Progression
4.5 Terminaison
4.5.1 Notion de taille des systèmes de contraintes
4.5.2 Mesure de terminaison syntaxique
4.5.3 Règles prioritaires
4.5.4 Règles principales
4.5.5 Conclusion de la preuve de terminaison
4.6 Obtention d’un algorithme NP 
4.7 Conclusion et perspectives 
II Justification cryptographique de modèles logiques 
5 Comparaison des formalismes dans le cas passif 
5.1 Modèles abstraits, implémentations concrètes
5.1.1 Algèbres abstraites
5.1.2 Environnements, déductibilité et équivalence statique
5.1.3 Sémantique concrète
5.2 Lien entre algèbres abstraites et concrètes 
5.2.1 Sûreté et fidélité d’une implémentation
5.2.2 Relations entre notions de sûreté et de fidélité
5.3 Implications de la ≈E-sûreté dans les groupes abéliens 
5.3.1 Preuves d’équivalence statique dans les groupes
5.4 Critère de sûreté 
5.4.1 Sémantique idéale et critère de ≈E-sûreté
5.4.2 Environnements transparents
5.4.3 Cas des probabilités non uniformes
5.5 Perspectives
6 Applications 
6.1 Le OU exclusif pur 
6.2 Étude préliminaire de l’équivalence statique 
6.3 Chiffrement, clés faibles et attaques par dictionnaire 
6.3.1 Sortes, termes et théorie équationnelle
6.3.2 Implémentation
6.3.3 Correction cryptographique de l’équivalence statique
6.3.4 Application aux attaques par dictionnaire
6.4 Preuve du théorème 6.5  
6.4.1 Notations
6.4.2 Procédure de décision
6.4.3 Étude de la déductibilité
6.4.4 Terminaison et progression
6.4.5 Correction formelle
6.4.6 Sûreté calculatoire
6.5 Comparaisons 
7 Conclusion

Télécharger le rapport complet