Liana Bozga, Stéphanie Delaune, Francis Klay, and Ralf Treinen. Spécification du protocole de porte-monnaie électronique. Technical Report 1, projet RNTL PROUVÉ, 2004. 12 pages
Cette étude de cas a pour but de contribuer à une première évaluation des besoins pour l'aspect description formelle des protocoles cryptographiques. Cet aspect est un préalable obligé avant d'aborder des points tels que la sémantique et la vérification. Le résultat de ce travail a guidé la définition de la syntaxe du langage de spécification développé dans la tâche 1 du projet : << Sémantique des protocoles et des propriétés >>.
Parmi la multitude de protocoles existants celui qui a été étudié est un porte-monnaie électronique à clé publique développé récemment par France Télécom R&D car il reflète fidèlement les ambitions du projet. Ce protocole, sortant sans surprise du spectre de tous les outils développés à l'heure actuelle, notre travail a consisté à modéliser au mieux le porte-monnaie électronique dans un sous ensemble représentatif d'outils existants. Cette étude met évidence, sur un cas réel, les carences et les faiblesses des outils actuels et permet ainsi d'affiner et de valider les objectifs du projet. D'un autre côté, ce travail montre que des lacunes importantes peuvent parfois être raisonnablement contournées modulo un codage adapté.
@techreport{Prouve:rap1,
abstract = {Cette \'etude de cas a pour but de contribuer \`a une
premi\`ere \'evaluation des besoins pour l'aspect
description formelle des protocoles cryptographiques.
Cet aspect est un pr\'ealable oblig\'e avant
d'aborder des points tels que la s\'emantique et la
v\'erification. Le r\'esultat de ce travail a guid\'e
la d\'efinition de la syntaxe du langage de
sp\'ecification d\'evelopp\'e dans la t\^ache~1 du
projet~: <<~S\'emantique des protocoles et des
propri\'et\'es~>>.\par Parmi la multitude de
protocoles existants celui qui a \'et\'e \'etudi\'e
est un porte-monnaie \'electronique \`a cl\'e
publique d\'evelopp\'e r\'ecemment par France
T\'el\'ecom R\&D car il refl\`ete fid\`element les
ambitions du projet. Ce protocole, sortant sans
surprise du spectre de tous les outils d\'evelopp\'es
\`a l'heure actuelle, notre travail a consist\'e \`a
mod\'eliser au mieux le porte-monnaie \'electronique
dans un sous ensemble repr\'esentatif d'outils
existants. Cette \'etude met \'evidence, sur un cas
r\'eel, les carences et les faiblesses des outils
actuels et permet ainsi d'affiner et de valider les
objectifs du projet. D'un autre c\^ot\'e, ce travail
montre que des lacunes importantes peuvent parfois
\^etre raisonnablement contourn\'ees modulo un codage
adapt\'e.},
author = {Bozga, Liana and Delaune, St{\'e}phanie and
Klay, Francis and Treinen, Ralf},
institution = {projet RNTL PROUV{\'E}},
month = jun,
note = {12~pages},
number = {1},
title = {Sp{\'e}cification du protocole de porte-monnaie
{\'e}lectronique},
year = {2004},
nmonth = {6},
}