Présentation
En anglaisRÉSUMÉ
La démarche qualité/fiabilité n'est pas aussi exigeante en informatique que dans des domaines comme la mécanique. Toutefois dans des domaines tels que l’aérospatiale ou la sécurité de l’information, la qualité, la fiabilité et la sécurité priment dans tous les projets informatiques. Le projet européen AVISPA est dédié au développement de techniques de validation de protocoles de sécurité afin de les rendre disponibles simplement aux ingénieurs développant ces protocoles. Le double enjeu était d'être à la fois performant dans cette validation et de mettre ces performances à la portée de non-spécialistes.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleABSTRACT
The quality/reliability approach is not as demanding in computing as in domains such as mechanics. However, in sectors such as the aerospace industry or information safety, quality, reliability and safety are paramount in every computing project. The European project AVISPA is dedicated to the development of validation techniques for safety protocols in order to make them available to the engineers who develop such protocols. The dual objective was to develop efficient validation and provide access to these performances to non-specialists.
INTRODUCTION
Le projet européen AVISPA est dédié au développement de techniques de validation de protocoles de sécurité afin de les rendre disponibles simplement aux ingénieurs développant ces protocoles. Le double enjeu était d'être à la fois performant dans cette validation et de mettre ces performances à la portée de non-spécialistes.
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Réseaux Télécommunications
(139 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
5. TA4SP
Avant de décrire plus avant la méthode utilisée dans TA4SP, il faut savoir que si l'on ne borne pas le nombre de sessions d'un protocole pouvant s'exécuter en parallèle, savoir si ce protocole est sensible aux attaques de type man in the middle est indécidable, c'est-à-dire qu'il n'est pas possible de réaliser un programme qui prend en entrée la description d'un protocole de sécurité et qui donne à chaque fois une analyse de ce protocole. Pour revenir à un cas décidable, c'est-à-dire réalisable à tous les coups par une machine, il est nécessaire de faire certaines restrictions ou hypothèses. La plus courante est de borner le nombre de sessions du protocole pouvant s'exécuter en parallèle, généralement à deux ou trois. Cela se justifie a posteriori par le fait que presque toutes les failles connues sur les protocoles n'utilisent que deux sessions (ou très rarement trois). Même avec ces hypothèses, le problème est plus complexe qu'il n'y paraît et demande le développement d'algorithmes dédiés. Les trois premiers outils d'AVISPA, OFMC, CL-ATSE et SATMC utilisent une restriction du nombre des sessions, ce qui n'est pas le cas de TA4SP.
La figure 7 illustre la situation. Initialement, un intrus dispose de connaissances simples, en général l'identité des personnes qu'il espionne, leurs clés publiques ainsi que ses clés privés, publiques et secrètes. Ces connaissances sont matérialisées en gris clair sur la figure. Ce que l'on a représenté en gris foncé constitue l'ensemble des connaissances auxquelles l'intrus peut accéder en jouant plusieurs sessions du protocole avec les différentes personnes du réseau. Il a été démontré qu'on ne pouvait en général pas calculer exactement cet ensemble gris foncé, c'est-à-dire qu'on ne peut pas en donner une description finie. L'approche consiste donc à calculer un ensemble de connaissances plus important que l"ensemble gris foncé Accessibles, il s'agit de l'ensemble marron Approximées sur la figure 7.
La question de la sûreté du protocole se résume à celle-ci : l'intersection entre les ensembles Approximées et Secrets est-elle vide? Si oui, le protocole est sûr, sinon il a une faille (l'intrus a accès à un secret). Mais comme on ne peut pas calculer l'ensemble Accessibles, on calcule l'intersection entre l'ensemble Approximées et l'ensemble Secrets. Si elle est vide alors, a fortiori celle entre...
Cet article fait partie de l’offre
Réseaux Télécommunications
(139 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
TA4SP
BIBLIOGRAPHIE
-
(1) - MANICORE (J.-M.) - Bénéfices environnementaux envisageables liés à l'introduction du télétravail - . Ministère de l'Industrie (2001). http://www.manicore.com/documentation/teletravail/OSI_synthese.html
-
(2) - RIVEST (R.L.), SHAMIR (A.), ADLEMAN (L.M.) - A method for obtaining digital signatures and public key cryptosystems - . Communications of the ACM, 21, 120-126 (1978).
-
(3) - NEEDHAM (R.), SCHROEDER (M.) - Using encryption for authentication in large networks of computers - . Communication of the ACM, 21 (12), 993-999 (1978).
-
(4) - LOWE (G.) - Breaking and fixing the Needham-Schroeder public-key protocol using FDR - . In (T.) Margaria et (B.) Steffen (éd.), Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), vol. 1055 of LNCS, 147-166. Springer-Verlag (1996).
-
(5) - The AVISPA team - HLPSL Tutorial. A Beginner's Guide to Modelling and Analysing Internet Security Protocols - . AVISPA (2006). http://www.avispa-project.org/package/tutorial.pdf
-
...
Cet article fait partie de l’offre
Réseaux Télécommunications
(139 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive