Stéphanie Delaune and Francis Klay. Vérification automatique appliquée à un protocole de commerce électronique. In Actes des 6èmes Journées Doctorales Informatique et Réseau (JDIR'04), pp. 260–269, Lannion, France, November 2004.
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 un protocole de porte-monnaie électronique, développé récemment par une équipe de France Télécom.
@inproceedings{dk-jdir-2004,
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 un protocole de porte-monnaie
{\'e}lectronique, d{\'e}velopp{\'e} r{\'e}cemment par
une {\'e}quipe de France T{\'e}l{\'e}com.},
address = {Lannion, France},
author = {Delaune, St{\'e}phanie and Klay, Francis},
booktitle = {{A}ctes des 6{\`e}mes {J}ourn{\'e}es {D}octorales
{I}nformatique et {R}{\'e}seau ({JDIR}'04)},
month = nov,
pages = {260-269},
title = {V{\'e}rification automatique appliqu{\'e}e {\`a} un
protocole de commerce {\'e}lectronique},
year = {2004},
acronym = {{JDIR}'04},
nmonth = {11},
}