Secrecy and Verifiability: An Introduction to Electronic Voting

TL;DR

This tutorial investigates how electronic voting can reconcile ballot secrecy with verifiability using modern cryptography. It adopts a game-based framework to define and prove properties like universal and individual verifiability as well as ballot secrecy, emphasizing reductions to well-studied cryptographic primitives such as IND-PA0 and non-malleable encryption. The text analyzes practical voting schemes (notably Helios and Belenios), highlighting vulnerabilities in earlier versions (e.g., ballot malleability) and showing how formal constraints and verifiable proofs can yield robust systems, including mixnets and threshold decryption. The work also discusses post-quantum considerations, ever-lasting privacy, and real-world deployments, underscoring the need for rigorous security proofs and careful operational practices in electronic voting.

Abstract

Democracies are built upon secure and reliable voting systems. Electronic voting systems seek to replace ballot papers and boxes with computer hardware and software. Proposed electronic election schemes have been subjected to scrutiny, with researchers spotting inherent faults and weaknesses. Inspired by physical voting systems, we argue that any electronic voting system needs two essential properties: ballot secrecy and verifiability. These properties seemingly work against each other. An election scheme that is a complete black box offers ballot secrecy, but verification of the outcome is impossible. This challenge can be tackled using standard tools from modern cryptography, reaching a balance that delivers both properties. This tutorial makes these ideas accessible to readers outside electronic voting. We introduce fundamental concepts such as asymmetric and homomorphic encryption, which we use to describe a general electronic election scheme while keeping mathematical formalism minimal. We outline game-based cryptography, a standard approach in modern cryptography, and introduce notation for formulating elections as games. We then give precise definitions of ballot secrecy and verifiability in the framework of game-based cryptography. A principal aim is introducing modern research approaches to electronic voting.

Figures (9)

• Figure 1: Overview of an election scheme with four algorithms. $\mathsf{Setup}$ generates a key pair; the public key is used by $\mathsf{Vote}$ to create encrypted ballots, while the private key is used by $\mathsf{Tally}$ to decrypt. Ballots flow through the bulletin board (dotted arrows indicate encrypted data). $\mathsf{Verify}$ checks the election outcome using public information. A detailed version appears in Figure \ref{['figure-voting']}.
• Figure 2: Operation of a mix network. Ciphertexts enter and pass through a sequence of mix servers. Each server randomly permutes its inputs and re-encrypts them, producing ciphertexts that encrypt the same plaintexts but appear different and are in an unpredictable order. An observer cannot link inputs to outputs provided at least one server keeps its permutation secret.
• Figure 3: Two approaches to tallying encrypted votes. Left: Homomorphic tallying combines ciphertexts mathematically, then decrypts once to reveal only the aggregate sum, so the individual votes are never exposed. Right: Mixnet tallying shuffles ciphertexts to break the link between voters and ballots, then decrypts each vote individually. Homomorphic tallying reveals less information but only supports summation; mixnet tallying supports arbitrary voting methods but reveals individual votes (though not who cast them).
• Figure 4: Structure of a security reduction. To prove a construction secure, we assume an adversary $\mathcal{A}$ can break it and build a reduction $\mathcal{B}$ that uses $\mathcal{A}$ as a subroutine. The reduction $\mathcal{B}$ plays the security game for the underlying primitive while simulating the construction for $\mathcal{A}$. If $\mathcal{A}$ succeeds, $\mathcal{B}$ uses this to win its own game. Since the primitive is assumed secure, no efficient $\mathcal{A}$ can exist.
• Figure 5: Detailed view of the election scheme. The four algorithms $\mathsf{Setup}$, $\mathsf{Vote}$, $\mathsf{Tally}$, and $\mathsf{Verify}$ are defined in Definition \ref{['def:election']}. Dashed arrows indicate secret data (the private key $\mathit{sk}$); dotted arrows indicate encrypted ballots.

Theorems & Definitions (42)

• Example 1: ElGamal encryption
• Example 2: Bitstring encoding and homomorphic tallying
• Definition 1: Indistinguishable
• Definition 2: Election scheme Smyth15:ElectionVerifiability
• Definition 3: Election correctness
• Definition 4: $\mathsf{Injectivity}$ Smyth15:ElectionVerifiabilitySmyth18:HeliosMixnetVerifiability
• Definition 5: $\mathsf{Soundness}$ Smyth15:ElectionVerifiability
• Definition 6: $\mathsf{Completeness}$ Smyth15:ElectionVerifiability
• Definition 7: $\mathsf{Universal}\textrm{-}\mathsf{Verifiability}$ Smyth15:ElectionVerifiabilitySmyth18:HeliosMixnetVerifiability
• Definition 8: Individual verifiability Smyth15:ElectionVerifiability