Francis Klay, Liana Bozga, Yassine Lakhnech, Laurent Mazaré, Stéphanie Delaune, and Steve Kremer. Retour d'expérience sur la validation du vote électronique. Technical Report 9, projet RNTL PROUVÉ, 2006. 47 pages
Dans ce rapport, nous présentons le travail de vérification qui a été réalisé sur le protocole de vote électronique que nous avons introduit et formalisé dans le rapport RNTL Prouvé numéro \(6\). Ce protocole a été mis au point par J. Traoré, ingénieur de recherche chez France Télécom. Il 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.
La formalisation de ce protocole à mis en évidence une grande complexité due en particulier aux structures de données et aux primitives cryptographiques manipulées. D'un autre côté ce travail a également révélé que les propriétés de sûreté à garantir sont particulièrement subtiles. Ce document présente les résultats qui ont été obtenus lors de la vérification de ce protocole. En particulier nous montrons que certaines propriétés de sûreté ont pu être prouvées automatiquement alors que pour d'autres une preuve manuelle s'est avérée nécessaire.
@techreport{Prouve:rap9,
abstract = {Dans ce rapport, nous pr{\'e}sentons le travail de
v{\'e}rification qui a {\'e}t{\'e} r{\'e}alis{\'e}
sur le protocole de vote {\'e}lectronique que nous
avons introduit et formalis{\'e} dans le rapport RNTL
Prouv{\'e} num{\'e}ro~\(6\). Ce protocole a
{\'e}t{\'e} mis au point par J.~Traor{\'e},
ing{\'e}nieur de recherche chez France
T{\'e}l{\'e}com. Il est bas{\'e} sur le m{\'e}canisme
de signature en aveugle et peut {\^e}tre
consid{\'e}r{\'e} comme un d{\'e}riv{\'e} du
protocole de Fujioka, Okamoto et~Ohta.\par La
formalisation de ce protocole {\`a} mis en
{\'e}vidence une grande complexit{\'e} due en
particulier aux structures de donn{\'e}es et aux
primitives cryptographiques manipul{\'e}es. D'un
autre c{\^o}t{\'e} ce travail a {\'e}galement
r{\'e}v{\'e}l{\'e} que les propri{\'e}t{\'e}s de
s{\^u}ret{\'e} {\`a} garantir sont
particuli{\`e}rement subtiles. Ce~document
pr{\'e}sente les r{\'e}sultats qui ont {\'e}t{\'e}
obtenus lors de la v{\'e}rification de ce protocole.
En particulier nous montrons que certaines
propri{\'e}t{\'e}s de s{\^u}ret{\'e} ont pu {\^e}tre
prouv{\'e}es automatiquement alors que pour d'autres
une preuve manuelle s'est av{\'e}r{\'e}e
n{\'e}cessaire.},
author = {Klay, Francis and Bozga, Liana and Lakhnech, Yassine and
Mazar{\'e}, Laurent and Delaune, St{\'e}phanie and
Kremer, Steve},
institution = {projet RNTL PROUV{\'E}},
month = nov,
note = {47~pages},
number = {9},
type = {Technical Report},
title = {Retour d'exp{\'e}rience sur la validation du vote
{\'e}lectronique},
year = {2006},
nmonth = {11},
lsv-category = {cont},
wwwpublic = {public},
}