论文标题
验证投票的社会技术方面：波兰邮政投票的案例2020
Verification of the Socio-Technical Aspects of Voting: The Case of the Polish Postal Vote 2020
论文作者
论文摘要
投票程序是由人，人类和人类参与的大量人设计和实施的。因此，应该考虑人为因素，以便全面地分析选举的特性并检测威胁。特别是，必须评估参与代理人（选民，市政办公室员工，邮件书记员）的行动和策略如何影响其他代理人行动的结果以及选举的总体结果。在本文中，我们首次提出了在2020年波兰总统大选的正式多代理模式中捕捉这些方面的尝试。选举标志着波兰普遍邮政投票的首次。不幸的是，投票计划是在时间压力和政治压力下制定的，而没有专家的参与。这可能已经为各种投票欺诈，内部强制等开辟了可能性。我们以多代理图的形式提出了该过程的初步可扩展模型，并通过代理逻辑的公式正式化了所选的完整性和安全性。然后，我们转换模型和公式，以便它们可以输入到最先进的模型检查器Uppaal。第一个实验表明，由于状态空间的爆炸，验证的尺度很差。但是，我们表明，通过可变抽象减少用户友好的模型降低技术，我们可以验证更复杂的方案。
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.
