Colloquium V. Cortier – Mardi 20 septembre 2016
Vote électronique: la logique à la rescousse
Résumé: Le vote électronique se doit d’ouvrir les mêmes garanties que le vote traditionnel à l’urne. Dans ce but, les protocoles de vote électronique ont recours à des primitives cryptographiques, comme dans le cas plus classique des protocoles d’authentification ou d’échange de clefs. Il est désormais reconnu que tous ces protocoles sont difficiles à concevoir et à vérifier. Ainsi, des attaques peuvent être découvertes des années plus tard. Les modèles formels, comme les algèbres de processus, les clauses de Horn ou les systèmes de contraintes, ont été utilisés avec succès pour analyser automatiquement de nombreux protocoles. Cependant, les protocoles de vote électronique compliquent significativement la tâche des outils de véri‑cation. En effet, ils font appel à des primitives souvent nouvelles et complexes (comme le chiffrement homomorphique), à de nouveaux schémas d’exécution et assurent de nouvelles propriétés de sécurité.