How to measure usable security: Natural strategies in voting protocols 1

Abstract

Formal analysis of security is often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the relevant security properties. In real life, this cannot be taken for granted. In particular, security mechanisms that are difficult and costly to use are often ignored by the users, and do not really defend the system against possible attacks.

Here, we propose a graded notion of security based on the complexity of the user’s strategic behavior. More precisely, we suggest that the level to which a security property φ is satisfied can be defined in terms of: (a) the complexity of the strategy that the user needs to execute to make φ true, and (b) the resources that the user must employ on the way. The simpler and cheaper to obtain φ, the higher the degree of security.

We demonstrate how the idea works in a case study based on an electronic voting scenario. To this end, we model the vVote implementation of the Prêt à Voter voting protocol for coercion-resistant and voter-verifiable elections. Then, we identify “natural” strategies for the voter to obtain voter-verifiability, and measure the voter’s effort that they require. We also consider the dual view of graded security, measured by the complexity of the attacker’s strategy to compromise the relevant properties of the election.

Keywords

Electronic voting coercion resistance natural strategies multi-agent models graded security

1. Introduction

Security analysis often focuses on the technological side of the system. It implicitly assumes that the users will duly follow the sequence of steps that the designer of the protocol prescribed for them. However, such behavior of human participants seldom happens in real life. In particular, mechanisms that are difficult and costly to use are often ignored by the users, even if they are there to defend those very users from possible attacks. This concerns the mental difficulty of handling the right behavior, as well as the costs in terms of time, money, computing power etc. necessary to obtain it.

For example, protocols for electronic voting are usually expected to satisfy receipt-freeness (the voter should be given no certificate that can be used to break the anonymity of her vote) and the related property of coercion-resistance (the voter should be able to deceive the potential coercer and cast her vote in accordance with her preferences) [9,21,23,38,40,48]. More recently, significant progress has been made in the development of voting systems that would be coercion-resistant and at the same time voter-verifiable, i.e., would allow the voter to verify her part of the election outcome [16,51]. The idea is to partly “crowdsource” an audit of the election to the voters, and see if they detect any irregularities. Examples include the Prêt à Voter protocol [50] and its implementation vVote [17] that was used in the 2014 election in the Australian state of Victoria.

However, the fact that a voting system includes a mechanism for voter-verifiability does not immediately imply that it is more secure and trustworthy. This crucially depends on how many voters will actually verify their ballots [57], which in turn depends on how understandable and easy to use the mechanism is [39,43]. Preliminary evidence suggests that, often, the number of voters who check if their votes have been cast as intended and recorded as cast is quite small [10,13,27]. The same probably applies to mechanisms that support coercion-resistance and receipt-freeness, and in fact to any optional security mechanism.If the users find the mechanism complicated and tiresome, and they can avoid it, they often avoid it.

Thus, the right question is often not only if but also how much security is obtained by the given mechanism. In this paper, we propose a graded notion of practical security based on the complexity of the strategic behavior, expected from the user if a given security property is to be achieved. More precisely, we suggest that the level to which property φ is “practically” satisfied can be defined in terms of: (a) the complexity of the strategy that the user needs to execute to make φ true, and (b) the resources that the user must employ on the way. The simpler and cheaper to obtain φ, the higher the degree of security. A similar observation applies to systems that are essentially vulnerable, i.e., no matter what the user does the attacker has a strategy to compromise the security property φ. In that case, we can talk about the practical degree of vulnerability by considering how complex a successful attack strategy must be and what resources it requires. In that view, the simpler and cheaper to compromise φ, the higher the degree of vulnerability.

Obviously, the devil is in the detail. It often works best when a general idea is developed with concrete examples in mind. Here, we do the first step, and look how voter-verifiability can be assessed in vVote and Prêt à Voter. To this end, we come up with a multi-agent model of vVote, inspired by interpreted systems [24]. We consider three main types of agents participating in the voting process: the election system, a voter, and a potential coercer. Additionally, we consider an intruder that can infect the voting machine with malware to eavesdrop and even change the votes being cast on the machine. Then, we identify strategies for the voter to use the voter-verifiability mechanism, and estimate the voter’s effort that they require. The strategic reasoning and its complexity is formalized by means of so called natural strategies, proposed in [34,35] and consistent with psychological evidence on how humans use symbolic concepts [11,25].

To illustrate reasoning about graded vulnerability, we look at how difficult it is to compromise the election through coercion. As it turns out, this requires a coalitional effort. Depending on the type of coercion, the coercer needs to team up with the voter or the eavesdropping intruder. Again, we identify coalitional strategies for coercion, and measure their complexity as well as necessary resources.

To create the models, we have used the Uppaal model checker for distributed and multi-agent systems [5], with its flexible modeling language and intuitive GUI. This additionally allows to use the Uppaal verification functionality and check that our natural strategies indeed obtain the goals for which they are proposed.

Related work. Formal analysis of security that takes a more human-centered approach has been done in a number of papers, for example with respect to insider threats [29]. A more systematic approach, based on the idea of security ceremonies, was proposed and used in [6–8,14,46], and applied to formal analysis of voting protocols in [45]. Here, we build on a different modeling tradition, namely on the framework of multi-agent systems. This modeling approach was only used in [30,31]. In [31], a preliminary verification of the Selene voting protocol was conducted. Moreover, [30] used Uppaal to model the basic variant of Prêt à Voter and conduct tentative model checking of some interesting temporal and temporal-epistemic properties. To our best knowledge, the idea of measuring the security level by the complexity of strategies needed to preserve a given security requirement is entirely new.

Other (somewhat) related works include socio-technical modeling of attacks with timed automata [19] and especially game-theoretic analysis of voting procedures [3,12,18,36]. Also, strategies for human users to obtain simple security requirements were investigated in [4]. Finally, specification of coercion-resistance and receipt-freeness in logics of strategic ability was attempted in [56].

A preliminary version of this article was published in the workshop paper [32].

2. Methodology

The main goal of this paper is to propose a framework for analyzing security and usability of voting protocols, based on how easy it is for the participants to use the functionality of the protocol and avoid a breach of security. Dually, we can also look at how difficult it is for the attacker to compromise the system. In this section we explain the methodology.

2.1. Modeling the voting process

The first step is to divide the description of the protocol into loosely coupled components, called agents. For each agent we define its local model, which consists of locations (i.e., the local states of the agent) and labeled edges between locations (i.e., local transitions). A transition corresponds to an action performed by the agent. An example model of the voter can be seen in Fig. 1. For instance, when the voter has scanned her ballot and is in the state $scanning$ , she can perform action $enter_vote$ , thus moving to the state $voted$ . This local model, as well as the others, has been created using the modeling interface of the Uppaal model checker [5]. The locations in Uppaal are graphically represented as circles, with initial locations marked by a double circle. The edges are annotated by colored labels, depicting preconditions (also called guards, in green), synchronizations (in teal) and updates (in blue). The syntax of expressions is similar to that of C/C++. Guards enable the transition if and only if the guard condition evaluates to true. Synchronizations allow processes to synchronize over a common channel. Update expressions are evaluated when the transition is taken.

Fig. 1.

Voter model.

The global model of the whole system consists of a set of concurrent processes, i.e., local models of the agents. The combination of the local models produces the global model, where each global state represents a possible configuration of the local states of the agents.

2.2. Natural strategic ability

Many relevant properties of multi-agent systems refer to strategic abilities of agents and their groups. For example, voter-verifiability can be understood as the ability of the voter to check if her vote was registered and tallied correctly. Similarly, receipt-freeness can be understood as the inability of the coercer, typically with help from the voter, to obtain evidence of how the voter has voted [56].

Logics of strategic reasoning, such as ATL and Strategy Logic, provide neat languages to express properties of agents’ behavior and its dynamics, driven by individual and collective goals of the agents [2,15,47]. For example, the ATL formula ${⟨ ⟨ cust ⟩ ⟩}_{} F ticket$ may be used to express that the customer $cust$ can ensure that he will eventually obtain a ticket, regardless of the actions of the other agents. The specification holds if $cust$ has a strategy whose every execution path satisfies $ticket$ at some point in the future. Strategies in a multi-agent system are understood as conditional plans, and play a central role in reasoning about purposeful agents [2,54]. Formally, strategies are defined as functions from sequences of system states to actions. The simpler notion of positional strategies, that we will use here, is defined by functions from states to actions. However, real-life processes often have millions or even billions of possible states, which allows for terribly complicated strategies – and humans are notoriously bad at handling combinatorially complex objects.

To better model the way human agents strategize, we proposed in [34,35] to use a more human-friendly representation of strategies, based on lists of condition-action rules. The conditions are given by Boolean formulas for positional strategies and regular expressions over Boolean formulas in the general case. Moreover, it was postulated that only those strategies should be considered whose complexity does not exceed a given bound. This is consistent with classical approaches to commonsense reasoning [20] and planning [26], as well as the empirical results on how humans learn and use concepts [11,25].

2.3. Natural strategies and their complexity

Natural strategies. Let $B ({Prop}_{a})$ be the set of Boolean formulas over atomic propositions ${Prop}_{a}$ observable by agent a. In our case, ${Prop}_{a}$ consists of all the references to the local variables of agent a, as well as the global variables in the model. We represent natural positional strategies of agent a by ordered lists of guarded actions, i.e., sequences of pairs $ϕ_{i} ⇝ α_{i}$ such that: (1) $ϕ_{i} \in B ({Prop}_{a})$ , and (2) $α_{i}$ is an action available to agent a in every state where $ϕ_{i}$ holds. Moreover, we assume that the last pair on the list is $⊤ ⇝ α$ for some action α, i.e., the last rule is guarded by a condition that will always be satisfied. In this way, we guarantee that at least one action is available in each state of the system. A collective natural strategy for a group of agents $A = {a_{1}, \dots, a_{| A |}}$ is a tuple of individual natural strategies $s_{A} = (s_{a_{1}}, \dots, s_{a_{| A |}})$ . The set of such strategies is denoted by $Σ_{A}$ .

By $length (s_{a})$ , we denote the number of guarded actions in $s_{a}$ . Moreover, ${cond}_{i} (s_{a})$ denotes the ith guard (condition) on the list, and ${act}_{i} (s_{a})$ the corresponding action. Finally, $match (q, s_{a})$ is the smallest $i ⩽ length (s_{a})$ such that $q ⊧ {cond}_{i} (s_{a})$ and ${act}_{i} (s_{a}) \in d_{a} (q)$ , where $d_{a} (q)$ are the available actions of agent a in state q. That is, $match (q, s_{a})$ matches state q with the first condition in $s_{a}$ that holds in q, and action available in q. The “outcome” function $out (q, s_{A})$ returns the set of all paths (i.e., all maximal traces) that occur when coalition A executes strategy $s_{A}$ from state q onward, and the agents outside A are free to act in an arbitrary way: $\begin{array}{rcl} out (q, s_{A}) & = & {λ = q_{0} q_{1} \dots ∣ (q_{0} = q) \land \forall_{i ⩾ 0} \exists_{α_{1}, \dots, α_{| A |}} . (a \in A \Rightarrow α_{a} = {act}_{match (q_{i}, s_{a})} (s_{a})) \land \\ (a \notin A \Rightarrow α_{a} \in d_{a} (q_{i})) \land (q_{i + 1} = succ (q_{i}, α_{1}, \dots, α_{| A |}))} \end{array}$ where $succ (q, α)$ is the successor state of state q given the tuple of actions α.

Complexity of strategies. We will use the following complexity metric for strategies: ${compl}_{} (s_{A}) = \sum_{(ϕ, α) \in s_{A}} | ϕ |$ , with $| ϕ |$ being the number of symbols in ϕ, without parentheses. That is, ${compl}_{} (s_{A})$ simply counts the total length of guards in $s_{A}$ .

Intuitively, the complexity of a strategy reflects its level of sophistication. Thus, it can be used to approximate the mental effort needed to come up with the strategy, memorize it, and execute it. Clearly, the approximation is not perfect, since the actual mental effort depends on the individual qualities of the agents, as well as the characteristics of the environment where the strategy is executed. For example, the interface of a voting system might present the voter with hints on how to verify one’s vote; in that case, the mental effort to follow the verification strategy is obviously smaller. Some psychological evidence suggests that the approximation is a step in the right direction [11,25]. A more accurate characterization might be obtained using the advances in the field of user experience (UX) [22,28,44]; we leave that path for future work.

2.4. Logical specification of natural ability

To reason about natural strategic ability, the logic $NatATL$ was introduced in [33,34] with the following syntax: $\begin{matrix} φ : : = p ∣ \neg φ ∣ φ \land φ ∣ {⟨ ⟨ A ⟩ ⟩}_{}^{⩽ k} ψ, ψ : : = X ψ ∣ F ψ ∣ G ψ ∣ ψ U ψ . \end{matrix}$ where A is a group of agents and $k \in N$ is a complexity bound. Intuitively, ${⟨ ⟨ A ⟩ ⟩}_{}^{⩽ k} ψ$ reads as “coalition A has a collective strategy of size less than or equal to k to enforce the temporal property ψ.” The formulas of $NatATL$ make use of classical temporal operators: “ $X$ ” (“in the next state”), “ $G$ ” (“always from now on”), “ $F$ ” (“now or sometime in the future”), and $U$ (strong “until”). For example, the formula ${⟨ ⟨ cust ⟩ ⟩}_{}^{⩽ 10} F ticket$ expresses that the customer can obtain a ticket by a strategy of complexity at most 10. This seems more appropriate as a functionality requirement than to require the existence of any function from states to actions.

Note that the standard strategic operator ${⟨ ⟨ A ⟩ ⟩}_{} ψ$ can be expressed in NatATL by ${⟨ ⟨ A ⟩ ⟩}_{}^{⩽ \infty} ψ$ . Moreover, the path quantifier “for all paths” from temporal logic can be defined as $A ψ \equiv {⟨ ⟨ \emptyset ⟩ ⟩}_{}^{⩽ 0} ψ$ .

In the rest of the paper, in addition to the classic atomic propositions, we will use for each atomic proposition p its persistent version, denoted by $\begin{matrix} p \end{matrix}$ . The idea is that, once proposition $p$ gets true for the first time, $\begin{matrix} p \end{matrix}$ also becomes true and remains true forever, even if $p$ changes its truth value to false again.

3. Specification and verification of voting properties based on natural strategies

$NatATL$ can be used to specify interesting properties of the voting system. In this section, we show tentative formalizations of such properties. We also discuss different levels of “strategic refinement”, and show at which level the graded notion of security can be derived. The focus is on (broadly understood) security properties, but the same pattern of reasoning can be applied to other kinds of requirements, such as usability.

3.1. How to specify voter-verifiability

The requirement of voter-verifiability captures the ability of the voter to verify what happened to her vote. In our case, this is represented by the $checkWBB$ phase, hence we can specify voter-verifiability with the formula ${⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F (checkWBB_ok \lor error)$ . The intuition is simple: the voter has a strategy of size at most k to successfully perform $checkWBB$ or else signal an error.

A careful reader can spot one problem with the formalization: it holds if the voter signals an error regardless of the outcome of the check (and it shouldn’t!). A better specification is given by ${⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F (checkWBB_ok \lor checkWBB_fail)$ , saying that the voter has a strategy of size at most k so that, at some point, she obtains either the positive or the negative outcome of $checkWBB$ .

3.2. Towards dispute resolution

We can use formula $A G (checkWBB_fail \to {⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F error)$ to connect the negative outcome of the check with the voter’s ability to report the problem. This property, which can be called “error signalling,” captures one aspect of dispute resolution. To characterize dispute resolution in full, we would need to significantly extend our model of the election. For instance, it would have to include a process that handles submitting the relevant evidence to the right authority (electoral commission, the judge, etc.), the deliberation and decision-making steps to be taken by that authority, and finally the way the final decision is to be executed (e.g., the election being declared void and repeated). We conjecture that dispute resolution would require not only more complex models than voter verifiability, but also higher mental complexity of the voter’s behaviour, i.e., more complex natural strategies to achieve it.

3.3. Strategic-epistemic specification of voter-verifiability

The above specification of voter-verifiability is rather technical and relies on appropriate labeling of model states (in particular, with propositions $checkWBB_ok$ and $checkWBB_fail$ ). On a more abstract level, one would like to say that the voter has a strategy to eventually know how her vote has been treated. Crucially, this refers to the knowledge of the voter. To capture the requirement, one can extend $NatATL$ with knowledge operators $K_{a}$ , where $K_{a} φ$ expresses that agent a knows that φ holds. For instance, $K_{voter} vote d_{i}$ says that the voter knows that her vote has been registered for the candidate i. Then, voter-verifiability could be re-formalized as: $\begin{matrix} {⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F \underset{i \in Cand}{⋀} (K_{voter} vote d_{i} \lor K_{voter} \neg vote d_{i}) . \end{matrix}$

3.4. Receipt-freeness

In that case, we want to say that the voter has no way of proving how she has voted, and that the coercer (or a potential vote-buyer) does not have a strategy that allows him to learn the value of the vote, even if the voter cooperates [38]: $\begin{matrix} \underset{i \in Cand}{⋀} \neg {⟨ ⟨ coerc, voter ⟩ ⟩}_{}^{⩽ k} F (end \land (K_{coerc} vot e_{i} \lor K_{coerc} \neg vot e_{i})) . \end{matrix}$

That means that the coercer and the voter have no strategy with complexity at most k to ensure that the coercer learns, after the election is finished, whether the voter has voted for i or not. Note that this is only one of the possible formalizations of the requirement. For example, one may argue that, to violate receipt-freeness, it suffices that the coercer can detect whenever the voter has not obeyed; he does not have to learn the exact value of her vote. This can be captured by the following formula: $⋀_{i \in Cand} \neg {⟨ ⟨ coerc, voter ⟩ ⟩}_{}^{⩽ k} F (end \land \neg vot e_{i} \land K_{coerc} \neg vot e_{i})$ . We note in passing that the related notion of vote anonymity can be specified as $⋀_{a \in Agents ∖ {voter}} ⋀_{i \in Cand} A G (\neg K_{a} vot e_{i} \land \neg K_{a} \neg vot e_{i}))$ .

3.5. Levels of strategic refinement

When talking about an important property of a voting system (such as receipt-freeness, voter-verifiability, and so on), one can consider at least three different conceptual variants, based on our assumptions about the strategic play of participating agents:

The temporal variant takes the temporal formula ψ, and requires that it is satisfied in all (resp. no) possible runs of the system. In other words, the model must satisfy the branching-time formula $A ψ$ (resp. $A \neg ψ$ ). For example, the temporal variant of voter-verifiability is $A F (checkWBB_ok \lor checkWBB_fail)$ , saying that the voter will eventually verify her vote on WBB, no matter what she (and anybody else) decides to do.

Similarly, the temporal variant of receipt-freeness is $A G \neg (end \land \neg vot e_{i} \land K_{coerc} \neg vot e_{i})$ , that is, it expresses the vote anonymity with respect to the knowledge of the coercer at the end of the election.

Typically, ψ captures a trace property (e.g., $F (checkWBB_ok \lor checkWBB_fail)$ ). However, it can also express an indistinguishability property by combining temporal and epistemic operators, cf. our formalizations of receipt-freeness and anonymity.

The strategic refinement takes ψ, and requires that it can (or cannot) be enforced by the relevant participants. Clearly, the temporal variant of voter-verifiability is too strong: we want to provide a mechanism so that the voter has the ability to verify her vote, and not that she is forced to do it. This is captured by the ATL formula ${⟨ ⟨ voter ⟩ ⟩}_{} F (checkWBB_ok \lor checkWBB_fail)$ .

The strategic refinement of receipt-freeness is constructed analogously by referring to the joint strategic ability of the voter and the coercer: $\neg {⟨ ⟨ coerc, voter ⟩ ⟩}_{} F (end \land \neg vot e_{i} \land K_{coerc} \neg vot e_{i})$ .

The graded strategic refinement takes ψ, and demands that it can (resp. cannot) be enforced by the relevant participants within the given mental complexity k. For example, ${⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F (checkWBB_ok \lor checkWBB_fail)$ can express that the voter has a simple strategy to verify her vote. This can be used to construct a graded notion of practical voter-verifiability.

Moreover, the formula $\neg {⟨ ⟨ coerc, voter ⟩ ⟩}_{}^{⩽ k} F (end \land \neg vot e_{i} \land K_{coerc} \neg vot e_{i})$ can be used to obtain a graded notion of vulnerability for receipt-freeness. This can be useful if there exists a successful attack to compromise the basic property ψ. In that case, we can still distinguish between systems that require different levels of complexity from the attacker.

Summarizing, one can talk about the basic property ψ (typically, a trace property or an indistinguishability property that is supposed to hold on all the executions of the system), its strategic variant where we only require that the relevant agent(s) have a strategy to enforce the basic property, and its graded refinement where we only allow for bounded strategies. Moreover, the latter level allows to parameterize the security property with arbitrary bounds on the complexity of strategic play.

3.6. Using verification tools to facilitate analysis

The focus of this work is on modeling and specification; the formal analysis is done mainly by hand. However, having the models specified in Uppaal suggests that we can also benefit from its model checking functionality. Unfortunately, the requirement specification language of Uppaal is very limited, and neither allows for strategic operators nor knowledge modalities [30]. That said it is still a very practical tool when it comes to creating the models, thanks to the well-designed graphical interface and extended modelling functionalities. Other existing model checking tools (such as MCMAS [42]) do not offer such functionalities, although they provide better requirement specification language. Still, we can use Uppaal to verify concrete strategies if we carefully modify the input formula and the model. We will show how to do it in Section 8.

We also remark that combining strategic and epistemic aspects poses a number of semantic problems [1,37]. In particular, one needs to choose the right notion of indistinguishability, and pair it with a matching type of strategies, available to the players. To avoid unnecessary distractions, in the rest of the paper we will concentrate on properties that use only strategic operators, such as the “technical” specification of voter-verifiability in Section 3.1.

4. Use case scenario: vVote

Fig. 2.

A vote printout in vVote [17].

Secure and verifiable voting is becoming more and more important for democracy to function correctly. In this case study, we analyze the vVote implementation of Prêt à Voter which was used for remote voting and voting of handicapped persons in the Victorian elections in November 2014 [17]. The main idea of the Prêt à Voter protocol focuses on encoding the vote using a randomized candidate list. In this protocol the ballot consists of two parts: the randomized order of candidates (left part) and the list of empty checkboxes along with the number encoding the order of the candidates (right part). The voter casts her vote in the usual way, by placing a cross in the right hand column against the candidate of her choice. Then, she tears the ballot in two parts, destroys the left part, casts the right one, and takes a copy of it as her receipt. After the election her vote appears on the public Web Bulletin Board (WBB)2

The WBB is an authenticated public broadcast channel with memory.

as the pair of the encoding number and the marked box, which can be compared with the receipt for verification. We look at the whole process, from the voter entering the polling station, to the verification of her vote on the Web Bulletin Board.

After entering the polling station, the Poll Worker (PW) authenticates the voter (using the method prescribed by the appropriate regulations), and sends a print request to the Print On Demand device (POD) specifying the district/region of the voter. If the authentication is valid (state $printing$ ) then the POD retrieves and prints an appropriate ballot for the voter, including a Serial Number (SN) and the district, with a signature from the Private Web Bulletin Board (PWBB). The PWBB is a robust secure database which receives messages, performs basic validity checks, and returns signatures. After that, the voter may choose to check and confirm the ballot. This involves demanding a proof that the ballot is properly formed, i.e., that the permuted candidate list corresponds correctly to the cipher-texts on the public WBB for that serial number. If the ballot has a confirmation check, the voter returns to the printing step for a new ballot (transition from state $check 1$ to $printing$ ).

Having obtained and possibly checked her ballot (state $has_ballot$ ), the voter can scan it by showing the ballot bar code to the Electronic Ballot Marker (EBM). Then, she enters her vote (state $scanning$ ) via the EBM interface. The EBM is a computer that assists the user in filling in a Prêt à Voter ballot. The EBM prints on a separate sheet the voter’s receipt with the following information: (i) the electoral district, (ii) the Serial Number, (iii) the voter’s vote permuted appropriately to match the Prêt à Voter ballot, and (iv) a QR code with this data and the PWBB signature, see Fig. 2.

Further, the voter must check the printed vote against the printed candidate list. In particular, she checks that the district is correct and the Serial Number matches the one on the ballot form. If all is well done, she can optionally check the PWBB signature, which covers only the data visible to the voter. Note that, if either $check 2$ or $check 3$ fails, the vote is canceled using the cancellation protocol. If everything is correct, the voter validates the vote, shreds the candidate list, and leaves the polling station. Finally, the voter can check her vote on the WBB after the election closes. She only needs to check the SN and the order of her preference numbers.

5. Models

In this section we present the model of a simplified version of vVote, focusing on the steps that are important from the voter’s perspective. We use Uppaal as the modeling tool because of its flexible modeling language and user-friendly GUI.

5.1. Voter model

The local model already presented in Fig. 1 captures the voter’s actions, from her potential interaction with the coercer, through entering the polling station and casting her vote, to going back home and verifying her receipt on the Web Bulletin Board. As shown in the graph, some actions (in particular the additional checks) are optional for the voter. Furthermore, to simulate realistic human behavior, we included some additional actions, not described by the protocol itself. For example the voter can try to skip even obligatory steps, such as $check 2$ . This is especially important, as $check 2$ may be the most time-consuming action for the voter and many voters may skip it in real life. To further simulate the real-life behavior of the voters, for each state we added a loop action labeled as $idle$ , to allow the voter to wait for as long as she wants. We omit the loops from the graph for the clarity of presentation. Note that the actions colored in teal represent the synchronization actions. Given an action a, the label “a?” means that the voter has to wait that another agent does a to go in the next state, while “ $a!$ ” means that when the voter selects a she determines also a transition in another local model. After every check, the voter can signal an error, thus ending up in the $error$ state. The state represents the situation when communication is triggered with the election authority, signaling that the voter could not cast her vote or a machine malfunction was detected.

5.2. Refinements of the voter model

The model shown in Fig. 1 is relatively abstract. For example, $checkWBB$ is shown as an atomic action, but in fact it requires that the voter compares data from the receipt and the WBB. In order to properly measure the complexity of the voter strategies, it is crucial to consider different levels of granularity.

Fig. 3.

Voter refinement: phase checkWBB.

Fig. 4.

Voter refinement: phase check2.

CheckWBB phase. Recall that this is the last phase in the protocol and it is optional. Here, the voter can check if the printed receipt matches her recorded vote on the WBB. This includes checking that the serial numbers match (action $check_serial$ ), and that the printed preferences order match the one displayed on the WBB (action $check_preferences$ ). If both steps succeed, then the voter reaches state $checkWBB_ok$ . The refined model for this phase is presented in Fig. 3.

Check2 phase. Other phases, such as $check 2$ , can be refined in a similar way. Recall that this is the only obligatory check phase; all the other ones are optional. Here, the voter should check that the printed receipt matches her intended vote. This includes checking that the serial numbers match (action $first_check$ ), and that the printed preferences match her intended vote arranged according to the candidate order on her ballot (action $second_check$ ). So, if both the steps succeed, then the voter checks that the district is correct. A refined model for this phase is shown in Fig. 4.

Fig. 5.

Voter refinement: serial number check. Label $check_serial (i)$ depicts checking the ith symbol of the serial number on the receipt and WBB.

Fig. 6.

Voter refinement: preferences order check. Label $check_number (i)$ refers to checking the ith position on the receipt and WBB.

Serial number phase. In some cases the model shown in Fig. 3 may still be too general. For example, the length of the serial number may have impact on the level of difficulty faced by the voter. To capture this, we split the step into atomic actions: $check_serial 1 (i)$ for checking the ith symbol on the WBB, and $check_serial 2 (i)$ for checking the ith symbol on the receipt. The resulting model is shown in Fig. 5, where n is the length of the serial number.

Preferences order phase. Similarly to comparing the two serial numbers, the verification of the printed preferences can also be troublesome for the voter. In order to make sure that her receipt matches the entry on the WBB, the voter must check each number showing her preference. Actions $check_number 1 (i)$ and $check_number 2 (i)$ refer to checking a number on the WBB and on the receipt, respectively. This is shown in the local model in Fig. 6, where m is the number of candidates in the ballot.

5.3. Voting infrastructure

The voter is not the only entity taking part in the election procedure. The election infrastructure and the electronic devices associated with it constitute a significant part of the procedure. Since there are several components involved in the voting process, we decided to model each component as a separate agent. The models of the Public WBB, Private WBB, the cancel station, the print-on-demand printer, and the EBM are shown in Figs 7–11.

Public WBB. In Fig. 7 we present the public WBB. Simply, this component displays a new information when it receives a new one. The action $send_to_wbb$ is synchronized with the Voter model and is executed after the voter has cast her vote.

Fig. 7.

Public WBB.

Fig. 8.

Private WBB.

Private WBB. In Fig. 8 we present the private WBB. Here, for each message received, the system component decides to sign or not to sign the message.

Cancel station. In Fig. 9 we present the cancel station. This component is a supervised interface for canceling a vote that has not been properly submitted or has not received a valid PWBB signature.

The three models described above have a very similar structure. In fact, each component waits for an external event and performs an action that returns in all the cases in the initial state.

Fig. 9.

Cancel station.

Fig. 10.

Print-on-demand printer.

Fig. 11.

Electronic Ballot Marker (EBM).

Print-on-demand printer. Fig. 10 models the behavior of the printing process. The initial state is $wait$ , where the printer stays idle until another agent sends a print request. Then, the printer checks whether the agent that has made the request has an account. If this is the case, then the printer prints the document, and returns to the waiting state. Otherwise, the printer does not accept the request and also returns to $wait$ .

EBM. Finally, in Fig. 11 we present the possible interactions of the Electronic Ballot Marker. At the beginning the EBM machine can be infected with the malicious software by the intruder. This is represented with the action $infect_vm$ synchronized with the Intruder model. Next, the EBM receives a ballot (event) and checks if the bar code is correct. If the check succeeds, the EBM waits for the voter to enter her vote (synchronized action $enter_vote$ ). If the machine has been infected, the vote is also sent to the intruder, which means that this action will be synchronized between the three agents at once, where the Voter plays the role of sender, and both the EBM and the Intruder receive the vote. In this scenario we only consider one type of infection, which results in leaking the vote to the intruder. Different types of infection, such as causing the malfunction of the device, are left for future work. The last step is to print the vote.

In all other cases the EBM passes through the $error$ state and then returns to the initial state ( $wait$ ).

5.4. Opponent model

To model the opponent, we first need to determine his exact capabilities. Is he able to interact with the voter, or only with the system? Should he have full control over the network, like the Dolev-Yao attacker, or do we want the agent to represent implicit coercion, where the relatives or subordinates are forced to vote for a specified candidate? Notice that there are two spheres of interaction for the opponent: one with the voter and another with the system. To capture these aspects, we split our threat model into two agents: the coercer and the intruder. The former is used to model the adversarial interaction with the voter (threatening the voter, forcing her to change her vote, and potentially punishing for disobedience). The latter is used to model the interaction with the system (infecting the voting machine with malware, eavesdropping for the content of the ballot, and relaying it to the coercer).

Thus, we use the modular approach to modeling, provided by Uppaal, in order to split the potential competences of the attacker into relevant subsets, and later combine them into appropriate threat models by looking at the abilities of sets of agents, i.e., coalitions. For example, the coercer that can only blackmail and punish is modeled by the singleton agent set ${coercer}$ , while one which can also compromise the privacy in the system can be referred to through the coalition ${coercer, intruder}$ .

Coercer model. The model of the coercer is depicted in Fig. 12. Starting from the initial state ( $start$ ), the coercer can remain in it by using the action $idle$ and can move to state $coerce$ by using the synchronized action $coerce (ca)$ . The latter action means that the coercer coerces the voter to vote for the candidate $ca$ . From $coerce$ , he can wait or request the ballot receipt from the voter. To do this, the voter must have finished her actions at the polling station and proceeded to direct communication with the coercer. From this point ( $request$ ) the next state depends on the coercer capabilities (in particular, whether he collaborates with the intruder). If he does, then the intruder notifies the coercer if the vote was cast for the candidate $ca$ (action $notify_ok$ ) or not (action $notify_not_ok$ ). If he does not, then the coercer executes action $move_next$ .

The next step depends on the voter’s choice. In fact, if she decides to give the receipt to the coercer then the next state will be ${share}_{i}, i = 1, 2, 3$ while if she decides not to give the receipt to the coercer then the next state will be ${nshare}_{i}, i = 1, 2, 3$ . Note that, in the latter situation, we capture also the cases in which the voter lost the receipt or she has not terminated the voting process. In the next step the coercer can decide to check the WBB (action $check_wbb$ ), or he can skip this step. Either way, the last action is to punish the voter or refrain from the punishment (actions $punish$ and $not_punish$ ). After that, the coercer remains in the last state of his module.

Fig. 12.

Coercer model. States $punish$ and $not_punish$ are duplicated for better readability.

Intruder model. The model of the intruder is depicted in Fig. 13. Starting from the initial state ( $start$ ), the intruder can remain in $start$ by using the action $idle$ or he can move forward by selecting his preferred candidate ( $select_candidate (ca)$ ). Further, he can move to the state $infection$ by using the action $infect_vm$ . The latter means that the intruder can infect and take control of the voting machine. From $infection$ , he can $idle$ or eavesdrop on the voting machine to capture the voter’s vote. In the latter case, the intruder compares the voter’s vote with his preferred candidate $ca$ . If the comparison shows the same candidate then the intruder proceeds to the state $ca = v$ and informs the coercer that the vote has been cast for the required candidate (action $notify_ok$ ). Otherwise he moves to the state $ca \neq v$ and informs the coercer about the discrepancy (action $notify_not_ok$ ). After that, the intruder remains in the last state of his module.

Fig. 13.

Intruder model.

6. Assessing the degree of voter-verifiability: Voter’s strategies and their complexity

There are many possible objectives for the participants of a voting procedure. A voter’s goal could be to just cast her vote, another one could be to make sure that her vote was correctly counted, and yet another one to verify the election results. The same goes for the coercer: he may just want to make his family vote in the way he instructs, or to change the outcome of the election. In order to define different objectives, we can use formulas of NatATL and look for appropriate natural strategies, as described in Sections 2 and 3. More precisely, we can fix a subset of the participants and their objective with a formula of NatATL, find the smallest strategy that achieves the objective, and compute its size. The size of the strategy will be an indication of how hard it is to make sure that the objective is achieved.

An example goal that the voter may want to pursue is the verification of her vote. Given the model in Fig. 1, we can use the formula $φ_{1} = {⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F (checkWBB_ok \lor checkWBB_fail)$ , as discussed in Section 3.

Note that it is essential to fix the granularity level of the modeling right. When shifting the level of abstraction, we obtain significantly different “measurements” of strategic complexity, i.e., different admissible values of k. This is why we proposed several variants of the voter model in Section 5. In this section, we will show how it affects the outcome of the analysis. To this end, we take a closer look at the previously defined models, and try to list possible strategies for the participants.

6.1. Strategies for the voter

In this section we focus on natural strategies for variants of voter-verifiability. Consider the following recipe for the voter’s behavior, aimed at making $φ_{1} = {⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F (checkWBB_ok \lor checkWBB_fail)$ true.

Natural Strategy 1.
A strategy for the voter is:
$start \lor check 2_ok \lor check 2_fail \lor outside_ps ⇝ move_next$

$polling_station ⇝ give_document$

$has_ballot ⇝ scan_ballot$

$scanning ⇝ enter_vote (v)$

$voted ⇝ check 2$

$cast ⇝ send_to_wbb$

$send ⇝ shred$

$shred ⇝ leave$

$check_request ⇝ not_share$

$checkWBB ⇝ checkWBB$

$⊤ ⇝ ⋆$

Recall that the above is an ordered sequence of guarded commands. The first condition (guard) that evaluates to true determines the action of the voter. Thus, if the voter has the ballot and she has not scanned it (proposition $has_ballot$ ), she scans the ballot. If $has_ballot$ is false and $scanning$ is true then she enters her vote, and so on. If all the preconditions except ⊤ are false, then she executes an arbitrary available action (represented by the wildcard ⋆).

In Natural Strategy 1, we have 11 guarded commands in which the command (1) costs 7 since in its condition there are seven symbols (four atoms plus three disjunctions), while the other guarded commands cost 1, so the total complexity is $1 \cdot 10 + 7 \cdot 1 = 17$ . So, the formula $φ_{1}$ is true with any k of 17 or more.

The next natural strategy comes with additional guarded commands in case the voter wants to do the optional phases $check 1$ and $check 3$ . The strategy aims to satisfy the formula $φ_{2} = {⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F (\begin{matrix} check 1 \end{matrix} \land \begin{matrix} check 3 \end{matrix} \land (checkWBB_ok \lor checkWBB_fail))$ which can be seen as a refinement of $φ_{1}$ . In particular, $φ_{2}$ asks if there exists a natural strategy for the voter such that sooner or later she has executed $check 1$ , $check 3$ , and verified her vote. Besides ordinary atomic propositions such as $check 1$ and $check 3$ , the formula uses also their persistent versions, denoted by $\begin{matrix} check 1 \end{matrix}$ and $\begin{matrix} check 3 \end{matrix}$ .
Natural Strategy 2.
A strategy for the voter that considers the optional phases $check 1$ and $check 3$ is:
$start \lor check 1 \lor check 3 \lor outside_ps ⇝ move_next$

$polling_station ⇝ give_document$

$has_ballot \land counter = = 0 ⇝ check_ballot$

$has_ballot ⇝ scan_ballot$

$scanning ⇝ enter_vote (v)$

$voted ⇝ check 2$

$check 2_ok \lor check 2_fail ⇝ check 3$

$cast ⇝ send_to_wbb$

$send ⇝ shred$

$shred ⇝ leave$

$check_request ⇝ not_share$

$checkWBB ⇝ checkWBB$

$⊤ ⇝ ⋆$

In Natural Strategy 2, we introduce the verification of $check 1$ and $check 3$ . To do this we add two new guarded commands (3) and (7), and update some clauses such as (1). Note that, in (3) we use a counter to determine if $check 1$ is done or not. This gives the total complexity of $1 \cdot 11 + 3 \cdot 2 + 7 \cdot 1 = 24$ . Thus, the formula $φ_{2}$ is true for any $k ⩾ 24$ .
6.2. Further refinements

An important aspect of the strategic complexity arises from a more detailed analysis of the $checkWBB$ phase. Some interesting questions are: how does the voter perform $checkWBB$ ? How does she compare the printed preferences with the information on the public WBB? These questions open up several scenarios both from a strategic point of view and for the model to be used. From the strategic point of view, we can consider a refinement of Natural Strategy 1, in which action $checkWBB$ is divided into several more primitive steps. If we consider that the $checkWBB$ includes: comparing preferences with the information in the public WBB and checking the serial number, we can already divide the single action into two different steps for each of the checks to be performed. Thus, given the model in Fig. 3, to verify that the voter does each step of $checkWBB$ , we need to provide a formula that verifies atoms $checkWBB_ok$ , $checkWBB .1_ok$ , and $checkWBB .2_ok$ . To do this in NatATL, we use the formula $φ_{3} = {⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F ((\begin{matrix} checkWBB_ok \end{matrix} \land \begin{matrix} checkWBB .1_ok \end{matrix} \land \begin{matrix} checkWBB .2_ok \end{matrix}) \lor checkWBB_fail \lor checkWBB .1_fail \lor checkWBB .2_fail)$ . Consequently, we refine the previous natural strategy of the voter as follows.

Natural Strategy 3.
A strategy for the voter that works in the refined model of phase $checkWBB$ is:
$start \lor check 2_ok \lor check 2_fail \lor outside_ps ⇝ move_next$

$polling_station ⇝ give_document$

$has_ballot ⇝ scan_ballot$

$scanning ⇝ enter_vote (v)$

$voted ⇝ check 2$

$cast ⇝ send_to_wbb$

$send ⇝ shred$

$shred ⇝ leave$

$check_request ⇝ not_share$

$checkWBB ⇝ check_serial$

$checkWBB_ok ⇝ ok$

$checkWBB .1 ⇝ check_preferences$

$checkWBB .1_ok ⇝ ok$

$checkWBB .2 ⇝ checkWBB$

$⊤ ⇝ ⋆$

In Natural Strategy 3, we have 15 guarded commands in which all the conditions are defined with a single atom but (1) in which there is a disjunction of four atoms. So, the total complexity is $1 \cdot 14 + 7 \cdot 1 = 21$ . So, $φ_{3}$ is true for any $k ⩾ 21$ ; one can use Natural Strategy 3 to demonstrate that.

In addition, to increase the level of detail, one could consider that the voter checks the preferences and the serial number one by one in an ordered fashion. So, given the models in Figs 5 and 6, we can consider a formula that checks whether the voter has a strategy that satisfies the following properties:

sooner or later she enters the $checkWBB$ phase;

she verifies the symbols of the SN on the public WBB against her receipt;

she does (2) until the last symbol of the serial number is verified;

she does a similar approach as in (2)-(3) for the verification of preferences;

she finishes the whole procedure.

This can be captured by the formula $φ_{4} = {⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F ((\begin{matrix} checkWBB \end{matrix} \land \begin{matrix} wbb_check_sn \end{matrix} \land \begin{matrix} receipt_check_sn \end{matrix} \land \begin{matrix} checkWBB .1 \end{matrix} \land \begin{matrix} wbb_check_pr \end{matrix} \land \begin{matrix} receipt_check_pr \end{matrix} \land \begin{matrix} checkWBB .2 \end{matrix}) \lor checkWBB_fail \lor checkWBB .1_fail \lor checkWBB .2_fail)$ . We can define a natural strategy that satisfies $φ_{4}$ , as follows.
Natural Strategy 4.
A strategy for the voter that still refines $checkWBB$ is:
$start \lor check 2_ok \lor check 2_fail \lor receipt_check_sn \lor receipt_check_pr \lor outside_ps ⇝ move_next$

$polling_station ⇝ give_document$

$has_ballot ⇝ scan_ballot$

$scanning ⇝ enter_vote (v)$

$voted ⇝ check 2$

$cast ⇝ send_to_wbb$

$send ⇝ shred$

$shred ⇝ leave$

$check_request ⇝ not_share$

$checkWBB ⇝ check_serial 1$

$wbb_check_sn ⇝ check_serial 2$

$receipt_check_sn \land i = = n ⇝ end_first$

$checkWBB_1 ⇝ check_number 1$

$wbb_check_pr ⇝ check_number 2$

$receipt_check_pr \land j = = m ⇝ end_second$

$checkWBB_2 ⇝ checkWBB$

$⊤ ⇝ ⋆$

To conclude, the above natural strategy has 17 guarded commands in which the conditions in (12) and (15) are conjunctions of two atoms, the condition in (1) is a disjunction of six atoms, and all the other conditions are defined with a single atom. Therefore, the complexity of Natural Strategy 4 is $1 \cdot 14 + 3 \cdot 2 + 11 \cdot 1 = 31$ . So, the formula $φ_{4}$ is true with $k ⩾ 31$ .
6.3. Counting other kinds of resources

So far, we have measured the effort of the voter by how complex strategies she must execute. This helps to estimate the mental difficulty related, e.g., to voter-verifiability. However, this is not the only source of effort that the voter has to invest. Verifying one’s vote might require money (for example, if the voter needs to buy special software or a dedicated device), computational power, and, most of all, time. Here, we briefly concentrate on the latter factor.

For a voter’s task expressed by the NatATL formula ${⟨ ⟨ voter ⟩ ⟩}_{}^{⩽ k} F φ$ and a natural strategy $s_{v}$ of the voter, we can estimate the time spent on the task by the number of transitions necessary to reach φ. That is, we take all the paths in $out (q, s_{v})$ , where q is the initial state of the procedure. On each path, φ must occur at some point. We look for the path where the first occurrence of φ happens latest, and count the number of steps to φ on that path. We will demonstrate how it works on the goals and strategies presented in Section 6.1.

For example, for Natural Strategy 3, starting from the initial state, the voter needs $11 + 5 = 16$ steps in the worst case to achieve $(\begin{matrix} checkWBB_ok \end{matrix} \land \begin{matrix} checkWBB .1_ok \end{matrix} \land \begin{matrix} checkWBB .2_ok \end{matrix}) \lor checkWBB_fail \lor checkWBB .1_fail \lor checkWBB .2_fail$ . More precisely, 11 steps are needed to achieve $checkWBB$ in the local model shown in Fig. 1, and 5 more steps to reach $checkWBB .2_ok \lor checkWBB .2_fail$ in the refinement of the final section of the procedure (see Fig. 3).

Similarly, the voter executing Natural Strategy 1 needs 12 steps to achieve the state $checkWBB_fail$ or the state $checkWBB_ok$ . Finally, Natural Strategy 2 requires 16 steps to conclude the verification of the voter’s vote.

6.4. Towards a graded view of usable security

In the preceding subsections, we have presented a sequence of formalizations for the requirement of voter-verifiability, each next one stronger and more detailed than the previous ones. Then, we presented natural strategies for the voter to bring about their strategic variants, and calculated the complexity of those strategies as well as the time (i.e., the number of steps) necessary to achieve the goal. Based on this, one may compare the degree of “usable voter-verifiability” for different variants $ψ_{1}$ , $ψ_{2}$ of the requirement, based on the standard notion of Pareto dominance. If each $ψ_{i}$ requires a strategy of complexity $ρ_{i}$ which achieves the goal in $ξ_{i}$ steps, and $ψ_{1}$ Pareto-dominates $ψ_{2}$ (that is, $ρ_{1} ⩽ ρ_{2}$ , $ξ_{1} ⩽ ξ_{2}$ , and at least one of the inequalities is strict), then $ψ_{1}$ is intuitively easier to achieve than $ψ_{2}$ .

For example, the basic property $ψ_{1} = F (checkWBB_ok \lor checkWBB_fail)$ has strategic complexity of 17 and needs of 12 steps, whereas $ψ_{2} = F (\begin{matrix} check 1 \end{matrix} \land \begin{matrix} check 3 \end{matrix} \land (checkWBB_ok \lor checkWBB_fail))$ has complexity 24 and needs of 16 steps, which suggests that, while the strategic variants of both $ψ_{1}$ , $ψ_{2}$ are satisfied in our model of vVote, the former presents the voter with a lighter burden. We note in passing that $ψ_{2}$ is strictly stronger than $ψ_{1}$ ; thus, it seems to promise a higher level of security. It introduces additional verification checks, which should make the system more verifiable. However, this results in higher complexity values, which suggests that the usable security of the system is reduced.

The same conceptual pattern can be employed to compare two different voting protocols with respect to a given security property ψ: if the characterization of protocol $P_{1}$ (in terms of strategic complexity and time) Pareto-dominates the characterization of protocol $P_{2}$ , then $P_{1}$ seems to have higher usable security towards ψ than $P_{2}$ . Of course, the problem with comparing different protocols is that, so far, our analysis is very sensitive to the level of abstraction and granularity in the modeling. This could be seen in Section 6.2 where a refinement of our model of vVote resulted in a (seemingly) higher complexity of voter’s strategies. How can one make sure that the security mechanisms being compared are modeled with the same granularity? We do not have an answer to this question yet. Clearly, without a common reference model (or metamodel), the numbers obtained in our computations are rather arbitrary. In this sense, our work is preliminary, and should be considered as the first step rather than a ready-to-use framework.

7. Quantifying the degree of vulnerability for coercion-resistance

In the previous section, we looked at the complexity of voters’ strategies for voter-verifiability. That is, we tried to estimate how hard it is for the voters to obtain a property which is, in principle, satisfied by the voting system. Now we will consider the alternative situation, namely properties for which no such strategy exists and, in fact, the potential attackers have a strategy to compromise it. In some cases, it makes sense to consider the complexity of the available attack strategies, and assess the mental effort required to exploit the vulnerability.

As it happens, the coercion-related vulnerabilities require cooperation of the coercer with another agent: either the eavesdropping intruder, or the voter herself. This can be nicely used to demonstrate how the complexity of coalitional play is quantified in the framework of natural strategies.

7.1. Natural strategies for the coalition of the coercer and the voter

We consider coalitional attack strategies against a weak variant of coercion-resistance, stating that “the coercer cannot obtain the receipt of the voter’s vote even if the voter cooperates with him.” The opposite of the property can be formalized as: $\begin{matrix} ψ_{1} = {⟨ ⟨ coerc, voter ⟩ ⟩}_{}^{⩽ k} F (share 1 \lor share 2 \lor share 3) . \end{matrix}$ While the receipts in Prêt à Voter and vVote do not reveal for whom the vote was cast, such a strategy can be used to construct a randomization attack [38]: it suffices that the coercer asks the voter to mark the first row in the ballot, no matter what the order of the candidates was, and later checks if the voter obeyed the instruction.

Appropriate natural strategies for the coalition ${coerc, voter}$ , aiming at property $ψ_{1}$ , are presented below.

Natural Strategy 5 (Coalitional strategy, the voter’s part).

$start \lor check 2_ok \lor check 2_fail ⇝ move_next$

$polling_station ⇝ give_document$

$has_ballot ⇝ scan_ballot$

$scanning ⇝ enter_vote$

$voted ⇝ check 2$

$cast ⇝ send_to_wbb$

$send ⇝ shred$

$shred ⇝ leave$

$check_request ⇝ share$

$⊤ ⇝ ⋆$

Natural Strategy 6 (Coalitional strategy, the coercer’s part).

$start ⇝ coerce (ca)$

$coerce ⇝ request$

$request ⇝ move_next$

$⊤ ⇝ ⋆$

In Natural Strategy 5, we have 10 guarded commands in which all the conditions are defined with a single atom except for (1) which is a disjunction of three atoms (and hence includes five symbols altogether). Thus, the total complexity is $1 \cdot 9 + 5 \cdot 1 = 14$ . Moreover, Natural Strategy 6 for the coercer has complexity 4 since it has three guarded commands with a single symbol. So, $ψ_{1}$ is true for any $k ⩾ 18$ .

We can also consider the case in which if the coercer does not receive the receipt from the voter he punishes her, otherwise he does not punish her. This property can be formalized as: $\begin{array}{rcl} ψ_{2} & = & {⟨ ⟨ coerc, voter ⟩ ⟩}_{}^{⩽ k} F (((\begin{matrix} share 1 \end{matrix} \lor \begin{matrix} share 2 \end{matrix} \lor \begin{matrix} share 3 \end{matrix}) \land not_punish \lor \\ ((\begin{matrix} nshare 1 \end{matrix} \lor \begin{matrix} nshare 2 \end{matrix} \lor \begin{matrix} nshare 3 \end{matrix}) \land punish . \end{array}$ For the voter, we can use again the Natural Strategy 5. The natural strategy for the coercer is presented below.

Natural Strategy 7 (Coalitional strategy, the coercer’s part).

$start ⇝ coerce (ca)$

$coerce ⇝ request$

$request ⇝ move_next$

$share 1 \lor share 2 \lor share 3 ⇝ not_punish$

$nshare 1 \lor nshare 2 \lor nshare 3 ⇝ punish$

$⊤ ⇝ ⋆$

Natural Strategy 7 for the coercer has complexity 14 since it has six guarded commands in which four of them have a single atom and the remaining two have a disjunction of three atoms. So, $ψ_{2}$ is true for any $k ⩾ 28$ .

7.2. Coalitional strategies with eavesdropping

Finally, we consider an important property stating that the coercing party can punish the voter if the voter disobeyed the coercer’s demand, and refrain from punishment otherwise. To capture that, we formally model the attacker by the coalition of the coercer and the intruder. More precisely, we specify the property by means of the formula: $\begin{matrix} ψ_{3} = {⟨ ⟨ coerc, intruder ⟩ ⟩}_{}^{⩽ k} F ((\begin{matrix} ok \end{matrix} \land not_punish) \lor (\begin{matrix} not_ok \end{matrix} \land punish) . \end{matrix}$

The natural strategies for the coalition are presented below.

Natural Strategy 8 (Coalitional strategy, the coercer’s part).

$start ⇝ coerce (ca)$

$coerce ⇝ request$

$share 1 \lor nshare 1 ⇝ not_punish$

$share 2 \lor nshare 2 ⇝ punish$

$⊤ ⇝ ⋆$

Natural Strategy 9 (Coalitional strategy, the intruder’s part).

$start ⇝ select_candidate (ca)$

$infection ⇝ infect_vm$

$capture ⇝ check_vote (v)$

$ca = v ⇝ notify_ok$

$ca! = v ⇝ notify_not_ok$

$⊤ ⇝ ⋆$

In Natural Strategy 8, we have 5 guarded commands in which all the conditions are defined with a single atom but (3) and (4) in which there are disjunctions of two atoms. So, the total complexity is $1 \cdot 3 + 3 \cdot 2 = 9$ . In Natural Strategy 9, we have 6 guarded commands in which all the guarded commands cost 1, so the total complexity is 6. So, the formula $ψ_{3}$ is true with any k of 15 or more.

7.3. Discussion

In Section 6, we argued that even if the system is in principle secure, its security is reduced by the complexity of the voter’s strategy. Here, we consider systems that are not secure in the first place. Still, it is sometimes worth looking at how hard it is to compromise the system. The validity of this kind of reasoning with respect to attack strategies depends on the underlying concept of the attacker. If we assume a powerful adversary who has (almost) unlimited resources and does not make mistakes, then the complexity of attack strategies plays a small role. On the other hand, many coercion scenarios involve human coercers who are neither skilled hackers nor good reasoners. In-house coercion by a family member is a prime example here. In that case, one may argue that the vulnerability is reduced by the complexity of the attacker’s strategy.

Another remark concerns the use of coalitional strategies in our analysis. A careful reader might have noticed that the coalitions considered in Sections 7.1 and 7.2 serve different purposes. The former refers to the cooperation of different participants of the voting process (the coercer and the voter in this case). The latter offers an neat way of modularizing the threat model: we distribute different potential capabilities of the attacker between different agents, and compose them by considering the relevant “coalition.”

8. Automated verification of strategies

In this section we explain how the model checking functionality of Uppaal can be used for an automated verification of the strategies presented in Section 6. To verify selected formulas and the corresponding natural strategies, we need to modify several things, namely: (i) the formula, (ii) the natural strategy, and finally (iii) the model. We explain the modifications step by step.

Formula. To specify the required properties for the protocol, we have used a variant of strategic logic, i.e., NatATL. Unfortunately, Uppaal supports neither NatATL nor plain ATL, but only a fragment of the branching-time temporal logic CTL. Thus, we cannot use Uppaal to model-check the formulas of Section 6. What we can do, however, is to verify if a given natural strategy achieves a given goal. To this end, we replace the strategic operator ${⟨ ⟨ A ⟩ ⟩}_{}^{⩽ k}$ in the formula with the universal path quantifier $A$ (“for all paths”). For example, instead of formula $φ_{1} \equiv {⟨ ⟨ v ⟩ ⟩}_{} F (checkWBB_ok \lor checkWBB_fail)$ we use $φ_{1}^{'} = A F (checkWBB_ok \lor checkWBB_fail)$ . At this point we do not differentiate between the persistent and standard propositions, as they are handled at the model level. Furthermore, we “prune” the model according to the given strategy, see below for the details.

Natural strategy. In order to efficiently merge the natural strategy with the model, the strategy should be modified so that all the guard conditions are mutually exclusive. To this end, we go through the preconditions from top to bottom, and refine them by adding (conjunctively) the negated preconditions from all the previous guards. Furthermore, if the strategy includes multiple entries $ϕ_{1} ⇝ α, \dots, ϕ_{k} ⇝ α$ for the same action α, they are all merged into a single entry: $ϕ_{1} \lor \dots \lor ϕ_{k} ⇝ α$ .

For example, Natural Strategy 1 becomes:

$has_ballot ⇝ scan_ballot$

$\neg has_ballot \land scanning ⇝ enter_vote$

$\neg has_ballot \land \neg scanning \land voted ⇝ check 2$

$\neg has_ballot \land \neg scanning \land \neg voted \land (check 2_ok \lor check 2_fail) ⇝ move_next$

$\neg has_ballot \land \neg scanning \land \neg voted \land \neg (check 2_ok \lor check 2_fail) \land cast ⇝ send_to_wbb$

$\neg has_ballot \land \neg scanning \land \neg voted \land \neg (check 2_ok \lor check 2_fail) \land \neg cast \land send ⇝ shred$

$\neg has_ballot \land \neg scanning \land \neg voted \land \neg (check 2_ok \lor check 2_fail) \land \neg cast \land \neg send \land shred ⇝ leave$

$\neg has_ballot \land \neg scanning \land \neg voted \land \neg (check 2_ok \lor check 2_fail) \land \neg cast \land \neg send \land \neg shred \land check_request ⇝ not_share$

$\neg has_ballot \land \neg scanning \land \neg voted \land \neg (check 2_ok \lor check 2_fail) \land \neg cast \land \neg send \land \neg shred \land \neg check_request \land checkWBB ⇝ checkWBB$

$\neg has_ballot \land \neg scanning \land \neg voted \land \neg (check 2_ok \lor check 2_fail) \land \neg cast \land \neg send \land \neg shred \land \neg check_request \land \neg checkWBB ⇝ ⋆$

Model. Semantically, a strategy of player a serves as a behavioral constraint that restricts the possible transitions in the module of a. To verify the selected strategy of the voter specified in the formula of NatATL, we merge the strategy with the voter model by adding the guard conditions from the strategy to the preconditions of the corresponding local transitions in the model. Thus, we effectively remove all the transitions that are not in accordance with the strategy.

This is done as follows: for every guarded command $ϕ ⇝ α$ in the strategy, find all the transitions in the module of the voter labeled by α and update their preconditions conjunctively with ϕ. That is, if the original precondition was ψ, it now becomes $ψ \land ϕ$ .

In consequence, only the paths that are consistent with the strategy will be considered by the model-checker. This of course requires the proper handling of the persistent propositions and variables. They need to be defined in the model in such way, that once the value is assigned to them, it will never be changed.

Levels of granularity. As we showed in Section 5, it is often important to have variants of the model for different levels of abstraction. To handle those in Uppaal, we have used synchronizations edges. For example, to have a more detailed version of the phase $checkWBB$ , we added synchronization edges in the voter model (Fig. 1) and in the $checkWBB$ model (Fig. 3). Then, when going through the $checkWBB$ phase in the voter model, Uppaal will proceed to the more detailed submodel, and come back after getting to its final state.

Automated script. The procedure described above is troublesome for larger models and prone to errors if executed manually. Because of that, we have created a script in Python to automatically modify the xml file with the Uppaal model according to the specified strategy. The script can be seen as an external plugin for Uppaal. The only additional requirement is that the action names used in the natural strategy must be put in the comments section of the corresponding transition. The script takes two parameters as input: the xml file containing the specification of the model, and the text file with the natural strategy as well as the name of the agent. The output is the modified xml file with added guards to the specified transitions. In case of a coalitional strategy, the tool needs to be run multiple times, once for each agent and its strategy. The script is available at https://github.com/blackbat13/stv/blob/development/stv/parsers/uppaal_parser.py.

Running the verification. Following the procedure explained before, we have modified models, formulas, and strategies from Section 6. To apply natural strategies to models we used an automated script. Then, we used Uppaal to verify that Natural Strategies 1–9 indeed enforce the prescribed properties, and measured the running time of the model checking procedure. We considered scenarios with two candidates, multiple voters, one coercer and one intruder. As the scaling factor we chose the number of the voters.

Table 1
Verification time in seconds of the formulas $φ_{1}, \dots, φ_{4}$

Voters $φ_{1}$ $φ_{2}$ $φ_{3}$ $φ_{4}$

1 <1 <1 <1 3

2 <1 <1 1 77

3 3 8 18 >120

4 58 >120 >120 >120

5 >120 >120 >120 >120

Voters	$φ_{1}$	$φ_{2}$	$φ_{3}$	$φ_{4}$
1	<1	<1	<1	3
2	<1	<1	1	77
3	3	8	18	>120
4	58	>120	>120	>120
5	>120	>120	>120	>120

Table 2

Verification time in seconds of the formulas $ψ_{1}$ , $ψ_{2}$ , and $ψ_{3}$

Voters	$ψ_{1}$	$ψ_{2}$	$ψ_{3}$	$ψ_{3} *$
1	<1	<1	>120	<1
2	<1	<1	>120	<1
3	<1	<1	>120	<1
4	<1	<1	>120	<1
5	<1	<1	>120	<1

Experimental results for strategies of the voter. We begin by discussing the performance of model checking for strategies of the voter. The results of the experiments are presented in Table 1. The columns refer to the number of voters and the verified formulas. The model checking time is given in seconds. The timeout was set to 120 s. The verification output for each formula was always the same: the property holds in the model.

As the results show, we were able to finish the verification within the timeout for up to 4 voters for the simplest formula $φ_{1}$ , and up to 2 voters for the formula $φ_{4}$ . The more complicated the formula or the model is, the more time it takes to finish the verification process. For example, verifying the formula $φ_{4}$ for 2 voters took more time than verifying the formula $φ_{1}$ for 4 voters. The explanation is simple: the Uppaal model considered in the formula $φ_{4}$ is more detailed, and includes more local states and transitions. Furthermore, it contains some (finite) loops in state templates (i.e., groups of related states, associated with the same node in the graph, but differing by the values of some underlying variables). Checking the serial number on the ballot is a good example of such a loop.

Experimental results for coalitional strategies. The second part of the experiments concerned coalition formulas $ψ_{1}$ , $ψ_{2}$ , and $ψ_{3}$ . The setting was the same as before: 2 candidates, one coercer, one intruder and a scalable number of voters. Without loss of generality, we assumed that the coercer can only interact with one arbitrarily chosen voter. This can be extended in a simple way by introducing several coercers or by adding new variables to the coercer model, that would hold the information about the coercer’s interactions with different voters. As previously, we prepared the models and the formulas, and ran the verification with Uppaal. The output of the verification was the same as before: the properties hold in the model, except for the formula $ψ_{3}$ (see below). The performance results are presented in Table 2.

As we can see, the verification times form a surprising pattern, compared to the previous set of experiments. Each time, the verification process took approximately 1 second, even for more voters. It seems that introducing new voters does not affect the verification time significantly when only one voter is interacting with the coercer. The reason may come from the fact that the other voters do not affect the actions of the chosen voter and the coercer.

For formula $ψ_{3}$ , Uppaal did not complete the verification within the assumed timeout. This was probably because the voter can infinitely loop on the check1 phase, within an infinite state template. That is, each transition in the loop increases the value of the unbounded variable $counter$ . Limiting the transitions along the loop to a finite number made Uppaal verify the property in under 1 second, which is presented in the column labeled by $ψ_{3} *$ .

9. Conclusions

Each voting protocol is designed to provide a certain set of functionalities to the voter. Consequently, in the analysis of a protocol, it is important to make sure that the voter has a strategy to use those functionalities. That is, she has a strategy to fill in and cast her ballot, verify her vote on the bulletin board, etc. However, this is not enough: it is also essential to see how hard that strategy is. In this paper, we propose a methodology that can be used to this end. One can assume a natural representation of the voter’s strategy, and measure its complexity as the size of the representation. Among other things, this can help to assess the difficulty associated with obtaining relevant security properties, such as voter-verifiability, receipt-freeness, and coercion-resistance.

In this paper, we make the first step towards a graded notion of security, based on the complexity of the participants’ strategies that must be used to obtain a given temporal or temporal-epistemic pattern. We identify three relevant levels of formalizing security that consist of the basic trace/indistinguishability property, its strategic refinement, and the graded variant of the strategic refinement from which the graded view of security can be derived. We also propose that, in case the security property does not hold on the strategic level, the graded refinement can provide means to assess how vulnerable the system is.

We mainly focus on one aspect of the voter’s effort, namely the mental effort needed to produce, memorize, and execute the required actions. We also indicate that there are other important factors, such as the time needed to execute the strategy or the financial cost of the strategy. This may lead to trade-offs where optimizing the costs with respect to one resource leads to higher costs in terms of another resource. Moreover, resources can vary in their importance for different agents. For example, time may be more important for the voter, while money is probably more relevant when we analyze the strategy of the coercer. Clearly, finding an optimal strategy in such settings may require to solve a multicriterial optimization problem [49,58], e.g., by identifying the Pareto frontier and choosing a criterion to select a point on the frontier. We leave a closer study of such trade-offs for future work.

We emphasize that the work presented in this paper is preliminary, and should be considered as the first step rather than a ready-to-use framework. It is evident from the presented examples that the numbers obtained in our computations are, to a large degree, arbitrary. We believe that the idea can be further developed into a more robust methodology. One way to proceed is to identify empirical experiments that help to assess some of the values in a psychologically meaningful way. To achieve this, we plan to harness the recent developments in User eXperience methods [22,28,44], for example the concept of forcing functions as a means to influence the user’s behavior by controlling their cognitive effort [55].

It would also be interesting to further analyze the parts of the protocol where the voter compares two numbers, tables, etc. As the voter is a human being, it is natural for her to make a mistake [4]. Consequently, the probability of making a mistake at each step can be added to the model to analyze the overall probability of successfully comparing two data sets by the voter. Then, the success level of a strategy can be computed, e.g., by using the probabilistic model checker PRISM [41].

Finally, we point out that the methodology proposed in this paper can be applied outside of the e-voting domain. For example, one can use it to study the usability of policies for social distancing in the current epidemic situation, and whether they are likely to obtain the expected results.

Footnotes

Acknowledgments

The authors thank the anonymous reviewers of STAST for their valuable comments. W. Jamroga and D. Kurpiewski acknowledge the support of the National Centre for Research and Development, Poland (NCBR), and the Luxembourg National Research Fund (FNR), under the PolLux/FNR-CORE projects VoteVerif (POLLUX-IV/1/2016) and STV (POLLUX-VII/1/2019).

References

Ågotnes,

Goranko,

Jamroga and

Wooldridge, Knowledge and ability, in: Handbook of Epistemic Logic,

H.P.

van Ditmarsch,

J.Y.

Halpern,

van der Hoek and

B.P.

Kooi, eds, College Publications, 2015, pp. 543–589.

Alur,

T.A.

Henzinger and

Kupferman, Alternating-time temporal logic, Journal of the ACM49 (2002), 672–713. doi:10.1145/585265.585270.

D.A.

Basin,

Gersbach,

Mamageishvili,

Schmid and

Tejada, Election security and economics: It’s all about eve, in: Proceedings of E-Vote-ID, 2017, pp. 1–20.

D.A.

Basin,

Radomirovic and

Schmid, Modeling human errors in security protocols, in: Computer Security Foundations Symposium, CSF, IEEE Computer Society, 2016, pp. 325–340.

Behrmann,

David and

K.G.

Larsen, A tutorial on uppaal, in: Formal Methods for the Design of Real-Time Systems: SFM-RT, LNCS, Vol. 3185, Springer, 2004, pp. 200–236. doi:10.1007/978-3-540-30080-9_7.

Bella and

Coles-Kemp, Layered analysis of security ceremonies, in: Information Security and Privacy Research – 27th IFIP TC 11 Information Security and Privacy Conference, Section 2012, Proceedings, Heraklion, Crete, Greece, June 4–6, 2012, IFIP Advances in Information and Communication Technology, Vol. 376, Springer, 2012, pp. 273–286. doi:10.1007/978-3-642-30436-1_23.

Bella,

Curzon,

Giustolisi and

Lenzini, A socio-technical methodology for the security and privacy analysis of services, in: COMPSAC Workshops, IEEE Computer Society, 2014, pp. 401–406.

Bella,

Curzon and

Lenzini, Service security and privacy as a socio-technical problem, J. Comput. Secur.23(5) (2015), 563–585. doi:10.3233/JCS-150536.

Benaloh and

Tuinstra, Receipt-free secret-ballot elections, in: Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing, ACM, 1994, pp. 544–553.

10.

Bernhard,

McDonald,

Meng,

Hwa,

Bajaj,

Chang and

J.A.

Halderman, Can voters detect malicious manipulation of ballot marking devices? in: IEEE Symposium on Security and Privacy, IEEE, 2020, pp. 679–694.

11.

L.E.

Bourne, Knowing and using concepts, Psychol. Rev.77 (1970), 546–556. doi:10.1037/h0030000.

12.

Buldas and

Mägi, Practical security analysis of e-voting systems, in: Proceedings of IWSEC, Lecture Notes in Computer Science, Vol. 4752, Springer, 2007, pp. 320–335.

13.

Burton,

Culnane and

S.A.

Schneider, Secure and verifiable electronic voting in practice: The use of vVote in the Victorian state election, 2015, CoRR arXiv:1504.07098.

14.

Carlomagno Carlos,

Everson Martina,

Price and

R.F.

Custódio, A proposed framework for analysing security ceremonies, in: SECRYPT, SciTePress, 2012, pp. 440–445.

15.

Chatterjee,

T.A.

Henzinger and

Piterman, Strategy Logic. Information and Computation208(6) (2010), 677–693. doi:10.1016/j.ic.2009.07.004.

16.

Cortier,

Galindo,

Küsters,

Müller and

T.T.

SoK, Verifiability notions for e-voting protocols, in: IEEE Symposium on Security and Privacy, 2016, pp. 779–798.

17.

Culnane,

P.Y.A.

Ryan,

S.A.

Schneider and

Teague, vvote: A verifiable voting system, ACM Trans. Inf. Syst. Secur.18(1) (2015), 3:1–3:30. doi:10.1145/2746338.

18.

Culnane and

Teague, Strategies for voter-initiated election audits, in: Decision and Game Theory for Security: Proceedings of GameSec, Lecture Notes in Computer Science, Vol. 9996, Springer, 2016, pp. 235–247.

19.

David,

Rydhof Hansen,

Guldstrand Larsen,

Legay,

M.C.

Olesen and

C.W.

Probst, Modelling social-technical attacks with timed automata, in: Proceedings of International Workshop on Managing Insider Security Threats, MIST, ACM, 2015, pp. 21–28.

20.

Davis and

Marcus, Commonsense reasoning, Communications of the ACM58(9) (2015), 92–103. doi:10.1145/2701413.

21.

Delaune,

Kremer and

Ryan, Coercion-resistance and receipt-freeness in electronic voting, in: Computer Security Foundations Workshop, 2006. 19th IEEE, IEEE, 2006, pp. 12.

22.

Distler,

M.-L.

Zollinger,

Lallemand,

P.B.

Rønne,

P.Y.A.

Ryan and

Koenig, Security – visible, yet unseen? in: Proceedings of Conference on Human Factors in Computing Systems, CHI, ACM, 2019, p. 605.

23.

Dreier,

Lafourcade and

Lakhnech, A formal taxonomy of privacy in voting protocols, in: Communications (ICC), 2012 IEEE International Conference on, IEEE, 2012, pp. 6710–6715. doi:10.1109/ICC.2012.6364938.

24.

Fagin,

J.Y.

Halpern,

Moses and

M.Y.

Vardi, Reasoning About Knowledge, MIT Press, 1995.

25.

Feldman, Minimization of Boolean complexity in human concept learning, Nature407 (2000), 630. doi:10.1038/35036586.

26.

Ghallab,

Nau and

Traverso, Automated Planning: Theory and Practice, Morgan Kaufmann, 2004.

27.

Gjøsteen and

A.S.

Lund, An experiment on the security of the Norwegian electronic voting protocol, Ann. des Télécommunications71(7–8) (2016), 299–307. doi:10.1007/s12243-016-0509-8.

28.

Hassenzahl and

Tractinsky, User experience-a research agenda, Behaviour & Information Technology25(2) (2006), 91–97. doi:10.1080/01449290500330331.

29.

Hunker and

C.W.

Probst, Insiders and insider threats – an overview of definitions and mitigation techniques, J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl.2(1) (2011), 4–27.

30.

Jamroga,

Kim,

Kurpiewski and

P.Y.A.

Ryan, Towards model checking of voting protocols in uppaal, in: Proceedings of E-Vote-ID, Lecture Notes in Computer Science, Vol. 12455, Springer, 2020, pp. 129–146.

31.

Jamroga,

Knapik and

Kurpiewski, Model checking the SELENE e-voting protocol in multi-agent logics, in: Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID), Lecture Notes in Computer Science, Vol. 11143, Springer, 2018, pp. 100–116.

32.

Jamroga,

Kurpiewski and

Malvone, Natural strategic abilities in voting protocols, in: Proceedings of STAST 2020, 2021, To appear.

33.

Jamroga,

Malvone and

Murano, Reasoning about natural strategic ability, in: Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), IFAAMAS, 2017, pp. 714–722.

34.

Jamroga,

Malvone and

Murano, Natural strategic ability, Artificial Intelligence277 (2019).

35.

Jamroga,

Malvone and

Murano, Natural strategic ability under imperfect information, in: Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019, IFAAMAS, 2019, pp. 962–970.

36.

Jamroga and

Tabatabaei, Preventing coercion in e-voting: Be open and commit, in: Electronic Voting: Proceedings of E-Vote-ID 2016, Lecture Notes in Computer Science, Vol. 10141, Springer, 2017, pp. 1–17. doi:10.1007/978-3-319-52240-1_1.

37.

Jamroga and

van der Hoek, Agents that know how to play, Fundamenta Informaticae63(2–3) (2004), 185–219.

38.

Juels,

Catalano and

Jakobsson, Coercion-resistant electronic elections, in: Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, ACM, 2005, pp. 61–70. doi:10.1145/1102199.1102213.

39.

Kulyk,

Volkamer,

Müller and

Renaud, Towards improving the efficacy of code-based verification in Internet voting, in: Financial Cryptography and Data Security Workshops, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 12063, Springer, 2020, pp. 291–309. doi:10.1007/978-3-030-54455-3_21.

40.

Küsters,

Truderung and

Vogt, A game-based definition of coercion-resistance and its applications, in: Proceedings of the 2010 23rd IEEE Computer Security Foundations Symposium, IEEE Computer Society, 2010, pp. 122–136. doi:10.1109/CSF.2010.16.

41.

Kwiatkowska,

Norman and

Parker, PRISM: Probabilistic symbolic model checker, in: Proceedings of TOOLS, Lecture Notes in Computer Science, Vol. 2324, Springer, 2002, pp. 200–204.

42.

Lomuscio,

Qu and

Raimondi, MCMAS: An open-source model checker for the verification of multi-agent systems, Int. J. Softw. Tools Technol. Transf.19(1) (2017), 9–30. doi:10.1007/s10009-015-0378-x.

43.

Marky,

Kulyk,

Renaud and

Volkamer, What did I really vote for? in: Proceedings of Conference on Human Factors in Computing Systems, CHI, ACM, 2018, p. 176.

44.

Marky,

M.-L.

Zollinger,

Funk,

P.Y.A.

Ryan and

Mühlhäuser, How to assess the usability metrics of e-voting schemes, in: Financial Cryptography Workshops, LNCS, Vol. 11599, Springer, 2019, pp. 257–271.

45.

Martimiano,

Dos Santos,

Olembo and

J.E.

Martina, Ceremony analysis meets verifiable voting: Individual verifiability in Helios, in: SECURWARE, 2015.

46.

Martimiano and

Everson Martina, Threat modelling service security as a security ceremony, in: 11th International Conference on Availability, Reliability and Security, ARES, IEEE Computer Society, 2016, pp. 195–204.

47.

Mogavero,

Murano,

Perelli and

M.Y.

Vardi, Reasoning about strategies: On the model-checking problem, ACM Transactions on Computational Logic15(4) (2014), 1–42. doi:10.1145/2631917.

48.

Okamoto, Receipt-free electronic voting schemes for large scale elections, in: Security Protocols, Springer, 1998, pp. 25–35. doi:10.1007/BFb0028157.

49.

Radulescu,

Mannion,

D.M.

Roijers and

Nowé, Multi-objective multi-agent decision making: A utility-based analysis and survey, Autonomous Agents and Multi Agent Systems34(1) (2020), 10. doi:10.1007/s10458-019-09433-x.

50.

P.Y.A.

Ryan, The computer ate my vote, in: Formal Methods: State of the Art and New Directions, Springer, 2010, pp. 147–184. doi:10.1007/978-1-84882-736-3_5.

51.

P.Y.A.

Ryan,

S.A.

Schneider and

Teague, End-to-end verifiability in voting systems, from theory to practice, IEEE Security & Privacy13(3) (2015), 59–62. doi:10.1109/MSP.2015.54.

52.

F.P.

Santos, Dynamics of Reputation and the Self-organization of Cooperation, PhD thesis, University of Lisbon, 2018.

53.

F.P.

Santos,

F.C.

Santos and

J.M.

Pacheco, Social norm complexity and past reputations in the evolution of cooperation, Nature555 (2018), 242–245. doi:10.1038/nature25763.

54.

Shoham and

Leyton-Brown, Multiagent Systems – Algorithmic, Game-Theoretic, and Logical Foundations, Cambridge University Press, 2009.

55.

Soegaard and

Friis Dam (eds), The Glossary of Human Computer Interaction, Interaction Design Foundation.

56.

Tabatabaei,

Jamroga and

P.Y.A.

Ryan, Expressing receipt-freeness and coercion-resistance in logics of strategic ability: Preliminary attempt, in: Proceedings of the 1st International Workshop on AI for Privacy and Security, PrAISe@ECAI 2016, ACM, 2016, pp. 1:1–1:8.

57.

Verified Voting. Policy on direct recording electronic voting machines and ballot marking devices, 2019.

58.

Zionts, A multiple criteria method for choosing among discrete alternatives, European Journal of Operational Research7(2) (1981), 143–147.

How to measure usable security: Natural strategies in voting protocols 1

Abstract

Keywords

1. Introduction

2. Methodology

2.1. Modeling the voting process

2.3. Natural strategies and their complexity

2.4. Logical specification of natural ability

3. Specification and verification of voting properties based on natural strategies

3.1. How to specify voter-verifiability

3.2. Towards dispute resolution

3.3. Strategic-epistemic specification of voter-verifiability

3.4. Receipt-freeness

3.5. Levels of strategic refinement

3.6. Using verification tools to facilitate analysis

4. Use case scenario: vVote

5.1. Voter model

5.2. Refinements of the voter model

6.1. Strategies for the voter

6.4. Towards a graded view of usable security

7. Quantifying the degree of vulnerability for coercion-resistance

7.1. Natural strategies for the coalition of the coercer and the voter

Natural Strategy 5 (Coalitional strategy, the voter’s part).

Natural Strategy 6 (Coalitional strategy, the coercer’s part).

Natural Strategy 7 (Coalitional strategy, the coercer’s part).

7.2. Coalitional strategies with eavesdropping

Natural Strategy 8 (Coalitional strategy, the coercer’s part).

Natural Strategy 9 (Coalitional strategy, the intruder’s part).

7.3. Discussion

8. Automated verification of strategies

Table 1 Verification time in seconds of the formulas φ 1 , … , φ 4 Voters φ 1 φ 2 φ 3 φ 4 1 <1 <1 <1 3 2 <1 <1 1 77 3 3 8 18 >120 4 58 >120 >120 >120 5 >120 >120 >120 >120

Footnotes

Acknowledgments

References

Table 1
Verification time in seconds of the formulas $φ_{1}, \dots, φ_{4}$

Voters $φ_{1}$ $φ_{2}$ $φ_{3}$ $φ_{4}$

1 <1 <1 <1 3

2 <1 <1 1 77

3 3 8 18 >120

4 58 >120 >120 >120

5 >120 >120 >120 >120