Liana Bozga, Stéphanie Delaune, Francis Klay, and Laurent Vigneron. Retour d'expérience sur la validation du porte-monnaie électronique. Technical Report 5, projet RNTL PROUVÉ, 2005. 29 pages
Le domaine de la modélisation et de la vérification est une activité délicate et importante qui a connu une véritable explosion dans les années 1990. On dispose à l'entrée des années 2000 de toute une gamme de modèles et de méthodes plus ou moins avancés en ce qui concerne l'expressivité et l'automatisation.
Afin de définir les besoins et les priorités à mettre sur les outils consacrés à la vérification de protocoles cryptographiques qui seront développés au sein du projet RNTL PROUVÉ, nous proposons de travailler en situation réelle, sur des protocoles plutôt << durs >>, en effectuant le cycle suivant: modélisation, formalisation puis validation dans des outils existants. Ce travail est effectué ici pour deux versions d'un protocole de porte-monnaie électronique, dont l'une a été développée récemment par une équipe de France Télécom. Les outils retenus pour la réalisation de cette étude sont ProVerif, Hermes et Casrul, en raison de leurs caractéristiques très différentes.
@techreport{Prouve:rap5,
abstract = {Le domaine de la mod{\'e}lisation et de la
v{\'e}rification est une activit{\'e} d{\'e}licate et
importante qui a connu une v{\'e}ritable explosion
dans les ann{\'e}es~1990. On dispose {\`a}
l'entr{\'e}e des ann{\'e}es~2000 de toute une gamme
de mod{\`e}les et de m{\'e}thodes plus ou moins
avanc{\'e}s en ce qui concerne l'expressivit{\'e} et
l'automatisation. \par Afin de d{\'e}finir les
besoins et les priorit{\'e}s {\`a} mettre sur les
outils consacr{\'e}s {\`a} la v{\'e}rification de
protocoles cryptographiques qui seront
d{\'e}velopp{\'e}s au sein du projet RNTL PROUV{\'E},
nous proposons de travailler en situation r{\'e}elle,
sur des protocoles plut{\^o}t <<~durs~>>, en
effectuant le cycle suivant: mod{\'e}lisation,
formalisation puis validation dans des outils
existants. Ce travail est effectu{\'e} ici pour deux
versions d'un protocole de porte-monnaie
{\'e}lectronique, dont l'une a {\'e}t{\'e}
d{\'e}velopp{\'e}e r{\'e}cemment par une {\'e}quipe
de France T{\'e}l{\'e}com. Les outils retenus pour la
r{\'e}alisation de cette {\'e}tude sont ProVerif,
Hermes et Casrul, en raison de leurs
caract{\'e}ristiques tr{\`e}s diff{\'e}rentes.},
author = {Bozga, Liana and Delaune, St{\'e}phanie and
Klay, Francis and Vigneron, Laurent},
institution = {projet RNTL PROUV{\'E}},
month = mar,
note = {29~pages},
number = {5},
title = {Retour d'exp{\'e}rience sur la validation du
porte-monnaie {\'e}lectronique},
year = {2005},
nmonth = {3},
lsv-category = {cont},
wwwpublic = {public},
}