Analyse formelle d'un protocole de vote électronique en
pi-calcul appliqué
kremer@lsv.ens-cachan.fr
Le vote électronique promet un moyen potentiellement efficace et sûr
pour réaliser des élections. Malheureusement, le fait d'informatiser une
élection expose cette élection à des nouveaux risques de fraude qui
pourraient se faire à grande échelle et seraient difficilement détectables.
Une partie de ces problèmes peuvent être évitées en vérifiant les
protocoles à l'aide d'outils formels. Nous introduisons un ensemble de
propriétés qu'un protocole de vote électronique devrait satisfaire.
Ensuite nous montrons sur une étude de cas, le protocole de Fujioka et
al., comment formaliser et vérifier certaines de ces propriétés dans le
formalisme du pi-calcul appliqué. En particulier, nous vérifierons les
propriétés d'équité, d'éligibilité et d'anonymat. Cette vérification a
pu être partiellement automatisée à l'aide de l'outil ProVerif. Nous
expliquerons aussi certaines limitations de l'outil.
|
