UC Modelling and Security Analysis of the Estonian IVXV Internet Voting System
Bingsheng Zhang, Zengpeng Li, Jan Willemson

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 (on average) of the Estonian voters audit…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsInternet Traffic Analysis and Secure E-voting · Advanced Authentication Protocols Security · Cryptography and Data Security
