Improving Automated Symbolic Analysis of Ballot Secrecy for E-Voting Protocols: A Method Based on Sufficient Conditions
| Autor: | Cas Cremers, Lucca Hirschi |
|---|---|
| Přispěvatelé: | Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), University of Oxford [Oxford], University of Oxford |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Protocol (science)
Theoretical computer science Speedup Computer science media_common.quotation_subject 020206 networking & telecommunications 02 engineering and technology 16. Peace & justice Formal methods Symbolic data analysis [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Ballot Voting Threat model Secrecy 0202 electrical engineering electronic engineering information engineering ComputingMilieux_COMPUTERSANDSOCIETY 020201 artificial intelligence & image processing [INFO]Computer Science [cs] media_common |
| Zdroj: | EuroS&P 2019-4th IEEE European Symposium on Security and Privacy EuroS&P 2019-4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden. pp.635-650, ⟨10.1109/EuroSP.2019.00052⟩ EuroS&P |
| DOI: | 10.1109/EuroSP.2019.00052⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|