Formal Methods for Internet Voting

Méthodes formelles pour le vote électronique Le vote par internet fait référence aux élections effectuées via internet, où les électeurs utilisent leurs propres appareils personnels pour exprimer leur vote. Un tel système, bien que fondamentalement différent des élections sur papier, doit fournir les mêmes garanties de sécurité que les systèmes électoraux traditionnels. Cela inclut la vérifiabilité de l'intégrité du résultat de l'élection, tout en préservant le secret de vote.

Dans la première partie de la thèse, nous explorons les mécanismes de sécurité employés par l'industrie. À cette fin, nous effectuons une étude systématique du marché et examinons la littérature académique pour identifier les systèmes utilisés, que nous analysons ensuite. Notre travail documente le fait que la plupart des systèmes de l'industrie sont effectivement des systèmes en boîte noire, ne fournissant aucune assurance significative de vérifiabilité. Cependant, nous avons également relevé plusieurs systèmes qui mettent en œuvre des mécanismes à la pointe de la technologie, démontrant ainsi leur praticité.

Dans la deuxième partie de la thèse, nous proposons un nouveau mécanisme permettant aux électeurs de voter en toute confidentialité, même si leur propre appareil est compromis. Notre protocole est basé sur le vote par code, où l'électeur saisi un code au lieu d'un candidat. Nous avons conçu le système de manière à ce que les codes soient très courts (typiquement un ou deux chiffres), adaptés à une saisie manuelle par l'électeur.

Nous avons intégré ce mécanisme dans un protocole qui respecte les exigences de sécurité très strictes établies par la Chancellerie suisse pour les élections politiques suisses. Néanmoins, le protocole reste simple et repose uniquement sur des primitives standard. Dans la troisième partie de la thèse, nous présentons un framework permettant d'obtenir des preuves formelles de sécurité pour des protocoles de vote sur internet.

Ce framework définit un contexte électoral général, dans lequel un protocole concret peut être intégré. ProVerif, qui est un prouver automatique adapté aux protocoles cryptographiques, peut alors être utilisé pour prouver à la fois la vérifiabilité et le secret de vote. Notre travail s'appuie sur un framework récemment proposé pour la vérifiabilité, que nous étendons au secret du vote, tout en restant compatible avec les versions antérieures.

Nous améliorons également l'expressivité de la syntaxe des lemmes dans ProVerif lui-même, ce qui présente un intérêt plus général. Nous avons appliqué avec succès le framework de preuve à plusieurs protocoles de la littérature et de l'industrie, y compris Belenios, Swiss Post, et notre propre proposition de vote par codes courts.