Verification of the Socio-Technical Aspects of Voting: The Case of the Polish Postal Vote 2020

TL;DR

This paper models the socio-technical voting process of Poland's 2020 postal vote using multi-agent systems and formal verification, highlighting challenges and solutions in ensuring election integrity.

Contribution

It introduces a formal multi-agent graph model for postal voting, formalizes security properties, and applies model checking with abstraction techniques to verify election integrity.

Findings

Verification faces scalability issues due to state-space explosion.

Model reduction via variable abstraction improves verification of complex scenarios.

First formal multi-agent approach to analyze postal voting security in Poland.

Abstract

Voting procedures are designed and implemented by people, for people, and with significant human involvement. Thus, one should take into account the human factors in order to comprehensively analyze properties of an election and detect threats. In particular, it is essential to assess how actions and strategies of the involved agents (voters, municipal office employees, mail clerks) can influence the outcome of other agents' actions as well as the overall outcome of the election. In this paper, we present our first attempt to capture those aspects in a formal multi-agent model of the Polish presidential election 2020. The election marked the first time when postal vote was universally available in Poland. Unfortunately, the voting scheme was prepared under time pressure and political pressure, and without the involvement of experts. This might have opened up possibilities for various kinds of ballot fraud, in-house coercion, etc. We propose a preliminary scalable model of the procedure in the form of a Multi-Agent Graph, and formalize selected integrity and security properties by formulas of agent logics. Then, we transform the models and formulas so that they can be input to the state-of-art model checker Uppaal. The first series of experiments demonstrates that verification scales rather badly due to the state-space explosion. However, we show that a recently developed technique of user-friendly model reduction by variable abstraction allows us to verify more complex scenarios.