Provably Improving Election Verifiability in Belenios
| Autor: | Sjouke Mauw, Sergiu Bursuc, Sevdenur Baloglu, Jun Pang |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Computer science [C05] [Engineering
computing & technology] Computer science Electronic voting media_common.quotation_subject Space (commercial competition) Gas meter prover Mathematical proof Computer security computer.software_genre Sciences informatiques [C05] [Ingénierie informatique & technologie] Bulletin board Simple (abstract algebra) Voting ComputingMilieux_COMPUTERSANDSOCIETY Formal verification computer media_common |
| Zdroj: | Electronic Voting ISBN: 9783030869410 E-VOTE-ID |
| Popis: | Belenios is an online voting system that provides a strong notion of election verifiability, where no single party has to be trusted, and security holds as soon as either the voting registrar or the voting server is honest. It was formally proved to be secure, making the assump- tion that no further ballots are cast on the bulletin board after voters verified their ballots. In practice, however, revoting is allowed and voters can verify their ballots anytime. This gap between formal proofs and use in practice leaves open space for attacks, as has been shown recently. In this paper we make two simple additions to Belenios and we formally prove that the new version satisfies the expected verifiability properties. Our proofs are automatically performed with the Tamarin prover, under the assumption that voters are allowed to vote at most four times. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|