Modélisation et vérification de protocoles pour des communications sécurisées de groupes

Des systèmes de communication de groupes sécurisés 

Les nouvelles générations d’utilisateurs intègrent aujourd’hui dans leur vie quotidienne l’informatique comme un moyen pour accéder à autres services et comme un outil pour communiquer avec d’autres personnes. La vente et l’achat de biens par internet se popularisent. Les outils et les forums de dialogue dans des espaces réels ou virtuels sont de plus en plus couramment utilisés. Avec cette évolution, la communication de groupes est un moyen d’échange dont les applications ont de plus en plus besoin. Dans notre monde actuel, l’évolution des systèmes informatiques a fait de la communication de groupes une technique nécessaire et très utilisée dans différents domaines. Par exemple, dans le monde des jeux informatiques, il existe une gamme des jeux basée sur la participation d’un ensemble d’utilisateurs distribués physiquement dans des endroits différents. L’idée de mettre « ensemble » un groupe de personnes de façon virtuelle pour partager un temps d’amusement informatique implique, en arrière plan, la mise à disposition d’une plateforme de communication multipoint fiable. Avec ceci, l’industrie du jeu induit une évolution et une modernisation des autres technologies, y compris la communication de groupes.

Eléments d’un système de communication de groupes

Dans une application de groupes où la communication entre ses membres prend un rôle important, nous pouvons observer qu’il existe communément deux types d’information à échanger [LIV 2.5] : 1). L’information concernant l’application et 2). L’information concernant le bon déroulement de cette communication. Puisque les messages à échanger par l’application, dits « messages de données », doivent être sécurisés, nous avons besoin des éléments, dits « éléments secrets », qui serviront de base pour sécuriser cette information. Et puisque ces éléments risquent d’être changés, afin de maintenir leur sécurité tout au long d’une session active, nous aurons aussi besoin de messages, dits « messages de contrôle » qui serviront principalement à l’actualisation des éléments secrets. En effet, dans la communication de groupes, nous devons à la fois assurer les tâches de communication intrinsèque de l’application, et effectuer le contrôle du protocole de communication.

Si nous considérons qu’il existe un seul canal de communication dans le groupe (ce qui peut se passer dans le pire des cas) nous aurons donc intérêt à optimiser l’utilisation du médium pour le transport des messages de données. Pour cela, plusieurs travaux de recherche [BAN 02], [WAN 05] portent leurs efforts sur la diminution du trafic de contrôle nécessaire au fonctionnement du protocole de communication, de façon à ne pas affecter les temps de réponse attendus par l’application. Cette première exigence, qui intervient très fortement dans la définition d’un système des groupes, correspond aux contraintes temporelles ou bien de performance établies lors de l’étape d’analyse de ce système. Souvent, dans un ensemble de groupes, les supports réseaux dont les nœuds disposent deviennent aussi un facteur important. La disponibilité et la robustes des ressources réseaux sont deux paramètres qui permettent de restreindre plus ou moins les processus de contrôle impliqués dans la communication. La composition des groupes liés par cette communication, ainsi que l’évolution de cette composition, est un paramètre déterminant pour les choix des mécanismes de protection de l’information échangée et des techniques d’actualisation des éléments secrets dont les mécanismes de protection ont besoin. Le choix des techniques pour la gestion des groupes se verra aussi affecté par cette composition et cette dynamique des membres. En ce qui concerne l’application, le terme sécurité est pris en compte comme une personnalisation des communications de groupes. Protéger contre tout type d’attaque la communication d’un groupe de membres n’est pas forcément synonyme d’efficacité. Offrir un système plus rapide et plus performant que les autres n’est pas, non plus la meilleure solution si aucune sécurité n’est garantie. Il est évident que la sécurité dans la communication joue aujourd’hui un rôle autour duquel les autres paramètres doivent souvent s’ajuster. Nous devons aussi prendre en compte que le niveau de sécurité peut varier selon l’application concernée.

Des solutions pour la communication des groupes 

C’est en 1976 que l’équipe composée par Diffie, Hellman et Merkle [DIF 76], [MER 78], [HEL 02] établit la technique de chiffrement de donnés « DiffieHellman » (DH), qui révolutionnera le concept des anciens systèmes pour la protection des données. Cette technique est maintenant la base de plusieurs systèmes, notamment dans le domaine de la communication de groupes. L’idée de cette technique est de faire contribuer totalement ou partiellement chacun des membres dans une session active pour la génération des éléments de base qui seront ensuite utilisés par les techniques de chiffrement nécessaires à la communication. A l’origine « Diffie-Hellman » établit un secret utilisé pour chiffrer et déchiffrer l’information échangée entre deux membres. En reprenant cet algorithme, [ING 82] l’adapte à des groupes, puis l’utilise dans des conférences multiutilisateurs (Conference Key Distribution System CKDS). D’autres extensions pour des groupes sont présentées dans [STE 90], [BUR 94], [STE 96], [STE 97], [STE 00], [ASO 00]. Avec l’apparition de grands réseaux et en ayant à l’esprit l’idée de minimiser le temps de traitement de la gestion du groupe, dans [MIT 97], [MOL 00] et [DU 99] les auteurs se basent sur la structure hiérarchique du groupe pour proposer un algorithme qui délègue le calcul de la clé aux nœuds composant le réseau. En étudiant la même problématique de gestion des éléments secrets, nous trouvons des travaux qui utilisent des arbres pour la génération de clés : [WAL 98], [CAR 98], [NOU 98], [WON 98], [SHE 03], [CAN 99a], [DON 99a], [DON 99b], [DON 00], [KIM 00], [KIM 04a] et [ZOU 04]. Dans [BAN 02], l’utilisation de clusters représente aussi une bonne solution pour diminuer la charge de gestion de ces éléments secrets. Les certificats sont aussi des éléments très utilisés dans le domaine de la communication de groupes. Dans [LIV 2.2], [LIV 2.3] et [LIV 2.4], les auteurs font une étude très complète qui concerne les certificats appliqués à la communication des groupes. En suivant une autre direction, plus focalisés sur les services de gestion des groupes, les auteurs [BIR 90], [WHE 94], [DOL 96], et [MOS 95] cherchent à garantir la fiabilité des systèmes distribués en considérant principalement la tolérance aux fautes, l’ordonnancement des messages, la synchronisation dans la communication, etc. Des services pour la gestion des utilisateurs comme le join ou le leave sont ici inclus. [REI 95], [KIH 98], [REN 96], [BIR 97] traitent, eux de leur côté, deux sujets innovants et importants, le premier traitant la sécurité dans la communication et le deuxième référant l’utilisation d’un système complet. Pour finir, nous avons identifié un ensemble de travaux dont l’intérêt a été de répondre aux besoins des nouvelles technologies et des nouvelles techniques de développement des systèmes logiciels. Ainsi dans [HIL 97], [HIL 00], [GON  96], [McD 00], [IRR 03] et [AMI 05], les auteurs proposent des architectures liées à des plates-formes middleware, mises à la disposition des applications sous la forme d’entités micro protocolaires pour la communication des groupes avec des interfaces faciles d’utilisation. La possibilité que les applications puissent fabriquer leurs propres services, l’évolution dans la proposition d’architectures globales, et l’utilisation de nouvelles techniques dans le domaine de la sécurisation de la communication font partie des avancées apportées au domaine de la communication des groupes sécurisés. De façon plus précise, leurs travaux traitent la problématique du bon compromis entre le niveau de sécurité choisi (authentification, confidentialité et intégrité de la communication, protection contre le rejeu et la collusion, etc.) et la performance du système de communication.

L’ensemble de problématiques traitées dans la communication des groupes est tellement vaste qu’il a été impossible d’identifier un groupe ou un travail qui traite, dans son ensemble et au même niveau, l’ensemble des axes auxquels nous nous sommes intéressés.

Contributions apportées dans ce mémoire

La proposition d’une architecture pour un système de communication de groupes sécurisés, sa modélisation et sa vérification représentent une tâche hautement complexe. Notre intérêt a été d’instancier dans un cas réel une architecture proposée dans le cadre de ce mémoire et de montrer l’intérêt de l’application d’une méthodologie incrémentale de conception dans le cas d’architectures aussi complexes. L’objet final a été de montrer, avec la vérification de ce système, que le protocole de communication choisi satisfait les exigences établies à l’origine de sa définition. Le travail présenté dans cette thèse intègre dans son architecture un ensemble représentatif des problématiques qui se présentent dans la communication de groupes sécurisés.

Nous présentons ci-dessous l’ensemble des apports de ce mémoire.
• Analyser des systèmes de communication de groupes en utilisant le profil UML 2.0 pour la définition des fonctionnalités intrinsèques de tels systèmes Nous avons choisi de suivre une méthodologie [MOT 05], [MOT 06], [FON 06] qui nous aide à l’identification des fonctionnalités d’un protocole de communication de groupes mais aussi à l’implantation du modèle. Ainsi, en se basant sur certains diagrammes de la notation Unified Modeling Language (UML) 2.0, nous analysons et documentons les composants d’un protocole de communication de groupes. Les résultats de cette analyse peuvent servir à l’établissement de standards pour l’analyse et la définition de tels systèmes.
• Proposer une architecture de modélisation et de vérification de protocoles pour la communication sécurisée de groupes Nous proposons l’architecture générique appelée SGCva (Secure Group Communication verification architecture) [MOT 06] [MOT 07], qui peut être utilisée dans différents contextes pour des protocoles de communication de groupes. Sa définition s’appuie sur les fonctionnalités précédemment identifiées dans ce type de communications. Le modèle de référence OSI (Open System Interconnection) [TAN 96] que nous considérons comme un cadre conceptuel adéquat pour concevoir les services et les protocoles de communications des systèmes distribués, a été la référence pour la structuration de notre architecture en couches. Les niveaux de déploiement de notre architecture s’inscrivent dans les couches hautes du modèle OSI, c.à.d. dans les couches Application, Session et Transport du modèle OSI. Globalement, nous proposons d’implémenter dans notre architecture les services concernés par : 1). Le transport sécurisé de l’information échangée entre les membres d’une session. 2). La gestion de la communication des groupes sécurisés. 3). La gestion du groupe. 4). L’application finale.
• Définir des primitives et des services pour des communications sécurisées de groupes L’identification des primitives de communication entre les couches d’une entité réseau implique un travail d’abstraction complexe. L’objet est de réussir à énumérer de façon exhaustive toutes les possibilités de dialogues entre les services des couches dans l’architecture. Nous avons identifié, tout d’abord, toutes les interactions existantes entre des couches. Puis, nous avons défini l’ensemble des échanges qui se déroulent entre les couches pour arriver, à la fin, à l’identification des primitives pour chaque couche. Un travail équivalent a été fait pour l’identification des « Unités de Données de Protocole » (PDUs), unités de données échangées entre entités équivalentes au sein d’une même couche réseau.
• Instancier notre architecture à travers une méthodologie incrémentale dans un projet industriel Le projet RNRT SAFECAST, dédié à l’étude, à la conception et à la validation de fonctionnalités de mécanismes garants de communications sécurisées à l’intérieur de groupes dynamiques [EAD 04], [SAFECAST], représente un cas réel et complexe de l’application d’un protocole sécurisé dans des communications de groupes. A travers l’application d’une méthodologie incrémentale [MOT 05], [MOT 06] de modélisation et de vérification, nous avons instancié notre architecture dans une modélisation du protocole Safecast [LIV 2.5] sous un environnement TURTLE [TURTLE]. Des résultats concernant la satisfaction ou la non satisfaction des exigences temporelles ont été fournis aux partenaires du projet. Notre contribution aux biens livrables de projet se trouve dans [LIV 2.5], [LIV 3.4], [LIV 4.1], [LIV 4.2], [LIV 4.3] et [LIV 4.4].
• Définir une nouvelle technique d’analyse de protocoles de groupes sécurisés Une contribution originale dans un tel domaine a été le fait de proposer une solution dont les qualités (fonctionnelles et de performances) auront été démontrées par des techniques de validation formelle. Le grand problème qui s’est posé, et qui à notre connaissance n’avait jamais été abordé, a porté sur la nécessité de traiter en même temps des problématiques qui, du point de vue de la modélisation et de la vérification formelle, avaient été adressées séparément dans la littérature, à savoir:

(1) la sécurité dans la communication ;
(2) la gestion de groupes dynamiques ;
(3) les contraintes temporelles.

Par rapport à ces trois problèmes de base, nous ajoutons plusieurs spécificités parmi lesquelles :

(4) des groupes régis selon une organisation hiérarchique de ses membres ;
(5) la combinaison étroite entre les exigences de sécurité et les exigences temporelles.

Le travail développé dans cette thèse ouvre des possibilités pour une nouvelle technique d’analyse des performances des protocoles de communication de groupes à travers une étude temporelle de ses fonctionnalités et de l’impact du renforcement de la sécurité vis-à-vis des performances effectives du protocole.

Le rapport de stage ou le pfe est un document d’analyse, de synthèse et d’évaluation de votre apprentissage, c’est pour cela chatpfe.com propose le téléchargement des modèles complet de projet de fin d’étude, rapport de stage, mémoire, pfe, thèse, pour connaître la méthodologie à avoir et savoir comment construire les parties d’un projet de fin d’étude.

Table des matières

1 Introduction
1.1. Des systèmes de communication de groupes sécurisés
1.2. Eléments d’un système de communication de groupes
1.3. Des solutions pour la communication des groupes
1.4. Contributions apportées dans ce mémoire
1.5. Organisation du mémoire
2 Etat de l’art
2.1. Introduction
2.2. Principaux éléments pour la sécurisation des communications
2.2.1. Cryptographie à clé publique
2.2.2. Cryptographie à clé secrète
2.2.3. Certificats
2.2.4. Autres mécanismes pour des systèmes particuliers/spécifiques
2.3. Architectures pour la communication des groupes
2.3.1. Premières architectures pour la communication de groupes
2.3.2. Architectures pour la communication des groupes sécurisées
2.3.3. Synthèse
2.4. Conclusion
3 Spécification des fonctionnalités pour des communications de groupes sécurisés
3.1. Introduction
3.2. Outils d’analyse et de modélisation
3.2.1. Unified Modeling Language 2.0
3.2.2. Diagrammes de Contexte (Context Diagram)
3.3. Structure des groupes
3.3.1. Dimensions dans un groupe
3.3.2. Notion de rôle des utilisateurs dans un groupe
3.4. Fonctionnalités pour la gestion des groupes
3.4.1. Composition interne des groupes
3.4.2. Gestion de la connectivité entre des groupes
3.5. Fonctionnalités pour la gestion de la communication des groupes
3.5.1. Confidentialité de communication à l’intérieur de chaque groupe, utilisation de clés de session par groupe
3.5.2. Confidentialité des communications à l’intérieur de chaque classe
3.5.3. Gestion de la clé de session
3.6. Fonctionnalités pour la transmission sécurisée
3.6.1. Transmission de messages
3.6.2. Protection des échanges
3.7. Récapitulatif des fonctionnalités
3.8. Conclusion
4 Architecture pour des communications de groupes sécurisés
4.1. Introduction
4.2. Architecture proposée
4.3. Couche Transport sécurisée
4.3.1. Primitives de service de la couche transport sécurisée
4.3.2. Sous-couche Médium
4.3.3. Sous-couche Operations élémentaires de sécurisation des échanges (Security Opérations SO)
4.4. Couche Session
4.4.1. Sous-couche de Gestion de la Communication des Groupes (Group Communication Key Management GCKM)
4.4.2. Sous-couche de gestion des groupes (Group Membership Management GMM)
4.5. Conclusion
5 Spécification, modélisation et vérification du protocole
5.1. Introduction
5.2. Projet SAFECAST
5.2.1. Description du projet SAFECAST
5.2.2. Technologie sous-jacente : TETRA et TETRAPOL
5.2.3. Description de l’application SAFECAST
5.3. Approche d’analyse des protocoles de communication de groupes
5.3.1. Méthodologie de modélisation des protocoles de communication
5.3.2. Outil TURTLE
5.3.3. Vérification d’un protocole de communication
5.3.4. Vérification temporelle
5.4. Modélisation et résultats de vérification du protocole SAFECAST
5.4.1. Modélisation du protocole
5.4.2. Présentation des résultats
5.5. Conclusion
6 Conclusion

Lire le rapport complet

Télécharger aussi :

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *