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

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


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
Original languageEnglish
Title of host publicationElectronic Voting - Second International Joint Conference, E-Vote-ID 2017, Bregenz, Austria, October 24-27, 2017, Proceedings
Publication date2017
ISBN (Print)978-3-319-68686-8
Publication statusPublished - 2017
SeriesLecture Notes in Computer Science


  • Selene voting protocol
  • individual verifiability
  • Vote-Privacy
  • Receipt-Freeness
  • formal verification


Dive into the research topics of 'Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy'. Together they form a unique fingerprint.

Cite this