Steve Kremer: Retour d'expérience sur la validation du vote électronique

Retour d'expérience sur la validation du vote électronique

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.

Download

[PDF]

Abstract

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.

BibTeX

@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},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap9.pdf},
}