Verifiability of Helios Mixnet
We study game-based definitions of individual and universal verifiability by Smyth, Frink and Clarkson. We prove that building voting systems from El Gamal coupled with proofs of correct key generation suffices for individual verifiability. We also prove
- PDF / 335,757 Bytes
- 15 Pages / 439.37 x 666.142 pts Page_size
- 4 Downloads / 153 Views
Abstract. We study game-based definitions of individual and universal verifiability by Smyth, Frink and Clarkson. We prove that building voting systems from El Gamal coupled with proofs of correct key generation suffices for individual verifiability. We also prove that it suffices for an aspect of universal verifiability. Thereby eliminating the expense of individualverifiability proofs and simplifying universal-verifiability proofs for a class of encryption-based voting systems. We use the definitions of individual and universal verifiability to analyse the mixnet variant of Helios. Our analysis reveals that universal verifiability is not satisfied by implementations using the weak Fiat-Shamir transformation. Moreover, we prove that individual and universal verifiability are satisfied when statements are included in hashes (i.e., when using the Fiat-Shamir transformation, rather than the weak Fiat-Shamir transformation).
1
Introduction
An election is a decision-making procedure to choose representatives [3,13,24,31]. Choices should be made by voters with equal influence, and this must be ensured by voting systems [26,27,41]. Many electronic voting systems build upon creativity and skill, rather than scientific foundations, and are routinely broken in ways that permit adversaries to unduly influence the selection of representatives, e.g., [5,7,14,18,40]. Breaks can be avoided by carefully formulating rigorous and precise security definitions that capture notions of voters voting with equal influence, and proving that systems satisfy these definitions. Applicable definitions include [9,10,15,17,19,20,37,38] and we build upon work by Smyth, Frink and Clarkson [37]. (The relative merits of definitions are considered in Sect. 2.) They present game-based security definitions in the computational model of cryptography [16], whereby a benign challenger, a malicious adversary and a voting system engage in a series of interactions which task the adversary to complete a challenge. Successful completion of the task corresponds to an execution of the voting system in which security is broken. Thus, the task captures what the adversary should not be able to achieve. Universal verifiability formalises a notion of checking whether voters voted with equal influence. – Universal verifiability. Anyone can check whether an outcome corresponds to votes expressed in recorded ballots. c International Financial Cryptography Association 2019 A. Zohar et al. (Eds.): FC 2018 Workshops, LNCS 10958, pp. 247–261, 2019. https://doi.org/10.1007/978-3-662-58820-8_17
248
B. Smyth
Smyth, Frink and Clarkson formalise a game-based definition of universal verifiability [37]. That game tasks the adversary to compute inputs to the tallying procedure, including an election outcome and some ballots, that cause checks to succeed when the outcome does not correspond to the votes expressed by those ballots, or that cause checks to fail when the outcome does correspond to the votes expressed. Merely casting a ballot is insufficient to ensure it is recorded, because an adversary ma
Data Loading...
