Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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.
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-02368857
Contributor : Lucca Hirschi <>
Submitted on : Friday, June 26, 2020 - 11:08:24 AM
Last modification on : Thursday, May 27, 2021 - 1:54:06 PM

File

EuroSP19_evoting.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

85

Files downloads

149