UC Modelling and Security Analysis of the Estonian IVXV Internet Voting System
This provides the first rigorous security analysis for a widely used internet voting system, addressing critical trust issues in elections.
The authors tackled the lack of formal security analysis for the Estonian IVXV internet voting system by modeling it as a ceremony in the universal composability framework, showing it achieves end-to-end verifiability in practice with only 4% of voters auditing their ballots.
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.