Dec 07

AVOTE : Principaux résultats du projet

Principaux résultats du projet

Le vote électronique offre de nombreux avantages comme le vote à distance ou l’automatisation de la phase de dépouillement. Cependant, la moindre faille dans un système de vote électronique pourrait conduire à une fraude à grande échelle. L’objectif général du projet était de concevoir des techniques pour analyser la sécurité des protocoles de vote. Nos résultats s’articulent sur quatre principaux plans.

  • Formalisation de propriétés: Nous avons identifié et formalisé les propriétés souhaitées: correction du résultat, confidentialité des votes, impossibilité pour un votant de révéler son vote, vérifiabilité du processus de vote. Nous avons défini formellement ces propriétés dans des modèles symboliques, souvent sous la forme de propriété d’équivalence. (, )
  • Procédures de décision:
    Nous avons développé des techniques pour déterminer si un protocole de vote assure ou non les propriétés souhaitées comme par exemple la confidentialité d’un vote. D’un point de vue technique, cela revient à décider des propriétés d’équivalence sur des algèbres de processus. Nos travaux ont porté sur deux principaux types d’équivalence: équivalence statique (pour un intrus observateur) et équivalence observationnelle (pour un intrus pleinement actif). Dans les deux cas, les propriétés des primitives cryptographiques (chiffrement, ou exclusif, …) sont axiomatisées par des théories équationnelles. Nous avons obtenu de nombreux résultats de décision aussi bien pour l’équivalence statique que pour l’équivalence observationnelle, et cela pour différentes théories équationnelles. (, , , [CD10], , )
  • Outils:
    Nous avons réalisé quatre prototypes pour analyser automatiquement des propriétés d’équivalence de protocoles, et en particulier la confidentialité dans les protocoles de vote. Nos quatre prototypes sont KiSs et , pour un attaquant observateur, ainsi que aKiSs et ADECS/Datep, pour un attaquant pleinement actif.
  • Études de cas:
    Nous avons validé nos résultats sur plusieurs études de cas issues de la littérature dont le protocole FOO, qui est à la base de nombreux protocoles utilisant les signatures en aveugle et le protocole JCJ implémenté en tant que CIVITAS. Nous avons également analysé Helios, un protocole de vote réel, développé récemment par Ben Adida et le Crypto Group de l’Université Catholique de Louvain (UCL). Ce protocole a été utilisé plusieurs fois pour des élections grandeur nature, par exemple en 2009 pour l’élection du recteur de l’UCL avec plus de 5000 votants et aussi en 2010 par l’association internationale de cryptographie (IACR) pour élire son conseil. Nous avons mis à jour une faille dans le protocole Helios permettant de mettre à mal la confidentialité des votes. Nous avons proposé une correction, ainsi qu’une preuve de confidentialité pour la nouvelle version ainsi obtenue. Nous avons également montré qu’Helios assurait la vérifiabilité individuelle et la vérifiabilité universelle, permettant une transparence du scrutin. ([DKR09b], , [KSR10])
    Une autre étude de cas pratique fut le protocole de vote à distance (bulletins imprimés avec codes à barre) utilisé par le CNRS dans le cadre d’élection au CAES (comité d’entreprise du CNRS). Nous avons montré comment il était possible de « bourrer les urnes » et notifié le CNRS . Un correctif a été apporté par la société prestataire, pour le scrutin suivant. ()

L’ensemble des publications du projet est disponible iciSuite du projet: Une partie des thèmes de recherche du projet ANR AVOTÉ a été reprise dans le projet ERC ProSecure (Provably secure systems: foundations, design, and modularity) et dans le projet ANR VIP (Programme JCJC) (Verification of Indistinguishability Properties). Le projet ProSecure a pour but de développer des techniques modulaires et génériques pour analyser de nouvelles familles de protocoles de sécurité, et notamment les protocoles de vote. Le projet VIP s’intéresse plus particulièrement à l’analyse de propriétés du type “respect de la vie privée” qui jouent un rôle important dans de nombreuses applications (dont les protocoles de vote). Une variante d’Helios, appelée Helios-C, est en cours de développement. Cette variante permet d’être conforme aux recommandations de la CNIL (le nom des électeurs ne doit pas être public), tout en garantissant toujours la confidentialité des vote et la vérifiabilité du scrutin, même vis-à-vis d’une urne hébergée sur un serveur malhonnête.

Analyse formelle de protocoles de vote électronique (AVOTÉ).