Soutenance mémoire
Logique du premier ordre
Nous allons définir ici de manière succincte la syntaxe et la sémantique de la logique du premier ordre. Pour une présentation plus détaillée, incluant les spécifications algébriques, le lecteur pourra se référer à [LEW96], ou encore à [AKKB99], plus proche de l’état de l’art. La définition d’un type de données (comme les listes d’entiers) comporte un certain nombre d’opérations (par exemple, prendre le successeur d’un entier, ou ajouter un entier à une liste). Ces opérations sont définies à la fois par leur nom et par leur arité (qui indique le type de leurs arguments ainsi que celui de leur valeur). La donnée d’un ensemble de sortes (qui représentent les noms des types possibles pour les arguments et valeurs) ainsi que d’un ensemble de symboles, chacun muni d’une arité constitue une signature algébrique.
Sémantique concrète des protocoles
Expliquons maintenant comment donner à un protocole cryptographique, représenté par un processus P = L1 [] . . . [] Ln ∈ ProcTr, une sémantique sous la forme d’une structure du premier ordre. Nous allons décrire cette structure au moyen d’une spécification en Casl qui sera composée de plusieurs parties, celles-ci étant, pour la plupart, indépendantes du protocole considéré. Signalons que cette modélisation est fortement inspirée de [Pau98], avec quelques différences toutefois. Pour décrire les noms, il nous faut, tout d’abord, une sorte Name, et l’interprétation de cette sorte doit satisfaire les contraintes suivantes :
– le domaine d’interprétation de Name doit être égal à Name ;
– ce domaine doit être partitionné en deux sous-domaines : les nonces créés seront pris dans le premier domaine alors que le second contiendra les constantes de l’exécution du protocole (les identités des participants, des données atomiques et le nom distingué 0). Pour ce faire, nous allons supposer que Name est infini et dénombrable et définir deux types libres Cst et Nonce qui seront tous deux identiques à celui des entiers. On définira Name comme étant leur réunion disjointe, de sorte que son domaine d’interprétation soit infini dénombrable, donc en bijection avec Name.
Interprétation abstraite algébrique
Nous allons décrire maintenant notre approche générale permettant de définir des abstractions pour des problèmes de la forme C |= ϕ où C est une structure du premier ordre et ϕ un énoncé sur une signature donnée. Rappelons que C est constitué d’ensembles (respectivement de fonctions, de relations) interprétant les sortes (respectivement les symboles de fonctions, les symboles de prédicats) de Σ. Le travail consistant à définir des abstractions se divise donc en :
– définir l’abstraction des domaines d’interprétation des sortes de Σ dans C ;
– définir l’abstraction des fonctions de C ;
– définir l’abstraction des relations de C ;
– définir l’abstraction de l’énoncé ϕ.
En ce qui concerne les deux premières tâches, nous choisissons d’abstraire l’algèbre [C] (sousjacente à C) par une algèbre B sur la même signature [Σ], ces deux algèbres étant reliées par un morphisme α : [C] → B. Afin de voir comment étendre cette algèbre en une structure du premier ordre, commençons par regarder un exemple.
Linéarisation des messages
L’abstraction que nous allons décrire maintenant présente un point commun et une différence majeure avec l’abstraction de la section précédente. Comme l’abstraction précédente, son but est de projeter l’ensemble des messages sur un ensemble fini. Elle a par contre l’avantage de procéder de manière beaucoup plus homogène. Comme pour l’abstraction précédente, nous allons partir de la [Σ•P]-algèbre de la section 6.1 notée B et du morphisme surjectif associé β : [CP ] → B. Nous allons là encore nous baser sur cette construction pour produire uneΣ•P-structure A.
Travaux existants
On peut citer trois types d’approches concernant la vérification formelle de protocoles optimistes d’échange. Dans chaque approche, le protocole est modélisé par un système de transitions. Dans les travaux de V. Shmatikov et J. Mitchell [SM00a, SM00b, SM02], il s’agit de systèmes de transitions ordinaires, finis, qui sont étudiés à l’aide de l’outil de vérification Murϕ. R. Chadha, M. Kanovich et A. Scedrov utilisent un formalisme de réécriture [CKS01], ce qui leur permet d’utiliser des systèmes de transitions infinis, en contrepartie les preuves doivent être faites à la main. Les propriétés qu’ils énoncent s’écrivent en termes de jeux, alors qu’avec Murϕ il est simplement possible de vérifier que tout état atteignable satisfait une certaine spécification. La troisième approche est celle de S. Kremer et J.-F. Raskin [KR01, KR02]. Elle utilise comme modèles des systèmes de transitions alternés et les propriétés attendues sont énoncées dans le langage de la logique temporelle alternée [AHK98]. Ce formalisme étend les systèmes de transitions classiques avec des concepts de théorie des jeux. Il en résulte que le modèle est simple à comprendre (c’est un système de transitions dans lequel le comportement des différents participants est représenté) et la vérification automatique d’un protocole donné possible, en utilisant l’outil Mocha. Un des inconvénients majeur était que l’étape de transformation d’un protocole en un système de transitions alterné était effectuée manuellement et incluait des simplifications qui demandaient une justification à part. Notre travail, en collaboration avec S. Kremer et J.-F. Raskin, avait essentiellement pour but de réaliser et justifier automatiquement ces simplifications, au moyen de techniques d’interprétation abstraite. Les concepts mis en jeu étaient déjà présents dans la littérature, mais il a fallu les adapter à cette approche, que nous détaillons dans la section suivante. La plupart des travaux associés à ce type de protocole doivent prendre en compte le fait que les participants au protocole, ainsi que les canaux de communication, peuvent fonctionner suivant plusieurs niveaux d’honnêteté. Ainsi, un participant peut être :
– honnête : il suit le protocole ;
– faiblement malhonnête : il ne suit pas le protocole et peut utiliser les messages reçus pour en construire de nouveaux et les envoyer ;
– fortement malhonnête : il peut de plus espionner tous les canaux de communication. De même, un canal de communication peut être :
– opérationnel : il délivre immédiatement les messages envoyés ;
– résistant : il délivre les messages envoyés en un temps fini (mais non borné) ;
– non-fiable : il ne délivre pas nécessairement les messages.
Vu la forme des propriétés attendues, il semble évident que si tous les canaux sont nonfiables, on ne pourra rien prouver. L’hypothèse minimale typique à faire sur les canaux de communication est la suivante : des canaux non-fiables entre A et B et des canaux résistants entre A et T et B et T. Le fait de distinguer plusieurs types de comportements malhonnêtes pour les participants permet de faire des analyses plus fines. Par exemple, l’attaque sur le protocole précédent découverte par V. Shmatikov et J. Mitchell existe dans notre modèle uniquement en présence d’un participant fortement malhonnête.
|
Table des matières
Introduction
1 La syntaxe
1.1 Un exemple de protocole
1.2 Messages et processus
1.3 Dans la suite
2 Vérification et abstractions
2.1 Modélisation
2.2 Des approximations correctes
I Propriétés de traces
3 Introduction
3.1 Un exemple
3.2 Les approches existantes
3.3 Notre approche
3.4 Les processus considérés
4 Modélisation algébrique de protocoles
4.1 Logique du premier ordre
4.2 Égalité et spécifications
4.3 Sémantique concrète des protocoles
5 Interprétation abstraite algébrique
5.1 Abstraction des structures
5.2 Guide pour les abstractions
6 En pratique
6.1 Projection des noms
6.2 Filtrage des messages
6.3 Linéarisation des messages
6.4 Que montre-t-on réellement ?
7 Optimalité
7.1 Catégories et institutions
7.2 Abstractions et traductions
7.3 Traductions et optimalité
7.4 Conclusion
II Propriétés de jeux
8 Introduction
8.1 Un exemple
8.2 Travaux existants
8.3 Notre approche
8.4 Syntaxe pour les protocoles d’échange
9 Systèmes de transitions alternés, logique temporelle alternée
9.1 Systèmes de transitions alternés
9.2 Logique temporelle alternée
9.3 Description d’ATS
10 Modélisation des protocoles
10.1 Prétraitement
10.2 ATS associé à un protocole
10.3 Un exemple
10.4 Propriétés de sécurité
11 Abstractions
11.1 Abstraction des ATS
11.2 Sémantique abstraite des énoncés ATL
11.3 Guide pour les abstractions
12 Sémantique abstraite des protocoles
12.1 Les agents, leur état local
12.2 Relations de transition locales
13 En pratique
13.1 Calcul des ATS abstraits
13.2 Vérification effective
13.3 Résultats
13.4 Conclusion
III Propriétés d’opacité
14 Introduction
14.1 Deux exemples
14.2 Approches existantes
14.3 Notre approche
15 Modélisation
15.1 L’équivalence par tests du spi-calcul
15.2 Les systèmes observables
15.3 L’observateur et les propriétés d’opacité
15.4 Abstractions
15.5 Un autre exemple : un protocole de vote
15.6 En conclusion
16 Relations de bisimilarité
16.1 Environnements
16.2 Bisimilarité contextuelle
16.3 h-bisimilarité contextuelle
16.4 h-bisimilarité gardée
16.5 Unification des différentes bisimilarités
16.6 Retour aux problèmes d’opacité
17 Utilisation de contraintes
17.1 Représentations d’un prédicat
17.2 Application à la simulation
18 En pratique
18.1 Le dîner des cryptographes
18.2 Le protocole de vote
18.3 Conclusion
Conclusion
Télécharger le rapport complet
