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.
Original language | English |
---|---|
Title of host publication | Electronic Voting - Second International Joint Conference, E-Vote-ID 2017, Bregenz, Austria, October 24-27, 2017, Proceedings |
Publisher | Springer |
Publication date | 2017 |
Pages | 110-126 |
ISBN (Print) | 978-3-319-68686-8 |
DOIs | |
Publication status | Published - 2017 |
Series | Lecture Notes in Computer Science |
---|---|
Volume | 10615 |
ISSN | 0302-9743 |
Keywords
- Selene voting protocol
- individual verifiability
- Vote-Privacy
- Receipt-Freeness
- formal verification