Electronic Voting: Definitions and Analysis Techniques
Vote électronique : définitions et techniques d'analyse
Résumé
In this thesis we study several aspects of the security of remote electronic voting protocols.
Such protocols describe how to securely organise elections over the Internet.
They notably aim to guarantee vote privacy - ie, votes must remain secret -and verifiability
- it must be possible to check that votes are correctly counted.
Our contributions are on two aspects.
First, we propose a new approach to automatically prove equivalence properties in the symbolic model.
Many privacy properties can be expressed as equivalence properties, such as in particular vote privacy,
but also anonymity or unlinkability.
Our approach relies on typing: we design a type system that can typecheck two protocols to prove their equivalence.
We show that our type system %, together with some additional conditions on the messages exchanged by the protocols,
soundly implies trace equivalence, both for bounded and unbounded numbers of sessions.
We compare a prototype implementation of our typechecker with other existing tools for symbolic equivalence,
on a variety of protocols from the literature.
This case study shows that our procedure is much more efficient than most other tools - at the price of losing precision (our tool may fail to prove some equivalences).
Our second contribution is a study of the definitions of privacy and verifiability - more precisely, individual
verifiability, a property that requires each voter to be able to check that their own vote is counted.
We prove that, both in symbolic and computational models,
privacy implies individual verifiability, contrary to intuition and related previous results that
seem to indicate that these two properties are opposed. Our study also highlights a limitation of existing
game-based definitions of privacy: they assume the ballot box is trusted, which makes for significantly weaker
guarantees than what protocols aim for. Hence we propose a new game-based definition
for vote privacy against a dishonest ballot box. We relate our definition to a simulation-based notion of privacy,
to show that it provides meaningful guarantees, and conduct a case study on several voting schemes.
Cette thèse porte sur l'étude de différents aspects de la sécurité des protocoles de vote électronique à distance.
Ces protocoles décrivent comment organiser des élections par Internet de manière sécurisée.
Ils ont notamment pour but d'apporter des garanties de secret du vote, et de vérifiabilité - ie, il doit être possible
de s'assurer que les votes sont correctement comptabilisés.
Nos contributions portent sur deux aspects principaux.
Premièrement, nous proposons une nouvelle technique d'analyse automatique de propriétés d'équivalence, dans le modèle symbolique.
De nombreuses propriétés en lien avec la vie privée s'expriment comme des propriétés d'équivalence, telles que le secret du vote en particulier, mais aussi l'anonymat ou la non-traçabilité.
Notre approche repose sur le typage: nous mettons au point un système de typage qui permet d'analyser deux protocoles
pour prouver leur équivalence. Nous montrons que notre système de typage est correct, c'est-à-dire qu'il implique
effectivement l'équivalence de traces, à la fois pour des nombres bornés et non bornés de sessions.
Nous comparons l'implémentation d'un prototype de notre système avec les autres outils existants pour l'équivalence
symbolique, sur divers protocoles de la littérature.
Cette étude de cas montre que notre procédure est bien plus efficace que la plupart des autres outils -
au prix d'une perte de précision (notre outil peut parfois échouer à prouver certaines équivalences).
Notre seconde contribution est une étude des définitions du secret du vote et de la vérifiabilité - ou,
plus précisément, la vérifiabilité individuelle, une propriété qui requiert que chaque votant soit en mesure de
vérifier que son propre vote a bien été pris en compte.
Nous prouvons, aussi bien dans les modèles symbolique que calculatoire, que le secret du vote implique la vérifiabilité
individuelle, alors même que l'intuition et des résultats voisins déjà établis semblaient indiquer que ces deux
propriétés s'opposent.
Notre étude met également en évidence une limitation des définitions existantes du secret du vote par jeux
cryptographiques : elles supposent une urne honnête, et par conséquent expriment des garanties significativement
plus faibles que celles que les protocoles visent à assurer. Nous proposons donc une nouvelle définition (par jeu)
du secret du vote, contre une urne malhonnête.
Nous relions notre définition à une notion de secret du vote par simulation, pour montrer qu'elle apporte
des garanties fortes. Enfin, nous menons une étude de cas sur plusieurs systèmes de vote existants.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...