Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-review
Open access
Publication Information
Output type
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 110-126Publication milestones
- Published - 2017
Publication status
Published - 2017
Publisher
Springer, United States, GermanyBook series
- Book series name: Lecture Notes in Computer Science
Volume: 10615
ISSN: 0302-9743
ISBN (Print)
978-3-319-68686-8Publication IDs
- Scopus: 85032468251
Host publication title
Electronic Voting - Second International Joint Conference, E-Vote-ID 2017, Bregenz, Austria, October 24-27, 2017, ProceedingsAbstract
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.
Publication metrics
PlumX, opens in new tab
Citations
17
Captures
5
Access to documents
Accepted author manuscript, 333.82 KB