Paper 2026/2576

Reverse Engineering IVXV: A Specification and Security Analysis of Estonia’s Internet Voting System

Abstract

Estonia’s IVXV system is one of the world’s longest-running and largest-scale deployments of internet voting, yet it lacks a precise public specification of the protocol as implemented or security claims, which has left it difficult to audit independently. We address this as follows: First, we reverse engineer a detailed specification of IVXV as implemented—covering the setup, voting, tallying, and audit phases—comprising protocol-flow diagrams, pseudocode algorithms, and the core data structures, reconstructed from the public source code, official documentation, and configuration examples. Second, we complement the specification with an executable TLA+ model of the setup, voting, and tally phases, which we check with TLC for basic executability and correctness and which serves as an extensible basis for modelling concrete attack scenarios. Third, using the reconstructed specification, we carry out a systematic security analysis under a broad range of threat models spanning individual verifiability, universal verifiability, privacy, coercion resistance, and eligibility verifiability, and we reassess previously known attacks against the current protocol. Fourth, we compare IVXV against two of the most extensively studied deployed systems, Belenios and Swiss Post, across these properties in order to situate its guarantees. Fifth, we discover numerous previously unknown, vulnerabilities—spanning ballot privacy, individual verifiability, and universal verifiability, many of them arising from inconsistent validation logic across components, encoding discrepancies, and unchecked cryptographic parameters—and validate selected findings with proof-of-concept tests that exercise the real implementation. Finally, we propose concrete mitigations for the attacks we identify.