Verification of the Socio-Technical Aspects of Voting The Case of the Polish Postal Vote 2020 Yan Kim1 Wojciech Jamroga12 and Peter Y .A. Ryan1

2025-05-06 0 0 840.65KB 19 页 10玖币

侵权投诉

Veriﬁcation of the Socio-Technical Aspects of Voting:

The Case of the Polish Postal Vote 2020

Yan Kim1, Wojciech Jamroga1,2, and Peter Y.A. Ryan1

1Interdisciplinary Centre for Security, Reliability, and Trust, SnT, University of Luxembourg

2Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland

{yan.kim, wojciech.jamroga, peter.ryan}@uni.lu

Abstract.

Voting procedures are designed and implemented by people, for people,

and with signiﬁcant 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 ofﬁce employees, mail clerks) can inﬂuence

the outcome of other agents’ actions as well as the overall outcome of the election.

In this paper, we present our ﬁrst attempt to capture those aspects in a formal multi-

agent model of the Polish presidential election 2020. The election marked the

ﬁrst 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 ﬁrst series of experiments demonstrates that veriﬁcation 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.

1 Introduction

In the last 30 years, the world has become densely connected. This results in a consider-

able space of potential threats, risks, and conﬂicting interests, that call for systematic

(and preferably machine-assisted) analysis. What is more, IT services are implemented

by people, with people, and for people. The intensive human involvement makes them

hard to analyse beyond the usual computational complexity obstacles.

Voting procedures. Voting and elections are prime examples of services that are difﬁcult

to specify, hard to verify, and extremely important to the society [

]. If democracy is

to be effective, it is essential to assess and mitigate the threats of fraud, manipulation,

and coercion [

]. However, formal analysis of voting procedures must consider both

the technological side of elections (i.e., protocols, architectures, and implementations)

and the human and social context in which it is embedded [

]. The impact of the social

factor has become especially evident during the US presidential elections of 2016 and

2020. In 2016, individual voters were targeted before the election by a combination

arXiv:2210.10694v2 [cs.MA] 18 Oct 2023

2 Yan Kim, Wojciech Jamroga, and Peter Y.A. Ryan

of technology and social engineering to induce emotional reactions that would change

their decisions, and possibly swing the outcome of the vote (the Cambridge Analytica

scandal). In 2020, a large group of voters was targeted after the election by unfounded

claims that severely undermined the public trust in the outcome. In both cases, it is

impossible to understand the nature of what happened, and devise mitigation strategies,

without the focus on human incentives and capabilities.

Speciﬁcation and veriﬁcation of multi-agent systems. Multi-agent systems (MAS)

provide models and methodologies for the analysis of systems that feature interaction

of multiple autonomous components, be it humans, robots, and/or software agents. The

theoretical foundations of MAS are based on mathematical logic and game theory [

In particular, logic-based methods can be useful to formally specify and verify the

outcomes of multi-agent interaction [22].

Formal analysis with multi-agent logics is typically based on model checking [

The system is formalized through a network of graphs (or automata) that deﬁne its com-

ponents, their available actions, and the information ﬂow between them. The properties

are usually given as temporal properties, expressing that a given temporal pattern must

(or may) occur, or strategic properties capturing the strategic abilities of agents and their

groups. Especially the latter kind of properties are relevant for MAS; e.g., one may try

to capture voter-veriﬁability as the ability of the voter to verify her vote, and coercion-

resistance as the inability of the coercer to inﬂuence the behavior of the voter [

]. There

are many available model checking tools, though none of them is perfect. Some admit

only temporal properties [

], some focus on the less practical case of perfect information

strategies [

], and the others have limited veriﬁcation capabilities [

]. Moreover, it is

often unclear how to formalize an actual real-life scenario, including the “right” model

of the system [32] and the formal “transcription” of its desirable properties [34].

Socio-technical aspects of voting. In this paper, we use agent-based methodology to

propose and analyze a simple multi-agent model of an actual election, that combines

the technological backbone of the voting infrastructure with a model of possible human

behaviors. The work is preliminary, in the sense that we do not explore the real breadth

of participants’ activities that might occur during the vote. Moreover, we mostly look at

requirements that can be expressed as trace properties. This is because the computational

complexity of the formal analysis turned out prohibitive even for such simple models

and properties. We managed to mitigate the complexity by an innovative abstraction

technique, but seeing if it scales well enough for realistic models of human interaction

remains a subject for future work.

Case study: Polish postal vote of 2020. To focus on a concrete scenario, we consider

the Polish presidential election of 2020. That was the ﬁrst time when postal voting

was universally available in Poland. Unfortunately, the voting scheme was prepared

under 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 [

], chosen because of its ﬂexible model speciﬁcation language and user-

friendly GUI. As expected, the veriﬁcation of unoptimized models scales rather badly

Veriﬁcation of Socio-Technical Aspects of Voting 3

due to the state-space explosion. To improve the performance, we employ a recently

developed technique of user-friendly abstraction [31], with more promising results.

Related research. Formal veriﬁcation of voting protocols has been the subject of

research for over a decade. Prominent approaches include theorem proving in ﬁrst-

order, linear or higher order logic [

], and model checking of temporal,

strategic and temporal-epistemic logics [29,32,33]. Most if not all results show that the

task is very hard due to the prohibitive computational complexity of the underlying

problems. For example, [

] conducted a formal analysis of voting protocols using

ProVerif, and reported that they had to come up with workarounds for the model in order

to the limitations of the tool.

Modelling and analysis of socio-technical systems is even more difﬁcult because of

the vast space of possible human behaviors, and problematic nature of the assumptions

usually made about how users choose their actions. The theory of socio-technical systems

dates back to the work of Trist and Bamforth in 1940s. In security, perhaps the best

studied methodology is based on ceremonies [

], in particular the Concertina cere-

mony [

]. Some research has been also based on choreographies [

]. Moreover,

game-theoretic models and analysis have been used in [

]. Here, follow up on the

strand based on modeling and veriﬁcation in multi-agent logics [

], while trying

to put more emphasis on the social part of the system outside of the voting infrastructure.

When analyzing systems that involve human agents, it is important to take into

account that they behave differently from the machines, and can make errors, or more

generally, deviate from the prescribed protocol. This can happen due to a variety of rea-

sons: misunderstanding, inattentiveness, malicious intention, or strategic self-interested

action. Possible deviations from protocol in user behavior have been studied in [

], and

we follow up on those ideas. To this end, we use the skilled-human approach to capture a

variety of users’ behaviors in our model of postal voting. That is, we extend the protocol

speciﬁcation of an “honest” behaviour through a hierarchy of deviation sets, i.e., sets of

actions that deviate from the protocol and expand the repertoire of the participants. As

pointed out in [

], there is a trade-off between the breadth of the deviation model and

the computational feasibility of the formal analysis. In fact, our experiments in section 4

show that even for the skilled human approach only, the explicit state model checking

becomes hard enough, and dedicated techniques must be used to mitigate the complexity.

Related veriﬁcation tools. We use the Uppaal model checker [

] in our case study,

mainly because of its GUI and a ﬂexible system speciﬁcation language. Other veriﬁcation

tools that we considered when preparing the study are:

–

MCMAS [

]: a state-of-art OBDD-based symbolic model checker for agent-based

systems. The system is described using ISPL (Interpreted Systems Programming

Language), and the requirements are speciﬁed as formulae of strategic or temporal-

epistemic properties;

–

Tamarin-prover [

]: a tool for security protocol veriﬁcation and not a model checker

per se. The system speciﬁcation language is based on multiset rewriting theories, and

the requirements are speciﬁed as ﬁrst-order temporal properties;

–

STV [

]: an experimental toolbox for explicit-state model checking of strategic

properties; at the moment, custom input models are not fully supported and may lack

documentation;

4 Yan Kim, Wojciech Jamroga, and Peter Y.A. Ryan

–

ProVerif [

]: an automated cryptographic protocol veriﬁer, in the symbolic (Dolev-

Yao) model. The protocol representation is based on Horn clauses; it can be used for

proving secrecy, authentication and equivalence properties.

Among the above tools, only STV, Uppaal, and (to lesser extent) Tamarin provide a

graphical view of the system structure. Of those, only Uppaal allows for interactive

graphical system speciﬁcation, which we claim to be crucial in modelling and analysis

of voting protocols. Real-life voting procedures include the interaction of numerous

participants, each of them with a possibly different agenda and capabilities. Furthermore,

the behaviour of most participants is characterized with a mixture of controllable and

uncontrollable nondeterminism. In consequence, interactive GUI is crucial if we want

to ensure that the model we verify and the one we want to verify are the same thing,

cf. [32] for discussion.

Moreover, Uppaal (and, to a smaller extent, STV) allow for parameterized speciﬁca-

tion of the system, without forcing the designer to program a dedicated model-generator

(e.g., as in the veriﬁcation of SELENE protocol with MCMAS in [29]).

2 Postal Voting Procedure

Postal voting is one of the oldest forms for voting. In its simplest version, it is easy to

setup for the authorities and easy to follow for the voters. On the other hand, it can be

susceptible to ballot fraud, lacks veriﬁability, and opens up potential for vote buying and

coercion. What is more, only basic mechanisms of recovery are possible (e.g., cancelling

the whole elections in case of irregularities). This sometimes leads to controversial ad

hoc decisions when dealing with the irregularities [28].

The postal voting procedure employed for the Polish Presidential Election in 2020

is no exception. There was an overall impression that the procedure had been prepared

in haste [

] and with no proper research on the existing postal voting schemes that

were proposed and used during the last two decades, such as [

]. For example,

voter authentication is based on the assumption that a voter’s national identiﬁcation

number (PESEL) is secret, which is hardly the case in real life. Moreover, there are

various ways how authorities can delete votes, e.g., by sending invalid ballots to districts

with anti-government majority [

]. In this paper, we make the ﬁrst step towards

systematic modeling and analysis of this kind of threats.

2.1 Postal Voting Procedure for the 2020 Presidential Election

The rules for organizing the election of the President of Poland, with the possibility of

postal vote, were published on June 2 and June 3, 2020; the date of the election was set

to June 28, 2020. A complete list of legal acts deﬁning the election procedure can be

found in [

]. For the postal vote, the regulations (mostly concerning the time limits)

vary based on the voter’s location and her current quarantine status. We focus on the

non-expat and non-quarantined voters, but the protocol for the other types of voters is

nearly the same.

The protocol consists of several, partly overlapping phases: the setup which involves

expression of intention to vote by post, preparation and distribution of election packages

(EPs), casting of the vote, validation of votes, and tallying, see Figure 1.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

VerificationoftheSocio-TechnicalAspectsofVoting:TheCaseofthePolishPostalVote2020YanKim1,WojciechJamroga1,2,andPeterY.A.Ryan11InterdisciplinaryCentreforSecurity,Reliability,andTrust,SnT,UniversityofLuxembourg2InstituteofComputerScience,PolishAcademyofSciences,Warsaw,Poland{yan.kim,wojciech.jamroga,pe...

展开>> 收起<<

Verification of the Socio-Technical Aspects of Voting The Case of the Polish Postal Vote 2020 Yan Kim1 Wojciech Jamroga12 and Peter Y .A. Ryan1.pdf

共19页,预览4页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Verification of the Socio-Technical Aspects of Voting The Case of the Polish Postal Vote 2020 Yan Kim1 Wojciech Jamroga12 and Peter Y .A. Ryan1

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: