Paper 2015/942

Ballot secrecy: Security definition, sufficient conditions, and analysis of Helios

Abstract

Let's formalise ballot secrecy as a game between a benign challenger, malicious adversary, and voting system, the adversary tasked to break security, make distinction between observed world and some parallel one, only the challenger knowing which world is under observation: Our formalisation improves earlier work to ensure detection of attacks when ballot collection is adversary controlled. We also formalise ballot independence (from asymmetric encryption's security game), and prove independence suffices for secrecy in voting systems with zero-knowledge tallying proofs. Using that proof simplification, we present blueprints for construction of non-malleable encryption based voting systems with certified ballot secrecy. Additionally, we analyse the Helios voting system and its mixnet variant, finding secrecy isn't satisfied by Helios, earlier techniques missing the attack because tallying algorithm inputs are assumed uncompromised, implicitly requiring all ballot processing be trusted, which we like to avoid, rather than assuming risk. Our blueprint guides construction of a variant proven to ensure secrecy.