Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
TitelElectronic Voting - Second International Joint Conference, E-Vote-ID 2017, Bregenz, Austria, October 24-27, 2017, Proceedings
ForlagSpringer
Publikationsdato2017
Sider110-126
ISBN (Trykt)978-3-319-68686-8
DOI
StatusUdgivet - 2017
NavnLecture Notes in Computer Science
Vol/bind10615
ISSN0302-9743

Citationsformater