Sécurité des communications de groupe

30/08/2017
Publication REE REE 2006-6
OAI : oai:www.see.asso.fr:1301:2006-6:19708
DOI : You do not have permission to access embedded form.

Résumé

Sécurité des communications de groupe

Métriques

12
4
2.93 Mo
 application/pdf
bitcache://3197e09e3ce210e23c8e25585285758e64b6b932

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/1301:2006-6/19708</identifier><creators><creator><creatorName>Najah Chridi</creatorName></creator><creator><creatorName>Laurent Vigneron</creatorName></creator></creators><titles>
            <title>Sécurité des communications de groupe</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2017</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Wed 30 Aug 2017</date>
	    <date dateType="Updated">Wed 30 Aug 2017</date>
            <date dateType="Submitted">Sat 17 Feb 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">3197e09e3ce210e23c8e25585285758e64b6b932</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>33480</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

Dossier RISQUES ET SÉCURITÉ DES RÉSEAUX ET DES SYSTÈMES À COMPOSANTES LOGICIELLES (iele partio) m Sécurité des communications de groupe Najah CHRIDI, Laurent VIGNERON Laboratoire Lorrain de Recherche en Informatique et ses Applications (UMR 7503) Mots clés Sécurité descommunications, Protocolesdegroupe, Propriétés desécurité, Vérification 1. Contexte La mise en oeuvre de systèmes de sécurité assurant l'échange sécurisé de données est devenu un besoin indis- pensable pour permettre au réseau Internet (ou à tout autre réseau avec ou sans fil) de devenir un support sûr pour le développement d'activités professionnelles, com- merciales ou administratives. Comme la protection physi- que des voies de communication s'avère difficile à réali- ser, ces systèmes se fondent sur les techniques de crypto- graphie. Ainsi, pour assurer la confidentialité, l'intégrité et l'authentification des messages échangés, les protago- nistes doivent suivre un protocole très précis, appelé pro- tocole cryptographique ou protocole de sécurité. L'objectif de ces protocoles est d'assurer un moyen de communication sécurisée dans un réseau non protégé. Il faut savoir que sur tout réseau normal, une personne ayant accès au réseau peut intercepter des messages, retarder leur livraison, ou encore envoyer de faux messa- ges. Le but d'un tel intrus est en général d'acquérir une information confidentielle ou de prendre une fausse iden- tité, dans une transaction financière par exemple. La pré- sence des protocoles cryptographiques dans beaucoup d'applications importantes (connexion à un ordinateur distant, messagerie, etc.) fait de leur conception et de l'établissement de leur sécurité un but très important en recherche. Malheureusement, atteindre cet objectif paraît très difficile, puisque beaucoup de protocoles se sont avé- rés défectueux après plusieurs années de mise en service. Ainsi, il a été montré à la fin des années 1990 que la plu- part des protocoles utilisés dans les années 1980 n'étaient pas fiables à 100 %. Les failles de sécurité soulevées n'ont rien à voir avec des problèmes de cryptage d'infor- mations, comme par exemple " casser" des clefs de cryp- tage. Il s'agit en général d'une simple combinaison " mali- cieuse " des messages prévus par le protocole pour mettre en défaut la propriété que le protocole est censé garantir. Depuis une dizaine d'années, de nombreux travaux ont été effectués pour formaliser les protocoles de sécu- rité et les propriétés qu'ils assurent, dans le but d'obtenir des preuves formelles de leur correction. Ainsi, des méthodes de vérification ont été développées, et il existe de nos jours des logiciels'permettant aux concepteurs de protocoles, comme par exemple les sociétés membres de l'IETF [4], de vérifier au moins partiellement leurs " inventions ". Cependant, ces logiciels ne permettent pas encore de considérer toute sorte de protocole de sécurité, en particu- lier lorsque ceux-ci considèrent des domaines complexes. Les recherches en vérification s'orientent donc actuelle- ment vers ces protocoles extrêmement compliqués, comme par exemple les protocoles devant gérer les com- munications sécurisées au sein d'un groupe, via un réseau filaire ou hertzien. La première difficulté pour sécuriser ce type de communication est de distribuer à chaque membre du groupe la même clef de cryptage, qui servira à coder les messages envoyés au groupe, et aussi à déco- der les messages émis par les autres membres du groupe. La seconde difficulté, et non la moindre, est de gérer l'évolution du groupe, car de nouveaux éléments peuvent l'intégrer à tout moment, et d'autres peuvent le quitter. Il faut, par exemple, éviter qu'une personne quittant le 1 Par exemple, le logicielAVISPAestle fruit d'unecollaborationeuropéenneentrel'Allemagne, laFrance,l'Italie et la SuisseLn ESSENTIEL SYNOPSIS De plus en plus d'informations confidentielles circulant sur des réseaux filaires ou hertziens, leur sécurisation est devenue une préoccupationimportante. Danscet article,nousnousintéressons à la communicationde groupe,caren plusde protégerles messa- ges échangés,il faut gérer l'évolution des membres. More and more confidential information being sent on wire or wireless networks, their protection has become an important preoccupation.In this article, we considergroup communication, becausein additionto secureexchangedmessages,the dynamics of group membershiphasalso to be handled. REE No 6/7 .iuin/jiiillet 2006 Dossier RISQUES ET SÉCURITÉ DES RÉSEAUX ET DES SYSTÈMES À COMPOSANTES LOGICIELLES (l'ce partie) groupe puisse toujours décrypter les messages émis par les membres restants. Ainsi, la gestion de ces clefs, appelées " clefs de groupe ", demande la mise au point de protocoles satisfai- sant de nombreuses propriétés de sécurité. Un tel proto- cole a par exemple été mis au point dans le cadre du pro- jet RNRT SAFECAST [8], concernant les communica- tions sur des réseaux de radios mobiles privées. Etant donné des utilisateurs équipés de téléphones mobiles, il permet de sécuriser leur voix, ainsi que les transferts de données ou multimédia. L'objectif de cet article est de décrire précisément les propriétés que doivent respecter les protocoles conçus pour gérer les clefs de groupe. 2. Protocoles de groupe Un protocole de groupe est un protocole ou une suite de sous-protocoles pour l'établissement d'une clef secrète entre un nombre non fixé a priori de membres. Cela peut prendre la forme d'un établissement simple de clef, exé- cuté entre les membres, ou d'une série de requêtes pour joindre ou quitter le groupe avec les mises à jour asso- ciées à la clef. Pour assurer la communication au sein d'un groupe, les membres ont généralement recours à une clef secrète pour sécuriser leurs communications. L'opération la plus cruciale et la plus délicate dans ce type de protocoles est alors la gestion de clefs. La gestion de clefs joue un rôle important, imposant le contrôle d'ac- cès sur la clef de groupe, et par conséquent sur la commu- nication de groupe. Elle comprend l'établissement et l'en- tretien de clefs entre des parties selon une politique de sécurité imposée sur le groupe. Des protocoles dédiés à cette opération ont été et continuent d'être le sujet de nombreuses études de recherche. Parmi les approches de gestion de clefs, nous nous intéressons à une classe parti- culière : la classe des protocoles d'accord de clefs. Un protocole d'accord de clefs est un protocole permet- tant à un groupe de participants d'engendrer une clef basée sur leurs contributions et sans avoir à établir aupa- ravant une clef partagée initiale. La génération de la clef s'effectue par un simple échange de messages sur un réseau pouvant être sous le contrôle total d'un intrus. Ces échanges de messages renferment les contributions liées à la clef de groupe qui ne peut pas être déterminée à l'avance. La vérification de protocoles de groupe est confrontée à plusieurs problèmes. En effet, la sécurité des communi- cations au sein de groupes n'est pas nécessairement une extension d'une communication sécurisée entre deux par- ties. Elle est beaucoup plus compliquée. Une fois la com- munication commencée, le groupe peut changer de struc- ture en ajoutant ou en supprimant un ou plusieurs mem- bres. Les services de sécurité sont alors plus élaborés. En outre, les protocoles de groupe mettent en cause un nombre non borné de participants. Or, la plupart des approches automatisées de vérification de protocoles nécessitent un modèle concret. La taille du groupe doit alors être fixée à l'avance. Cette contrainte restreint consi- dérablement le nombre d'attaques détectables. Ensuite, vu que les besoins en sécurité sont généralement liés aux pro- tocoles, il est très difficile de décrire les propriétés que le protocole doit satisfaire. Cette phase de spécification des propriétés est critique : toute erreur (de compréhension ou de formalisation de ces propriétés) peut engendrer de faus- ses failles de sécurité. Des efforts ont été effectués pour une spécification des propriétés indépendamment des applications visées, à l'aide d'abstractions par exemple. Des langages formels ont également servi à définir des propriétés comme l'authentification : un message est accepté par un participant si et seulement si, il l'a effecti- vement demandé à un second participant, et si ce dernier le lui a bien envoyé. La définition et la spécification des propriétés de sécurité est donc un passage obligé très délicat, avant même d'entamer la vérification. La difficulté est d'autant plus grande lorsqu'il faut considérer des propriétés non standards, comme celles liées à la dynamicité des proto- coles de groupe. Ces propriétés de sécurité doivent suivre l'évolution du statut du groupe, et donc assurer la sécurité des membres appartenant au groupe, à un instant bien déterminé. Dans cet article, nous parcourons les travaux existants pour la vérification de protocoles de groupe. Ensuite, nous proposons un modèle pour les protocoles de groupe, et plus généralement pour les protocoles contribuants. Ce modèle permet de décrire un protocole contribuant, d'étudier ses caractéristiques et ses propriétés de sécurité, et donc d'identifier les différents types d'attaques possi- bles. Chaque notion introduite est suivie d'un exemple basé sur le protocole A-GDH.2. Nous mentionnons égale- ment les résultats de l'application de notre modèle sur d'autres protocoles. 3. Vérification des protocoles de groupe L'analyse de protocoles cryptographiques standards gérant deux ou trois parties a donné beaucoup de résultats intéressants. Ce domaine de recherche a été énormément exploité. Afin d'élargir la portée des techniques d'analyse, les chercheurs se sont orientés vers d'autres protocoles plus complexes : les protocoles de groupe. Diverses méthodes d'analyse ont été menées dans ce sens. Elles peuvent être classées en deux grandes catégories : les méthodes manuel- les et les méthodes automatiques. Avec une analyse manuelle, Pereira et Quisquater [7] ont par exemple pu trouver différentes attaques intéressan- tes dans la suite de protocoles CLIQUES [2]. La méthode proposée consiste à convertir le problème de possession REE No 6/7 Juin/juillet 2006 Sécurité des communications de groupe d'une information par l'intrus en un problème de résolu- tion d'un système d'équations linéaires. Dans les attaques ainsi découvertes, l'intrus peut avoir un comportement très libre ; par exemple, il peut utiliser des informations d'une session dans une session postérieure afin d'obtenir des secrets. D'autres travaux ont eu pour but d'obtenir un résultat générique : ils ont ainsi montré qu'il est impossi- ble de définir un protocole d'accord de clef authentifié basé sur les accords de A-GDH pour un nombre de parti- cipants supérieur à quatre. Des méthodes automatiques d'analyse de protocoles de groupe ont été intégrées dans divers outils. Taghdiri et Jackson [10] ont obtenu des résultats en modélisant un arrangement de gestion de clef en multicast. Ils ont for- malisé un modèle pour ce protocole, puis recherché des contre-exemples pour les propriétés de sécurité étudiées, en résolvant des problèmes de satisfaction de contraintes. Divers contre-exemples ont ainsi été trouvés ; le plus dan- gereux a été d'indiquer que les membres courants du groupe acceptent des messages valides diffusés par un membre antérieur de ce groupe. Taghdiri et Jackson ont proposé une version améliorée du protocole. Néanmoins, leur modèle formel de protocoles ne permettant pas de considérer qu'un intrus peut être actif, c'est-à-dire ne pas se contenter de lire les messages échangés, mais s'insérer et interagir dans ces échanges, ils n'ont pu détecter que leur version du protocole contenait deux attaques beau- coup plus dangereuses... L'outil CORAL [9] qui a fait cette découverte a également permis de découvrir des attaques dans le protocole Asokan-Ginzboorg [1], ainsi que dans le protocole de gestion de clef Iolus. D'autres travaux se sont focalisés sur la complexité de ces problèmes, due à l'exploitation d'un espace de recher- che d'attaque infini. En effet, avec les protocoles de groupe et pour une seule exécution normale, il faut consi- dérer un nombre illimité d'étapes possibles. Aussi, même si certains outils sont capables de considérer des protocoles de groupe, ils n'arrivent pas forcément à réaliser des étu- des complètes. Par exemple, NRL Protocol Analyzer est un outil capable de traiter la suite de protocoles GDOI (Group Domain Of Interpretation), mais il n'a pu retrou- ver les attaques de Pereira et Quisquater sur CLIQUES [5]. D'autres outils, comme MuCAPSL [6], ont permis de trouver des attaques sur des protocoles importants comme GDH.2, mais ils ont nécessité de figer certains paramètres comme par exemple le nombre de membres du groupe, ce qui est évidemment une contrainte très forte. La vérification de protocoles de groupe pose donc de sérieux problèmes, que ce soit pour traiter un nombre non borné de participants, ou encore pour définir formelle- ment les propriétés de sécurité qui doivent être satisfaites. La plupart des outils traitent seulement les propriétés de secret et, dans le meilleur des cas, la propriété d'authen- tification. 4. Un modèle pour les protocoles de groupe Comme tout protocole de communication, un proto- cole de groupe peut être vu comme un échange de messa- ges entre plusieurs participants. Cet échange est habituel- lement décrit par la liste des actions réalisées par chaque participant lors d'une exécution normale du protocole (exécution sans intervention d'un intrus). 4.1. Description du modèle Le modèle que nous proposons sert au départ à modé- liser un protocole de groupe. Il consiste à définir un sys- tème global de plusieurs composantes qui interagissent entre elles. Ainsi, un protocole de groupe peut être vu comme un système représenté par un triplet < A, K, S >, avec A : ensemble des membres du groupe, K : ensemble des connaissances des participants, S : ensemble des services. Nous désignons par service la contribution d'un parti- cipant pour engendrer la clef de groupe. La contribution d'un participant ai à un autre participant aj est toute infor- mation engendrée par ai, utile pour aj afin de déduire la clef de groupe. Notre modèle se base sur les définitions suivantes : . ai E A désigne le participant, . Si C est l'ensemble minimal des services utiles à ai pour construire la clef de groupe ; . Ki C K est l'ensemble des connaissances privées de . Il s'agit de l'ensemble minimal des connaissances utiles pour construire les services et la clef finale. Il inclut les connaissances privées au départ de la ses- sion ainsi que les informations engendrées au cours du déroulement de la session ; . Kij C K est l'ensemble des connaissances partagées entre les participants ai et aj. C'est l'ensemble mini- mal des connaissances partagées et utiles pour la génération de la clef de groupe. Ces informations sont données par la spécification du protocole. Il est à noter que Kij et Kji sont équivalents. En plus des services utiles pour engendrer la clef de groupe, on distingue d'autres sous-ensembles de services utilisés pour regrouper les services offerts par chaque par- ticipant. Ainsi, nous notons SOIle sous-ensemble de servi- ces auxquels ai a contribué (directement ou indirecte- ment) par l'utilisation d'informations privées (À ",). En résumé, notre modèle est donc basé sur un triplet < A, K, S >, décrivant que chaque participant ai possède des informations confidentielles (Â), partage des infor- mations (K,) avec d'autres participants, a besoin de REE W 6/7 Juin/juillet 2006 RISQUES ET SÉCURITÉ DES RÉSEAUX ET DES SYSTÈMES A COMPOSANTES LOGICIELLES (i& " partie) Trois personnes, Alice, Brice et Clara, souhaitent établir un groupe de communication sécurisée. Pour cela, ils ont besoin de concevoir une clef de groupe connue uniquement d'eux, qui servira à crypter et décrypter leurs messages. La mise au point de cette clef de groupe s'effectue par l'échange de quelques messages décrits ci-dessous, dans les- quels Alice, Brice et Clara vont devoir utiliser une clef secrète créée par chacun pour l'occasion (clef Alice, clef Brice, clef Clara), mais aussi des clefs partagées par plusieurs d'entre eux (clef Alice-Clara, clef Brice-Clara), <-llicc- B'i'c : re, rodc-r (cE; clf,,f.,v ;,f-) B'l'l, ('c - C"llTf2 : C'nflur'(Ct ('Îf'.Il3ritc'. (:O%l' (l/CIF,f--llice-).< "(Clrlllj ('.tal7n,o.Clf'.l3ri-ct r t1 \ Clfll'fl -'ri ('G!'Ç': (:Ofl(.1'-flf'%C.fNri :<.'lf.f ['lmu, (C'.f lli,r-C'Iu,nJ Cllbl'll -.-, ljf' (.f'C.: ('Ullf l'CfC'lf..l7ic.c.l'O,IC'lum, (:lf :,fyi,-r :-f.'lnra) Alice est l'initiatrice de ces échanges de messages. Elle envoie à Brice un message initial ( (x), qui sera utilisé comme brique de base pour la constitution de la clef de groupe. Elle transmet aussi à Brice ce message codé par sa clef secrète (clef A lice)' Brice, incapable de décoder cette deuxième partie du message, va cependant l'utiliser deux fois dans le message u clef secr'te. Il fait précéder ces deux parties du résul-qu'ilenvoie à Clara : telle quelle, puis codée par sa propre clef secrète. II fait précéder ces deux parties du résul-q tat du codage du message initial par sa clef secrète. Clara va utiliser les deux premières parties du message de Brice pour répondre à Alice et Brice. Elle transmet à Alice la première partie, coder (a/clef Brice), qu'elle code par sa clef privée et par la clef qu'elle partage avec Alice. Elle transmet à Bob la deuxième partie, coder (a/clef Alice), qu'elle code par sa clef privée et par la clef qu'elle partage avec Brice. Suite à cet échange de messages, chacun des trois participants est capable de composer la clef de groupe, qui cor- respond au codage du message initial par les trois clefs privées : coder (cIclefAli,e,clef 81-ice, clef clara). Pour cela, Clara n'a qu'à coder la dernière partie du message reçu de Brice par sa clef privée. Alice utilisera le message transmis par Clara : elle le décodera par leur clef commune clef Alice-Clara, puis le codera par sa clef privée. Brice suivra le même principe avec le message reçu de Clara. Ainsi, Alice, Brice et Clara ont réussi à calculer une clef qu'eux seuls connaissent, et qu'ils vont pouvoir utiliser pour crypter leurs communications, assurant la confidentialité des informations qu'ils vont échanger. Tableau 1. Le protocole A-GDH.2. connaissances () pour engendrer la clef de groupe et contribue (Si) à la génération de la clef pour les autres participants du groupe. 4.2. Caractéristiques du modèle Notre système est donc composé de trois ensembles de base A, K, et S, à partir desquels sont construits de nombreux autres ensembles ( KU, Si, Sa). La construc- tion de ces ensembles pour un protocole donné est assez simple, mais ils doivent cependant satisfaire quelques propriétés indispensables. Nous décrivons ci-dessous ces propriétés, qui concernent essentiellement les interactions entre ces différents ensembles. Ces caractéristiques seront ensuite illustrées par l'exemple de A-GDH.2. Unicité des identificateurs des participants. Les identi- tés des participants doivent être différentes. Visibilité des connaissances privées. Les connaissances dites " privées " des participants doivent être réellement confidentielles. Elles ne peuvent ni être partagées, ni être diffusées en clair dans un message. Visibilité des connaissances partagées. Les connaissan- ces partagées entre plusieurs participants sont en fait des connaissances confidentielles vis-à-vis des autres partici- pants. Chaque participant sait avec qui il partage des connaissances. Comme pour les connaissances privées, ces connaissances partagées ne doivent pas être transmi- ses en clair. Distinction des services utiles. Les ensembles des servi- ces nécessaires à la construction de la clef de groupe pour deux participants doivent être différenciés par au moins un élément. Indépendance des services utiles. Les ensembles de ser- vices nécessaires à la construction de la clef de groupe REE W 6/7 Juiii/juillet 2006 Afin de formaliser un peu plus notre exemple, remplaçons Alice, Brice et Clara par < a ?et a3 respectivement. Notons ri la clef privée de ai, et la ctcf partagée par ai et qj. Alors, coder (IclefB,i,,, clefcl,,i-Éi, ClefA lice- Clcii-Él) est représenté par 0.1-21--Ck,3. Le modèle obtenu pour la protocole A-GDH.2 est alors : A = lai, a2, a3l, K = Iri, r, r3, k 13 kl-31 s = C ('l c (I'l Ct'11*1 c (i*li*3k3 -a 5 1 1 1 (1) " 1'3ki31 Les informations relatives aux participants sont illustrées dans le tableau suivant : ai Si Sa, Ki UjKij a, () tl*11'3kl 3 (Y.1'15 Ui^li*3kl3 rl k 13 a, 0.1'11'3k2c 0.1'21 Ctl'ii « 2> Ul'il'3ki, r2 k23 a3 C ('l 1'2 Ctr2l--,kl,, CXI'11'3k3 r3 k 13, k23 Tableait 2. Modélisatioii du pi-otocole A-GDH. 2. pour deux participants ne doivent pas être liés par une relation d'inclusion. Correspondance des services. Tout élément de Si doit correspondre à un élément d'un .. Cela signifie que les services nécessaires à un participant ai pour construire la clef doivent provenir de contributions d'autres participants. Les caractéristiques définies précédemment concer- nent la construction des ensembles de connaissances et de services attachés aux participants. Ces informations sont utilisées par les participants pour construire la clef de groupe, notée K. Cette phase de déduction de KG, inter- venant à la fin de la session du protocole, doit également être contrôlée. Nous désignons par déduction l'applica- tion de certaines règles de composition et de décomposi- tion de messages. Il s'agit en général d'étapes de cryptage et de décryptage utilisant des connaissances initiales et acquises. Dans notre exemple, le cryptage s'effectue par exponentiation : s'' peut ainsi représenter de cryptage d'un service s par la clef-j. Le décryptage s'effectue par exponentiation par l'inverse d'une clef : (V) '' permet d'obtenir s. Ainsi, chaque participant sait quelle suite de déductions appliquer, et sur quelles connaissances, pour trouver la clef de groupe. C'est ce que nous appelons son algorithme, Alg. Déduction de la même clef de groupe. Pour un partici- pant ai5 la clef de groupe est engendrée en appliquant l'al- gorithme Algi aux connaissances privées et partagées, ainsi qu'aux services nécessaires de ce participant. Tous les membres du groupe doivent déduire la même clef. L'application de l'algorithme doit donc donner le même résultat pour tous les membres. Services minimaux. Un ensemble de services est dit minimal si l'accomplissement de l'objectif auquel il est destiné nécessite la participation de tous les éléments de l'ensemble. Dans le cadre de notre système, toutes les contributions doivent être utilisées pour la génération de la clef de groupe. Un participant ai ne peut pas se limiter à un sous-ensemble de Si pour construire la clef. Un participant ai doit donc avoir recours à tout l'ensem- ble Si en tenant compte de ses connaissances privées et partagées. Une conséquence est la propriété suivante : aucun élément de Si ne peut être déduit des autres élé- ments de cet ensemble. 4.3. Évolution dans le temps Le modèle que nous venons de présenter décrit un état stable du système. Il décrit comment une clef de groupe est engendrée à un instant précis par un protocole donné. Le procédé aboutissant à cette génération est représenté par les relations entre les différents ensembles de l'état du sys- tème < A, K, S >. Néanmoins, un groupe n'est en général pas stable au cours du temps. Il peut évoluer à la suite de différentes opérations telles que l'ajout, la suppression d'un membre ou d'un ensemble de membres. Le système n'a donc pas intérêt à se limiter à un seul état. L'évolution du système se traduit par la modification d'au moins une des trois composantes. Par exemple, l'ajout ou la suppres- sion d'un membre modifie l'ensemble A. Afin de prendre en compte cette dynamique du système, nous allons éten- dre le modèle proposé précédemment en introduisant la REE W6/7 Juin/juillet2006 Dossier RISQUES ET SÉCURITÉ DES RÉSEAUX ET DES SYSTÈMES A COMPOSANTES LOGICIELLES (ie'partie) Étudions chacune des caractéristiques pour le protocole A-GDH.2. 1. L'unicité des identificateurs des participants est vérifiée. 2. La caractéristique de visibilité des connaissances privées est vérifiée. En effet, les ensembles de connais- sances privées sont disjoints : r, n Ir, ? n r3' 0. Et d'autre part, aucune connaissance privée n'apparaît en clair dans un service. 3. La caractéristique de visibilité des connaissances partagées est vérifiée puisque k,3 U/K2, et k23 e Uj.Ki i De plus, kl3 et k ? -3n'apparaissent pas en clair dans un service. 4. Les propriétés de distinction de services utiles et d'indépendance des services utiles sont vérifiées car : SI n ns3 -s2ns3-o. 5. La caractéristique de correspondance de services est vérifiée pour les trois participants. En effet, - pour ai, SI C : S,,, et S, Sa3 - pour a2, S2 C : S (i) ; - pour a3, S3 C S,,, et S3 C : S,,,- 6. La caractéristique de déduction de la même clef de groupe est vérifiée. L'algorithme de calcul de cette clef du groupe pour chaque membre est : Al ! ji (t,,. (1, l'il. 1 : Al (i,). A, >. (.1!') !-'i,-, " "/'(1 1 -, 1, ; i, i ;, 1 1, : 1 1 J j 1 i,, ; i 1 -, i, > ; .,'''J' :;1 1, -', ; 11 111; 1 - i -, 1 A 1 ! 7 : - ( " 1 -' cTous les membres du groupe déduisent donc la même clef, 7. La caractéristique de services minimaux est vérifiée. En effet, pour les trois participants, l'ensemble Si est l'ensemble minimal à partir duquel la clef du groupe peut être engendrée. Tableaii 3. Vérificatioii des caracléi-istiqites du inodèle de A-GDH.2. notion de temps. Soit T l'ensemble (infini) des valeurs que peut prendre une horloge. Le modèle proposé auparavant ne représente que l'état observé à un instant T de T. Un état à l'instant T est donc le triplet constitué des participants, de leurs connaissances (privées ou publiques) et des services (nécessaires et contribuants) représentant le groupe à cet instant précis. Un groupe peut être vu alors comme étant l'ensemble des états pris à différents instants. GPT- < A, B, S >7- - < A7-1 B7-1 S7 " > ,,, J Le système global est donc donné par : Gp T = t Gp7, TI 4.3. 1. Ordre temporel. L'ensemble Test muni d'un ordre noté " <'\ Soient ret r' deux instants de T. L'influence du temps dans notre modèle peut être vue comme suit : Si T < i alors GJYT est un état qui précède temporellement GJYT'. Si T> T'alors GPT est un état qui suit temporellement GP. Si T= T'alors il s'agit du même état GPT. 4.3.2. Définition d'un événement. Le passage d'un état stable à un autre état se fait suite à des événements. On désigne par événement toute opéra- tion capable de modifier l'un des constituants de l'état du système. Dans le cadre de protocoles de groupe, un évé- nement peut être vu comme une opération d'ajout ou de suppression d'un membre du groupe, ou l'expiration d'un délai (par exemple pour un rafraîchissement de clef). Dans le cadre de notre modèle, un événement peut affec- ter l'ensemble des membres A (ajout ou élimination de participants), ou le sous-ensemble des connaissances pri- vées d'au moins un membre. Cette propriété peut s'expri- mer comme suit : REE W 6/7 Juiti/jtiiiici 2006 < A, K, S >7'ei,eiii < A, K, S >7j siona : ( " -7A7-') v (A " -A7-'A 3ai E A, KI-1 # KIl') Le rafraîchissement de clefs est un événement qui modi- fie les connaissances privées (comme par exemple le changement d'une clef privée ). 5. Formalisation des propriétés de sécurité Le but principal des protocoles d'accord de clef étant d'aboutir à une clef secrète commune, partagée entre les différents membres du groupe, les propriétés de sécurité ne s'intéressent plus seulement à la clef finale mais aussi aux différentes phases de gestion de cette clef Ces pha- ses sont étroitement liées à la dynamique du groupe (à la suite d'événements tels que l'ajout ou l'exclusion d'un membre). Nous distinguons dans cette section deux types de propriétés de sécurité. Cette distinction est basée sur l'in- dépendance ou la dépendance par rapport au temps. Pour pouvoir chercher des attaques dans un protocole donné, c'est-à-dire essayer de trouver des échanges de messages qui vont permettre de contredire une propriété supposée du protocole, nous avons besoin de définir le comporte- ment d'un intrus. Un agent malhonnête, ou intrbis, est soit un participant non officiel du protocole, soit un partici- pant officiel (ancien ou actuel membre du groupe) utili- sant sa position avantageuse pour perpétrer des actions malhonnêtes. Dans notre modèle, un intrus peut engendrer des actions laissant le système dans un état stable, comme par exemple accéder aux différents services offerts (U.iCAS,,i), ou bien intercepter ou modifier des messages échangés. Il peut aussi engendrer des actions provoquant un changement d'état comme l'envoi d'un message d'ini- tialisation d'une session du protocole. 5.1. Propriétés indépendantes du temps Il s'agit des propriétés de sécurité liées à un état sta- ble du système. Nous considérons ici l'état du groupe à un instant T. Le statut du groupe renferme donc l'ensem- ble des participants, leurs connaissances, qu'elles soient privées ou publiques, ainsi que leurs services, utiles et contribuants. Comme la clef du groupe est engendrée à partir d'informations collectées, et en suivant un point de vue particulier à chaque participant, les propriétés de sécurité portent sur les informations permettant d'engen- drer la clef, vues d'un ou plusieurs participants. Nous modélisons ci-après les propriétés d'authentification implicite de clef (une propriété liée à un participant ), de secret de la clef (concerne tout le groupe), de confirma- tion de clef (concerne deux participants) et d'intégrité (concerne tous les participants du groupe ainsi que tous les services utiles). Authentification implicite de la clef. Un protocole véri- fie la propriété d'authentification implicite de la clef de groupe si, à la fin de la session, chaque participant est assuré qu'aucun élément exteme ne peut acquérir sa vue de la clef de groupe. La vue d'un participant ai correspond à l'algorithme Alg, qu'il doit appliquer pour engendrer la clef de groupe, à l'aide des informations nécessaires (À U U. Kii). Un intrus (noté al) peut avoir une telle vue s'il peut la déduire grâce aux différentes informations qu'il possède ou peut récupérer (KI Uj Klj Uok EA J. Secret de la clef. Dans un état du système, seuls les mem- bres du groupe peuvent engendrer la clef partagée. Un agent externe al peut violer cette propriété en dédui- sant la clef du groupe à partir de ses connaissances acqui- ses ( U KIj UakEA Sak)'Étant donné que la clef du groupe peut être déduite à partir des informations d'un participant, la définition du secret de la clef correspond à une généralisation de la propriété d'authentification impli- cite de la clef à tous les participants. Confirmation de la clef. Dans le contexte de protocoles de groupe, il existe une propriété servant à convaincre une partie du groupe que les autres membres arrivent à engen- drer la clef partagée : la confirmation de la clef. Comme la seule possibilité pour un participant de pouvoir engendrer la clef est d'avoir les services nécessaires, la confirmation de clef revient alors à la confirmation de ces services. Pour qu'un participant confirme avoir engendré la clef, il doit montrer à chaque émetteur d'un service utile à la généra- tion de cette clef qu'il a reçu sa contribution. Intégrité de la clef. La propriété d'intégrité, quant à elle, permet de vérifier que tous les participants contribuent à la clef de groupe et que toute personne extérieure au groupe ne peut pas participer à la génération de cette clef. La première condition est vérifiée si l'ensemble des ser- vices Si de chaque participant ai résulte des contributions de tous les autres membres du groupe ; il s'agit donc de la confirmation de la clef et de la correspondance des ser- vices, présentées précédemment, appliquées à chaque participant. La deuxième condition peut être vérifiée si aucun élément de Si ne provient d'une partie extérieure au groupe. Sinon, il y a nécessairement un intrus qui a contribué à la géné- ration de la clef. 5.2. Propriétés liées à l'évolution du système dans le temps Dans un groupe, la notion de temps est fondamentale. REE No 6/7 Juin/juillet2006 Dossier RISQUES ET SÉCURITÉ DES RÉSEAUX ET DES SYSTÈMES A COMPOSANTES LOGICIELLES (ieepartie) Un groupe n'est pas stable dans le temps : à la suite d'événements tels qu'ajout ou sortie d'un membre, le sta- tut du groupe change. En changeant de statut, le groupe n'a plus les mêmes caractéristiques de sécurité. La clef doit suivre ce changement, et donc être mise à jour afin de n'être connue que par les membres effectifs du groupe. Par exemple, un membre qui appartenait auparavant au groupe et qui a été exclu peut avoir un comportement nui- sible en agissant malhonnêtement. Il ne doit donc plus pouvoir accéder aux communications du groupe. D'autre part. un nouveau venu dans le groupe ne doit pas pouvoir accéder à une communication passée. L'une des propriétés de sécurité temporelles les plus importantes est l'indépendance de clefs de grotipe. Elle garantit qu'aucun sous-ensemble de clefs ne peut être utilisé pour découvrir un autre sous-ensemble de clefs qui lui est disjoint. Il s'agit en fait de la combinai- son de deux propriétés de sécurité : le secret du futur (for- ward secrecy) et le secret du passé (backward secrecy). 5.2. 1. Secret du futur Cette propriété garantit qu'un adversaire passif qui connaît un certain nombre d'anciennes clefs de groupe ne peut pas découvrir une clef de groupe plus récente. Soit par exemple la séquence de clefs de groupe suivante : KGT, K 7G,.... o%u 71 < 7-1 <... < La propriété deG secret du ftillir exprime que, d'un sous-ensemble IK'i K,..., K}, l'intrus passif ne peut pas découvrir une clef de groupe KE telle que 7, > Ti'Selon notre modèle, pour pouvoir définir une telle propriété, il est nécessaire de revenir sur la définition de la propriété de Secret de la clef de groupe. En effet, le secret d'une clef de groupe est relatif à un instant donné : il est impossible (du point de vue calculatoire) de découvrir la clef à partir des informa- tions de l'instant. La définition de la propriété de secret du futur peut être raffinée, en décrivant les attaques qui peuvent être détectées. Protection contre une attaque par service connu. Un protocole est dit vulnérable à ce type d'attaque si la connaissance d'un service d'une session passée permet d'obtenir la vue d'un participant pour la clef d'une ses- sion future. Protection contre une attaque par clef connue. Un pro- tocole est dit vulnérable à ce type d'attaque si la connais- sance d'une clef à long terme d'un agent d'une session passée permet d'obtenir la vue d'un agent pour la clef d'une session future. 5.2.2. Secret du passé Cette deuxième propriété garantit qu'un intrus passif connaissant un sous-ensemble de clefs de groupe ordon- nées K,',, KI, KI, ne peut pas découvrir une clef deG G groupe précédente et cela pour tous l, i, j tels que tau, < taui < talli. 6. Détection de types d'attaques Notre modèle étant décrit, nous montrons ci-après les résultats obtenus lors de l'étude de quatre protocoles connus pour être défectueux. Nous avons modélisé ces '1'1 1 " ? 1'l >1 i'. ? (t. (1 (1. (,. (' - : > 1 --r2- al -(-Il et 1.. ./ 1 r2 (11,1/rr// et (l, i'l 1'2 1 1'l 1'2 t'l Tableau 4. Scénario d'attaque dA-GDH.2. REE W 6/7 Juin/juillet2006 Sécurité des communications de groupe protocoles, leurs propriétés, puis identifié les types d'at- taques auxquelles ils sont vulnérables. Pour notre étude, nous nous sommes basés sur des scénarios d'attaques. La modélisation d'une exécution de protocole nous a permis de tester une à une les caractéris- tiques ainsi que les propriétés définies dans notre modèle. Il est à noter que même à partir d'une seule phase d'un scénario d'attaque, nous avons pu détecter plusieurs pro- priétés de sécurité non vérifiées. Par exemple, c'est le cas avec le scénario d'attaque illustré ci-dessous, qui concerne A-GDH.2 avec quatre participants dont le troi- sième est malhonnête, et représenté par l'intrus al : il va substituer la deuxième partie du message qu'il émet, (xril ", par ann, ce qui va changer la seconde partie du message émis par a4 et fausser la vue de a2 sur la clé. La modélisation de ce scénario est la suivante : Protocole A-GDH.2 SA-GDH.2 Asokan- Ginzboorg Eiresson- Chevassut- Essiari- Pointcheval Caractéristiques nonvérifiées Déductionde la même clef de groupe Déductionde la même clef de groupe Déductionde la même clef de groupe Correspondance deservices Propriétés non vérifiées Authentificationimplicite ; secretde la clef ; confirmationde la clef ; intégrité Authentificationimplicite ; secretde la clef ; secretdu futur (attaqueparserviceconnu) Authentification implicite Secretdu futur (attaquespar serviceconnuet parclef connue) Tableau 5. Analyse de protocoles. ai Si 1 D. ai K 1 t J- UjKij 'r ! 7r I r 4T-1-4 al a4 a Q ; ,rir2'fl ot1 T1T2 T1T2TJa'r, 11 ce T'l jr2 a'r'lr'2 T » I Tl () Z r 1/r2'Ï'I 1 y CË'Îlr21,,4k2-1 et r2,t,i,r4 k, 4 ce'Î'l 72 74 k 14 1 a 1'l r2 r4.. re a > 7'l r4k,,,r2r74-i4 k 14 T-1-4/4 jT'2r4'241 a'r 1'F'2'1'4 K,'14. a7'2 T*4 K.'24 1 1 a2 a rl r2t*4 A24 a T'2 ce'I'l T'2 a T&2r'l1 r2 k24 () Z r 1/r2'Ï'I1 a. a, CË'Îl r2 1,,4 k2-1 et r2,r,i,r4k,-, 1 r3 kl4j k241 A partir de ces informations, nous déduisons que la caractéristique Déduction de la même clef de groupe n'est pas satisfaite. En effet, les vues de clef de al et de a2 ne convergent pas vers la même clef Les algorithmes de construction de la clef de groupe étant définis par : (} (12) 1/A : 14 rtr-Â'. A192 (1'2 l ( 1'l 1 2 1 1 A>) 4 ( 1 l'Ji [> >,I) -i1 h >,l 2/t,, 4 g 1 (1',l 1 ( 7 L i>,7 1 (t'. ) 1-1 al et a4 vont bien construire la même Clef Ctrl " 2rl " 4, alors que a2 va construire laclef Ctrlr2r2l'4. Si nous étudions maintenant la propriété de sécurité authentification implicite, l'intrus a, peut avoir la même vue que a4. Grâce aux informations qu'il possède ( et k,4), l'intrus utilise le service offertarlr2r4kl4pour déduire la vue de a4, en calculant ot (I'l r2r3kl3) *rIlkI3 7. Conclusion Nous avons présenté une étude qui s'applique aux protocoles de groupe, et plus généralement aux protoco- les contribuants. Elle permet de modéliser les protocoles eux-mêmes, mais surtout de décrire formellement leurs caractéristiques et les propriétés de sécurité qu'ils doivent considérer. Cette formalisation permet d'éviter toute ambiguïté sur la définition des problèmes de sécurité posés, et donc de garantir que les recherches de failles s'effectuent sur de bonnes bases. Ainsi, les failles trou- vées seront effectives. Nous avons brièvement illustré ces travaux sur quatre protocoles connus, mais non triviaux. Le traitement d'un grand nombre de protocoles passe par l'implantation de méthodes automatiques d'analyse des propriétés définies. Pour cela, nous allons utiliser le logiciel AVISPA [3] : son puissant langage de spécification de protocoles per- REE No 6/7 Juin/juillet 2006 Dossier RISQUES ET SÉCURITÉ DES RÉSEAUX ET DES SYSTÈMES 1 À COMPOSANTES LOGICIELLES (l' " partie) mettra (modulo quelques extensions) de décrire sans grande difficulté les protocoles contribuants ; les proprié- tés à vérifier pourront également être décrites grâce au langage intégré, basé sur un fragment de la logique tem- porelle LTL. L'outil de vérification AtSé intégré dans ce logiciel devra également être étendu pour traiter ces pro- priétés si particulières, comparées aux propriétés stan- dards de secret et d'authentification. Le travail présenté dans cet article est réalisé dans le cadre de différentes collaborations scientifiques et indus- trielles, avec pour objectif principal de sécuriser les com- munications sur des réseaux non protégés, comme nous en effectuons tous les jours rien qu'en utilisant Internet. Références [1] N. ASOKAN et P GINZBOORG. " Key agreement in ad hoc networks " Computer Communications, 23 (17) : 1627-1637, 2000. [2] G. ATENIESE, M. STEINER. et G. TSUDIK. " New Multiparty Authentication Services and Key Agreement Protocols ", IEEE Journal on Selected Areas in Communications, 18 (4) : 628- 639,2000. [3] AVISPA. "A Tool for Automated Validation of Internet Security Protocols ; by DIST (Genova, Italy), INRIA Lorraine (Nancy, France), ETHZ (Zurich, Switzerland)' ; Siemens (Munich, Germany), 2005. http ://www.avispa-project.org. [4] ETF.The ! nternet Engineering Task Force. http ://www.ietf.org. [5] C. MEADOWS. " Extending Formai Cryptographic Protocol Analysis Techniques for Group Protocols and Low-Level Cryptographic Primitives ", ln Proc. of the Ist Workshop on Issues in the Theory of Security, pages 87-92, Geneva, Switzerland, 2000. [61 J. MILLEN et G. DENKER. " MuCAPSL',' In DARPA InformationSurvivability Conference and Exposition, pages 238-249. IEEE Computer Society, 2003. [7] 0. PEREIRA et J.-J. QUISQUATER. " Some Attacks Upon Authenticated Group Key Agreement ", Protocols. Journal of Computer Security, 11 (4) : 555-580, 2003 18] SAFECAS. Sécurité des communications de groupe. http ://www.te ecom.grouv.fr/rnrt/rnrt/projets/safecast.htm. [91 G. STEE et A. BUNDY, "Attacking Group Multicast Key Management Protocols using CORAL'. In Proc. of the Workshop on Automated Reasoning for Secun/Proroco/ Analysis, volume 125 :1 of ENTCS, pages 125-144, 2004. [10] M. TAGHDIRI et D. JACKSON. "A Lighteweight Formal Analysis of a Multicast Key Management Scheme'.'In Formal Techniques for Networked and Distributed Systems, volume 2767 of LNCS, pages 240-256, Berlin, Germany, 2003. Springer. Les auteurs Najah Chridi, après des études en Master à L'Ecole Nationale de Sciences de informatique deTunis, et un DEA obtenu à l'Université Henri Poincaré (Nancy), prépare actuellement un Doctorat en infor- matique au LORIA (Laboratoire Lorrain de Recherche en Informatique et ses Applications). Ses travaux portent sur l'analyse des communications sécurisées au sein de groupes. Laurent Vigneron est enseignant-chercheur à l'Université Nancy 2, et membre du LORIA (Laboratoire Lorrain de Recherche en Informatique et ses Applications). Ses activités de recherche concernent principalement la définition et l'Implantation de métho- des formelles permettant d'étudier les problèmes de sécurité de communications. II s'intéresse à l'analyse de ces problèmes au niveau logique, et non pas au niveau technique. REE W 6/7 Juin/jiiillet 2006