Stéphanie Delaune, Francis Klay, and Steve Kremer. Spécification du protocole de vote électronique. Technical Report 6, projet RNTL PROUVÉ, 2005. 19 pages
Cette nouvelle étude de cas a pour but de tester les limites du langage \scshape Prouvé. En effet, le protocole que nous avons choisi d'étudier est volontairement complexe tant au niveau de la modélisation des propriétés de sécurité que de la description du protocole lui-même en raison de la manipulation de structures de données telles que les listes.
Notre étude de cas est un protocole de vote qui a été mis au point par J. Traoré, ingénieur de recherche chez France Télécom. Ce protocole est basé sur le mécanisme de signature en aveugle et peut être considéré comme un dérivé du protocole de Fujioka, Okamoto et Ohta. Ce document introduit dans un premier temps le problème du vote électronique en général avant de décrire le protocole en lui-même et sa formalisation dans le langage \scshape Prouvé.
@techreport{Prouve:rap6,
abstract = {Cette nouvelle \'etude de cas a pour but de tester
les limites du langage~{\scshape Prouv\'e}. En effet,
le protocole que nous avons choisi d'\'etudier est
volontairement complexe tant au niveau de la
mod\'elisation des propri\'et\'es de s\'ecurit\'e que
de la description du protocole lui-m\^eme en raison
de la manipulation de structures de donn\'ees telles
que les listes.\par Notre \'etude de cas est un
protocole de vote qui a \'et\'e mis au point par
J.~Traor\'e, ing\'enieur de recherche chez
France~T\'el\'ecom. Ce protocole est bas\'e sur le
m\'ecanisme de signature en aveugle et peut \^etre
consid\'er\'e comme un d\'eriv\'e du protocole de
Fujioka, Okamoto et~Ohta. Ce document introduit dans
un premier temps le probl\`eme du vote \'electronique
en g\'en\'eral avant de d\'ecrire le protocole en
lui-m\^eme et sa formalisation dans le
langage~{\scshape Prouv\'e}.},
author = {Delaune, St{\'e}phanie and Klay, Francis and
Kremer, Steve},
institution = {projet RNTL PROUV{\'E}},
month = nov,
note = {19~pages},
number = {6},
title = {Sp{\'e}cification du protocole de vote
{\'e}lectronique},
year = {2005},
nmonth = {11},
lsv-category = {cont},
wwwpublic = {public},
}