UC Modelling and Security Analysis of the Estonian IVXV Internet Voting System

TL;DR

This paper provides the first formal security analysis of Estonia's IVXV internet voting system, modeling human behavior and verifying its end-to-end verifiability using the UC framework.

Contribution

It introduces a rigorous security model for IVXV, incorporating real voter behavior, and demonstrates its practical verifiability despite low audit participation.

Findings

IVXV achieves end-to-end verifiability in practice

Only 4% of voters audit their ballots on average

The security model accounts for human behavior effects

Abstract

Estonian Internet voting has been used in national-wide elections since 2005. However, the system was initially designed in a heuristic manner, with very few proven security guarantees. The Estonian Internet voting system has constantly been evolving throughout the years, with the latest version (code-named IVXV) implemented in 2018. Nevertheless, to date, no formal security analysis of the system has been given. In this work, for the first time, we provide a rigorous security modeling for the Estonian IVXV system as a ceremony, attempting to capture the effect of actual human behavior on election verifiability in the universal composability (UC) framework. Based on the voter behavior statistics collected from three actual election events in Estonia, we show that IVXV achieves end-to-end verifiability in practice despite the fact that only $4\%$ (on average) of the Estonian voters audit their ballots.