Towards a mechanized proof of Selene receipt-freeness and vote-privacy

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 studied 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.