Abstract
Selene is a novel voting protocol that supports individual
verifiability, Vote-Privacy and Receipt-Freeness. The scheme provides
tracker numbers that allow voters to retrieve their votes from a public
bulletin board and a commitment scheme that allows them to hide their
vote from a potential coercer. So far, however, Selene was never stud-
ied formally. The Selene protocol was neither completely formalized, nor
were the correctness proofs for Vote-Privacy and Receipt-Freeness.
In this paper, we give a formal model for a simplified version of Selene in
the symbolic model, along with a machine-checked proof of Vote-Privacy
and Receipt-Freeness. All proofs are checked with the Tamarin theorem
prover.
verifiability, Vote-Privacy and Receipt-Freeness. The scheme provides
tracker numbers that allow voters to retrieve their votes from a public
bulletin board and a commitment scheme that allows them to hide their
vote from a potential coercer. So far, however, Selene was never stud-
ied formally. The Selene protocol was neither completely formalized, nor
were the correctness proofs for Vote-Privacy and Receipt-Freeness.
In this paper, we give a formal model for a simplified version of Selene in
the symbolic model, along with a machine-checked proof of Vote-Privacy
and Receipt-Freeness. All proofs are checked with the Tamarin theorem
prover.
| Originalsprog | Engelsk |
|---|---|
| Titel | Electronic Voting - Second International Joint Conference, E-Vote-ID 2017, Bregenz, Austria, October 24-27, 2017, Proceedings |
| Forlag | Springer |
| Publikationsdato | 2017 |
| Sider | 110-126 |
| ISBN (Trykt) | 978-3-319-68686-8 |
| DOI | |
| Status | Udgivet - 2017 |
| Navn | Lecture Notes in Computer Science |
|---|---|
| Vol/bind | 10615 |
| ISSN | 0302-9743 |
Emneord
- Selene voting protocol
- individual verifiability
- Vote-Privacy
- Receipt-Freeness
- formal verification