A short introduction to secrecy and verifiability for elections

TL;DR

This paper discusses the importance of formal definitions of secrecy and verifiability in election schemes, illustrating their use through analysis and improvement of the Helios voting system.

Contribution

It introduces formal definitions of secrecy and verifiability for elections and demonstrates their application in analyzing and enhancing election schemes like Helios.

Findings

Identified vulnerabilities in the original Helios system

Developed a secure variant of Helios with formal proofs

Highlighted the importance of formal analysis in election security

Abstract

We explore the fundamental properties that are necessary to ensure that election schemes behave as expected. The exploration reveals how our understanding of those expectations has evolved, culminating in the emergence of formal definitions of properties necessary to fulfil expectations. We provide insights into definitions of secrecy and verifiability, allowing us to learn and appreciate the underlying intuition and technical details of these notions. Equipped with definitions, we can build election schemes that can be proven to behave as expected. And, as an illustrative example, we review a variant of the Helios election system that was built and proven secure, in this way. Furthermore, the definitions can be used to analyse existing election schemes, and vulnerabilities have been uncovered. Indeed, we describe a series of vulnerabilities that were discovered during the analysis of the original Helios system, which advanced our understanding of system behaviour and prompted the design of the aforementioned variant. Thus, this article contributes to the science of security by sharing valuable insights into elections, and demonstrating the value that formal definitions and analysis have in building schemes guaranteed to behave as expected.