Improving Automated Symbolic Analysis of Ballot Secrecy for E-Voting Protocols: A Method Based on Sufficient Conditions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Improving Automated Symbolic Analysis of Ballot Secrecy for E-Voting Protocols: A Method Based on Sufficient Conditions

Résumé

We advance the state-of-the-art in automated symbolic analysis of ballot secrecy for e-voting protocols by proposing a method based on analysing three conditions that together imply ballot secrecy. Our approach has two main advantages over existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: our approach can systematically deal with (a) honest authorities present in different phases, (b) threat models in which no dishonest voters occur, and (c) protocols whose ballot secrecy depends on fresh data coming from other phases. The second advantage is that our approach can significantly improve verification efficiency, as the individual conditions are often simpler to verify. E.g., for the LEE protocol, we obtain a speedup of over two orders of magnitude. We show the scope and effectiveness of our approach using ProVerif in several case studies, including the FOO, LEE, JCJ, and Belenios protocols.
Fichier principal
Vignette du fichier
EuroSP19_evoting.pdf (442.67 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02368857 , version 1 (26-06-2020)

Identifiants

Citer

Lucca Hirschi, Cas Cremers. Improving Automated Symbolic Analysis of Ballot Secrecy for E-Voting Protocols: A Method Based on Sufficient Conditions. EuroS&P 2019 - 4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden. pp.635-650, ⟨10.1109/EuroSP.2019.00052⟩. ⟨hal-02368857⟩
51 Consultations
75 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More