Alexandre Anzala-Yamajako - Propriétés de sécurité des protocoles de vote électronique - Résultats

De Ensiwiki
Aller à : navigation, rechercher


Propriétés de sécurité des protocoles de vote électronique

Labo Verimag
Equipe Distributed and Complex Systems
Encadrants marie-laure.potet@imag.fr pascal.lafourcade@imag.fr, marie-laure.potet@imag.fr

Etudiant

Anzala-Yamajako, Alitcha

Introduction

La notion de vote électronique désigne ici un protocole dans lequel les actions typiques du déroulement d'une élection (inscription sur les listes, vote, comptage et publication des résultats) sont informatisées. Aujourd'hui De nombreux pays ont été convaincus de l'intérêt du vote électronique (élection parlementaire sur internet en estonie) ou sont entrain de tester et de valider la solution qu'ils ont choisie (France, Brésil, Canada). Cependant les problèmes sont multiples et la moindre erreur peut se révéler désastreuse pour l'ensemble de l'élection. On se concentrera ici sur les différentes propriétés de sécurité que peuvent garantir les protocoles de votes électroniques. Ces propriétés sont très nombreuses et recoupent pour la plupart celles que l'on peut attendre lors d'une élection classique. Les propriétés sur lesquelles nous nous sommes concentrés sont décrites dans la littérature comme privacy-type c'est à dire que les attaquants correspondant à ces attaques vont donner des ordres à l'électeur cible puis tenter de déterminer ,avec les informations à leur disposition, si ce dernier à suivi ou pas l'ordre qui lui a été donné. Ces dernières différent principalement par la force de l'attaquant et plus précisément de la quantité d'information à sa dispotion et le moment auquel cette information lui est transmise. Plusieurs modèles de formalisation existent aujourd'hui et l'objectif de ce TER était de compléter un des modèles en fournissant des définitions formelles des propriétés décrites ci-dessous.

Eléments de pré-requis

Les trois notions centrales sont les suivantes

  • Privacy

Un protocole a la propriété de privacy si il est impossible pour un adversaire n'ayant accès qu'aux données publiques de deviner pour qui a voté un électeur donné. C'est la plus basique des propriétés des protocoles de vote électroniques et tous les protocoles de la littérature ont cette propriété

  • Receipt-Freeness

Un protocole a la propriété de receipt-freeness si il est impossible pour un votant coopérant avec son attaquant de pouver qu'il a voté d'une certaine manière. Dans ce modèle d'attaque, l'attaquant a accès au matériel privé du votant (en partie ou dans son entierté) après l'étape de vote.

  • Coercion-Resistance

La coercion-résistance, la plus forte des trois propriétés, modélise des attaques d'une tout autre ampleur. En effet, dans ce modèle d'attaque, l'attaquant a accès au matériel privé du votant mais juste après l'étape d'enregistrement. Ceci lui permet donc de poster un bulletin de vote à la place du votant, de ne poster aucun bulletin, voire de poster des bulletins au hasard et d'observer les réponses que lui fourni le protocole.

Il est interessant de noter que les définitions informelles de ces notions laissent à penser qu'elles s'impliquent (de coercion-resistance à privacy la quantité d'information va en décroissant donc empiriquement CR \Rightarrow RF \Rightarrow P et P \nRightarrow RF \nRightarrow CR. Nous avons résumé les différents modèles d'attaques dans le schéma suivant

Attackmodel.jpeg

Cette dernière notion n'a été formalisé que très récemment (voire les travaux [1] [2] [3] [4]) et la très grande majorité des protocoles actuels sont sensibles à cette attaque et la seule définition computationelle de coercion-resistance est la définition de Juels [4] malheureusement cette définition est peu intuitive et très liée au protocole décrit dans ce même papier. Pour cette raison Pascal Lafourcade et Roukaya Keinj ont proposé dans [5] une nouvelle définition de coercion résistance.

Pour éclairer la suite, nous préciserons également ici que dans le modèle computationel les propriétés sont définies par des propabilités sur des jeux entre un attaquant et sa cible au cours desquels la cible de l'attaquant a la possibilité de tenter de lui échapper (tout en feignant la coopération) et le but de l'attaquant est de déterminer le comportement de sa cible. Plus formellement un protocole ES à la propriété prop si pour tout adversaire A la quantité Adv^{prop}_{ES,A} =|Pr[ Exp^{prop}_{ES,A}(.)= 1\vert b=1]-Pr[ Exp^{prop}_{ES,A}(.)= 1\vert b=0]| est négligeable. L'expérience Exp^{prop}_{ES,A}(.) représente le jeu mentionné ci-dessus. Au cours de ce jeu, un bit b est tiré au hasard, si le bit vaut 0 alors le votant cible tente de berner l'attaquant, si b vaut 1, le votant se soumet. A la fin de l'étape de vote et en fonction de la quantité d'information à sa disposition (selon le modèle de l'attaque) l'attaquant tente de deviner la valeur de b. En réalité Adv^{prop}_{ES,A} est la traduction formelle de la notion suivante: un protocole ES a la propriété prop si lorsqu'un adversaire pense que sa cible s'est soumise à sa volonté, il a autant de chances d'avoir raison que de se tromper.


Travail réalisé

Before.jpg

Ceci représente l'état de l'art dans le domaine des propriétés de sécurité des protocoles de votes électroniques. On remarque que dans le modèle computationel il n'y'a ni définition de receipt-freeness, ni définition de privacy, de plus il n'y a pas de relation claire entre la définition de Lafourcade et al. et celle de Juels.

Nous allons détailler ici les résultats principaux de ce TER

  • Définition formelle de privacy

Pour formaliser cette définition nous avons suivi en plus de la notion intuitive décrite dans les prérequis celle donnée dans [1] mais transposée dans le modèle computationel. Un protocol a la propriété de privacy si un adversaire est incapable de distinguer la situation dans la laquelle 2 cibles échangent leurs votes de la situation dans laquelle elles votent comme elles l'avaient initialement prévues.

  • Définition formelle de Receipt-Freeness

Pour modéliser la notion de receipt-freeness nous avons tenter de modéliser le fait qu'un attaquant est incapable de déterminer le comportement de sa cible si il est incapable lorsqu'il reçoit des informations privées de cette dernière de déterminer si elles sont authentiques ou non. Pour cela nous avons utilisé une fonction fake_private qui suppose que le protocole laisse la possibilité au votant de construire un ensemble de données privées invalide mais indistingable de vraies données privées sans le contrôle d'une majorité des entités autorités.

  • Précision de la puissance de l'attaquant modélisé par la définition [5]

Il étaient important également de comprendre le rôle et la "place" de la définition fournie dans [5]. Nous avons réussi à montrer formellement qu'elle était moins forte que la propriété de coercion résistance mais moins forte que celle de receipt-freeness ie RF \Rightarrow NewCR \Rightarrow P et P \nRightarrow NewCR \nRightarrow RF

  • Preuve des relations "naturelles" entre les définitions

Comme nous l'avions fait remarqué plus haut, les définitions en langage naturels des propriétés laissent penser qu'il existe des relations d'implications entre elles. Nous avons formellement montré ces relation pour les 2 définitions que nous avons proposé ie. RF \Rightarrow P et P \nRightarrow RF .

Plus de détails ainsi que les expériences décrivant les propriétés ainsi que les preuves sont décrites dans le rapport


Conclusion

Compute.jpg

Pour permettre la comparaison, nous avons indiqué en rouge sur ce schéma les résultats obtenus pendant ce projet ( les flèches représentent une preuve d'implication ou de non-implication).

Pendant ce projet nous avons pu construire un modèle cohérent pour l'étude future des protocoles de votes électroniques. Il manque cependant les relations avec la définition de coercion-resistance de [4] pour en faire un modèle aussi complet que le modèle symbolique. De futurs travaux s'axeraient sur l'approfondissement de la compréhension de la définition de juels [4], de tentatives d'application de cette définition sur d'autres protocoles que celui de [4] et eventuellement la proposition d'une nouvelle définition de coercion-resistance


Références

Pour des pointeurs directs vers les articles, se référer à la bibliographie du rapport

  • [1] Stephanie Delaune, Steve Kremer and Mark Ryan "Coercion-resistance and Receipt-freeness in Electronic Voting"
  • [2] Ralf Kuesters, Tomasz Truderung "An Epistemic Approach to Coercion-Resistance for Electronic Voting Protocols"
  • [3] Michael Backes, Catalin Hritcu, Matteo Maffei "Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus"
  • [4] Ari Juels, Markus Jakobsson "Coercion-Resistant Electronic Elections"
  • [5] Pascal Lafourcade, Roukaya Keinj "A new definition of Coercion-Resistance"


Documents additionnels