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

Cremers, Cas and Hirschi, Lucca
(2019) Improving Automated Symbolic Analysis of Ballot Secrecy for E-voting Protocols: A Method Based on Sufficient Conditions.
In: 4th IEEE European Symposium on Security and Privacy, June 17-19, 2019, Stockholm.
Conference: EuroS&P IEEE European Symposium on Security and Privacy

Full text not available from this repository.

Abstract

We advance the state-of-the-art in automated symbolic analysis for e-voting protocols by introducing three conditions that together are sufficient to guarantee ballot secrecy. There are two main advantages to using our conditions, compared to existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: we 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 it 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 FOO, LEE, JCJ, and Belenios. In these case studies, our approach does not yield any false attacks, suggesting that our conditions are tight.

Actions

Actions (login required)

View Item View Item