Nos amis les profs

SPORE : une bibliothèque publique de protocoles cryptographiques

Participants : Florent Jacquemard [correspondant], Ralf Treinen, Hubert Comon-Lundh, Alexandre Boisseau, Véronique Cortier, (liste non limitative).

SPORE est une page Web disponible en http://www.lsv.ens-cachan.fr/spore/. Son but est de fournir une bibliothèque publique de protocoles cryptographiques, leurs différentes versions, les propriétés de sécurité qu'ils sont censés vérifier, celles qu'ils vérifient effectivement et sous quelles hypothèses, les attaques connues contre ces protocoles.

SPORE contient en particulier une liste de protocoles cryptographiques identifiés par Trusted Logic S.A. dans le cadre du projet EVA.

Une bibliothèque similaire avait été publiée en 1997 par John Clark et Jeremy Jacob (University of York), dans la seconde partie d'un survol très largement diffusé dans la communauté de la vérification de protocoles cryptographiques. En particulier, leur bibliothèque a souvent servi de base de cas d'étude pour les concepteurs d'outils de vérification automatique de protocoles.

Le but de la page SPORE est de poursuivre l'effort de Clark et de Jacob, d'une part par une mise à jour des protocoles que l'on trouve dans leur survol, et d'autre part avec l'ajout de nouvelles entrées, l'ensemble de la bibliothèque étant accessible en ligne, afin d'assurer une meilleure interactivité avec les utilisateurs et faciliter la réutilisabilité par les concepteurs d'outils.

Chaque entrée de la bibliothèque contient la description d'un protocole cryptographique (dans la syntaxe semi-formelle du papier de référence définissant la logique de Burrows, Abadi et Needham), les propriétés de sécurité que ce protocole est censé assurer ainsi que des commentaires et des liens vers des articles et pages traitant de ce protocole. On trouvera en particulier des références bibliographiques de travaux proposant des preuves formelles ou des attaques de protocoles. Les protocoles de la bibliothèque sont disponibles pour téléchargement dans plusieurs formats, incluant des formats imprimables (postscript, pdf) et des spécifications en texte des messages du protocole, à destination des concepteurs d'outils à la recherche de cas d'études.

La page SPORE, qui contient actuellement une cinquantaine de protocoles, a été conçue dans un esprit d'ouverture : les lecteurs peuvent commenter les entrées par email, entraînant une mise à jour, et surtout, peuvent soumettre de nouveaux protocoles.

Signature électronique de contrats

Participants : Alexandre Boisseau, Hubert Comon-Lundh.

Alexandre Boisseau a travaillé cette année sur les protocoles de signature électronique de contrats, et plus spécifiquement sur le protocole GJM, dû à J.A. Garay, M. Jakobsson, et P. MacKenzie ( http://www.lsv.ens-cachan.fr/spore/gjm.html). Il s'agit d'un protocole censé permettre à deux principaux A et B n'ayant pas nécessairement confiance l'un en l'autre de signer un contrat, en présence d'un tiers de confiance, appelé le TTP (« trusted third party »). Les propriétés de sécurité ne sont plus les propriétés usuelles de secret ou d'authentification, mais de :

*

équité : si B a obtenu le contrat signé par A, alors A peut obtenir le contrat signé par B et réciproquement ;
*

complétude : si le protocole de signature se déroule correctement, aucun protocole annexe, typiquement d'annulation de la procédure, n'est nécessaire ;
*

absence d'abus de confiance (« abuse-freeness ») : ni A ni B ne peut prouver à un participant extérieur qu'il connaît l'issue de la négociation ; ceci a pour but d'interdire à l'un des participants, disons A, un avantage déloyal qui lui permettrait d'obtenir de meilleures conditions auprès d'un troisième participant C à qui il pourrait montrer qu'il va avoir un contrat signé avec B ;
*

audit du TTP : si le TTP se conduit de façon malhonnête, alors A et B peuvent le prouver.

S. Kremer et J.-F. Raskin (Université libre de Bruxelles, Belgique) ont donné une modélisation du problème en utilisant la logique ATL (Alternating-Time Temporal Logic) et un modèle de systèmes de transitions alternées, dûs à Alur, Henzinger, et Kupfermann.

Le modèle d'Alexandre Boisseau étend ce dernier en en enlevant un certain nombre de simplifications dont la justification restait à trouver. Le modèle d'A. Boisseau, de ce fait, est plus complet, mais est trop gros pour les model-checkers actuels. A. Boisseau a montré, en collaboration avec S. Kremer et J.-F. Raskin, qu'on pouvait ramener le modèle complet au modèle simplifié par une technique automatique d'abstraction .