Is one vote really enough? Vote privacy with re-voting and a dishonest ballot box

Abstract

Electronic voting promises the possibility of convenient and efficient systems for recording and tallying votes in an election. To be widely adopted, ensuring the security of the cryptographic protocols used in e-voting is of paramount importance. However, the security analysis of this type of protocol raises a number of challenges, and they are often out of reach of existing verification tools. In this paper, we study vote privacy, a central security property that should be satisfied by any e-voting system. More precisely, we propose the first formalisation of the recent BPRIV notion in the symbolic setting. To ease the formal security analysis of this notion, we propose a reduction result allowing one to bind the number of voters and ballots needed to mount an attack. We first consider the case where voters do not revote, and the ballot box is trusted. Then, we extend this reduction result, as well as our formalisation of BPRIV, to account for the case of re-voting and a dishonest ballot box. We apply our reduction results to a number of case studies including several versions of Helios, Belenios, JCJ/Civitas, and Prêt-à-Voter. For some of these protocols, thanks to our result, we are able to conduct the analysis relying on the automatic tool Proverif.

Keywords

electronic voting formal methods protocol verification privacy

1. Introduction

Remote electronic voting systems aim at allowing the organisation of elections over the Internet, while providing the same guarantees as traditional paper voting. Although relying on e-voting for large-scale elections is controversial, it is already in use in many lower-stakes elections today (e.g. the Helios (1) voting system has been used to elect the IACR Board of Directors since 2010), and is likely to be used even more in the future, for better or for worse. These elections may involve a large number of voters and may have an important impact on democracy when it comes to electing political leaders. It is therefore of paramount importance to ensure the security of these systems.

As for security protocols, in general, formal methods provide powerful techniques to analyse e-voting systems and prove their security. Identifying what makes a good, secure e-voting system is a complex problem that has not yet been completely solved, and is actively being researched. It is, however, rather universally acknowledged that a central security guarantee e-voting systems should provide is vote privacy. Intuitively, this property states that votes must remain secret, so that no one can learn who voted for which candidate.

One common way of formalising vote privacy, which we will call SWAP, is to require that an attacker is not able to distinguish between the situation where Alice is voting yes and Bob is voting no from the situation where the two voters swapped their vote. That formalisation was first proposed by Benaloh and Yung (2), originally in a computational model. It has since been adapted to the symbolic setting (3), and applied to many voting schemes, for example, Backes et al. (4), Cortier and Smyth (5), Arapinis et al. (6), Cortier and Wiedling (7), Cortier et al. (8) and Basin et al. (9). The SWAP notion was originally written considering the specific case of a referendum, where the result is the number of yes and no votes. It has then been generalised to cover other kinds of elections (10), but remains limited w.r.t. the way of counting votes – essentially, it only makes sense when the result of the election is the number of votes for each candidate, excluding more complex counting procedures such as single transferable vote (STV).

More recently, a new definition, called BPRIV for ‘ballot privacy’, has been proposed to overcome such limitations, in the case of a trusted ballot box (11), with later extensions to handle an untrusted one (12). Essentially, BPRIV lets the attacker interact with the system, and see either real ballots or fake ones containing fake votes. Using oracles, he can choose the values of real and fake votes and cast any ballot he can construct (in the name of corrupted voters). In the end, the tally of real ballots is published. To be BPRIV, the attacker should be unable to distinguish the two scenarios, that is, no information is leaked on the ballots’ content.

Privacy-type properties, and in particular vote privacy, are often expressed using a notion of behavioural equivalence (13). A notable exception is the definition of $(α, β)$ -privacy (14), which nevertheless relies on some notion of static equivalence. Proving equivalences is cumbersome, and is difficult to do in detail by hand, as witnessed by the manual analysis of the SWAP property done for, for example, the Helios protocol (5) and the Norwegian one (7). Regarding mechanisation, several mature tools are available for analysing trace properties such as secrecy or authentication in the symbolic setting: most notably, Proverif (15; 16) and Tamarin (17). These tools support equivalence properties (18; 19), although they remain limited to a restricted form of equivalence, called diff-equivalence. Some e-voting schemes have been analysed with these automated tools in the symbolic model, for example, the Neuchâtel (8) or BeleniosVS (20) protocols. Proverif even has an extension called ProSwapper (21) that specifically handles swapped branches that typically occur in the SWAP definition. These tools have proved very helpful for the study of e-voting systems. However, they still suffer from limitations that restrict their applicability, as they, for example, cannot handle homomorphic encryption, or manipulate lists of arbitrary size to encode the bulletin board, and tend to quickly run into performance issues when the number of agents in parallel increases.

Contributions

Our goal here is to propose a methodology to enable the analysis of BPRIV. Our contributions are threefold.
(1)
First, we propose a definition of BPRIV adapted for the symbolic model. BPRIV has been first introduced in the computational setting where some subtleties regarding the communication model have been overlooked. In the computational setting, for instance, the casting of a ballot is handled by an oracle adding it to the ballot box. This means it is implicitly assumed that a ballot cast will necessarily reach the ballot box, and this is an important assumption when analysing weeding-based protocols (where duplicate ballots are eliminated before tallying).
(2)
Second, we identify some conditions under which BPRIV can be analysed considering only one honest voter and $k$ dishonest ones, casting at most $k$ ballots in total. The bound $k$ depends on a property of the procedure used to count votes which we define. Actually, in most usual cases, we have $k = 1$ , and the number of ballots being tallied is reduced to 1. These reduction results are generic, in particular, we do not restrict the equational theory, and our result applies to different counting functions. We first establish the reduction result in the setting where voters do not revote, and the ballot box is trusted. We then propose two extensions: we show the same result still holds when allowing revote, and when facing a dishonest ballot box. In the case of the untrusted ballot box, this requires us to propose an adaptation of the game-based definition of Cortier et al. (12) to the symbolic model.
(3)
Finally, we apply our result to several e-voting protocols from the literature relying on the tool Proverif. Even if our theoretical reduction results are generic, we are limited in practice by the features offered by the tools (e.g. homomorphic encryption is not supported by existing tools). Nevertheless, relying on Proverif, we successfully establish that BPRIV holds for an arbitrary number of voters in several cases.

Related work

Developing reduction results to ease protocol security analysis is not a new approach. For instance, this approach has been used to bound the number of agents involved in an attack for both reachability (22), and equivalence properties (23). Reduction results bounding the number of sessions (24; 25) have also been proposed in more restricted settings. All these results do not apply in the context of e-voting protocols. Here, we would like to bind the number of voters (agents) participating in the election. However, since only one vote is counted for each voter, we cannot replace a session played by $A$ by one played by $B$ , as was done, for example, in Cortier et al. (23).

The only existing result in that context is the result proposed in Arapinis et al. (6), where the authors give bounds on the number of voters and ballots – respectively, $3$ and $10$ – needed for an attack on the SWAP notion This allows them to carry out several case studies using Proverif. No such results, however, exist for the newer and more general BPRIV definition. Our bounds for BPRIV, better than those obtained in Arapinis et al. (6) when considering SWAP, allow us to analyse many protocols in a reasonable time (whereas several hours were needed in some cases in Arapinis et al. (6)). We also identify an issue in the security analysis performed in Arapinis et al. (6), where a protocol has been declared secure while it is not. An error in their reduction result led to an incorrect analysis of the Helios protocol in the presence of re-voting. This issue is discussed in Sections 5.3 and 7.2. Finally, we have chosen to consider a general notion of BPRIV involving an arbitrary number of honest participants (unlike the SWAP notion as studied in Arapinis et al. (6)). This introduces an additional challenge, which will be explained and detailed when establishing our first reduction result (see Section 4.3).

This paper is an extended version of our work (26), published at the 27^th ESORICS conference (2022): in particular, the BPRIV D definition as well as the reduction result established in Section 6 to deal with the case of a dishonest ballot box is entirely new.
2. Modelling security protocols

In this section, we introduce background notions on protocol modelling. We model security protocols in the symbolic model with a process algebra inspired by the applied pi calculus (27). Participants are represented by processes, while messages exchanged between participants are represented by terms. Our model is mostly standard, except that in order to model the stateful nature of e-voting protocols, we consider memory cells, that can store a persistent state across processes. We need to avoid concurrent accesses to memory cells while updating them: to that end, we use a specific instruction that atomically appends a message to the content of a memory cell.

2.1. Messages

We assume an infinite set $N$ of names used to model keys, nonces, etc. We consider two infinite and disjoint sets of variables $X$ and $W$ . Variables in $X$ are used to refer, for example, to input messages, and variables in $W$ , called handles, are used as pointers to messages learned by the attacker. Lastly, we consider two disjoint sets of constant symbols, denoted $Σ_{0}$ and $Σ_{e r r}$ . Constants in $Σ_{0}$ represent public values, for example, identities, nonces or keys drawn by the attacker. This set is assumed to be infinite. Constants in $Σ_{e r r}$ will typically refer to error messages. We fix a signature $Σ = Σ_{c} \cup Σ_{d}$ consisting of a finite set of function symbols together with their arity. We distinguish between constructors in $Σ_{c}$ and destructors in $Σ_{d}$ . We denote $Σ^{+} = Σ_{c} ⊎ Σ_{0} ⊎ Σ_{e r r}$ . We note $T (F, D)$ the set of terms built from elements in $D$ by applying function symbols in the signature $F$ . The set of names (respectively, variables) occurring in a term $t$ is denoted $n a m e s (t)$ (respectively, $v a r (t)$ ). A term $t$ is ground if $v a r (t) = \emptyset$ . We refer to elements of $T (Σ^{+}, N)$ as messages.

Example 1
We consider the signature $Σ_{e r r} = {{e r r}_{v o t e}, {e r r}_{i n v a l i d}}$ to model error messages. The signature $Σ_{l i s t} = {n i l, h d, t l, ::}$ allows us to model lists of arbitrary size. We often write $[t_{1}, \dots, t_{n}]$ for $t_{1} :: \dots :: t_{n} :: n i l$ . The operators $h d$ and $t l$ are used to retrieve the head and the tail of a list. Lastly, we consider $Σ_{e x} = {a e n c, a d e c, p k, z k p, {c h e c k}_{z k p}, t r u e, ⟨ ⟩_{3}, {p r o j}_{1}^{3}, {p r o j}_{2}^{3}, {p r o j}_{3}^{3}, y e s, n o}$ to model asymmetric encryption, zero-knowledge proofs, and pairing operators. As a running example, we will consider a model of the Helios protocol (in its original version, as seen in Cortier and Smyth (5)) and $Σ_{H e l i o s} = Σ_{e x} \cup Σ_{l i s t}$ , where symbols in $Σ_{H e l i o s}$ are constructors.

Let $i d_{H} \in Σ_{0}$ , $r, s k \in N$ , and $p k = p k (s k)$ . Intuitively, $i d_{H}$ represents the identity of an honest voter, and $y e s$ her vote (these data are known to the attacker), whereas $r$ and $s k$ are private names, modelling, respectively, the randomness used in the encryption and the private key of the authority. Let $e_{y e s} = a e n c (y e s, p k, r)$ and $b_{y e s}^{i d_{H}} = ⟨ i d_{H}, e_{y e s}, z k p (e_{y e s}, y e s, r, p k) ⟩_{3}$ . The first term encrypts the vote, and the second one is the ballot sent by the voter in the voting phase of Helios.

An element of $T (Σ^{+} \cup Σ_{d}, W)$ is called a recipe and models a computation performed by the attacker using his knowledge. A substitution $σ$ is a mapping from variables to messages, and $t σ$ is the application of $σ$ to term $t$ , which consists in replacing each variable $x$ in $t$ with $σ (x)$ . A frame $ϕ$ is a substitution that maps variables from $W$ to messages and is used to store an attacker’s knowledge.
Example 2
Continuing Example 1, we consider the equational theory $E_{e x}$ given below and $E_{l i s t} := {h d (x :: y) = x, t l (x :: y) = y}$ .
$E_{e x} = {\begin{matrix} a d e c (a e n c (x, p k (y), z), y) = x {p r o j}_{i}^{3} (⟨ x_{1}, x_{2}, x_{3} ⟩_{3}) = x_{i} with i \in {1, 2, 3} \\ {c h e c k}_{z k p} (z k p (a e n c (x, y, z), x, z, y), a e n c (x, y, z), y) = t r u e \end{matrix}} .$
We have $a d e c (e_{y e s}, s k) =_{E_{e x}} v$ and ${c h e c k}_{z k p} ({p r o j}_{3}^{3} (b_{y e s}^{i d_{H}}), v, r, p k) =_{E_{e x}} t r u e$ .

In order to provide a meaning to constructor symbols, we equip (constructor) terms with an equational theory. We assume a set $E$ of equations over $T (Σ_{c}, X)$ , and define $=_{E}$ as the smallest congruence containing $E$ that is closed under substitutions.

In addition, the semantics of destructor symbols is given by a set $R$ of ordered rewriting rules of the form $g (M_{1}, \dots, M_{n}) \to M_{0}$ with $M_{0}, M_{1}, \dots, M_{n} \in T (Σ_{c}, X)$ . A ground expression $D$ can be rewritten in $D^{'}$ if there is a position $p$ in $D$ , a rewrite rule $g (M_{1}, \dots, M_{n}) \to M_{0}$ and a substitution $θ$ from variables to ground terms such that $D |_{p} =_{E} g (M_{1} θ, \dots, M_{n} θ)$ , and $D^{'} =_{E} D [M_{0} θ]_{p}$ , that is, $D$ in which the subterm at position $p$ has been replaced with $M_{0} θ$ . In case more than one rule may be applied at position $p$ , only the first such rule can be effectively used. Moreover, we assume that the last rewriting rule defining a destructor $g$ is of the form $g (x_{1}, \dots, x_{n}) \to M_{0}$ with $x_{1}, \dots, x_{n}$ distinct variables, and thus always applies. Given a ground expression $D$ , it may be possible to rewrite it (in an arbitrary number of steps) into a ground (constructor) term $M$ : in that case, this term is noted $D ⇓$ , and we say that $D$ evaluates to $D ⇓$ . Note that, in our setting, a computation never fails.

We extend the notation $=_{E}$ to terms that may contain destructor symbols (that never fail). We write $u =_{E} v$ when $u ⇓ =_{E} v ⇓$ .
Example 3
Consider $Σ_{d} = {i t e}$ , where $i t e$ is a destructor symbol of arity $4$ that can be used to model conditional branching with the following ordered rewriting rules:
$\begin{array}{rclcrcl} i t e (x, x, y, z) & \to & y, & i t e (x, x^{'}, y, z) & \to & z . \end{array}$

The destructor defined in Example 3 may seem of little use, since it does not let an attacker compute any value he did not already know. It does indeed not bring extra power to the attacker. However, when dealing with the case of a dishonest ballot box, having such a construction will make it easier to write recipes used in our reduction result.

In the following, we consider an arbitrary signature $Σ = Σ_{c} \cup Σ_{d}$ , and we simply assume that the equational theory $E$ (equations built over $Σ_{c}$ only), contains at least the formalisation of lists given in Examples 1 and 2, that is, $Σ_{l i s t} \subseteq Σ$ and $E_{l i s t} \subseteq E$ .
2.2. Processes

We model protocols using a process calculus. We consider an infinite set of channel names $C h = {C h}_{p u b} ⊎ {C h}_{p r i}$ , partitioned into infinite sets of public and private channel names. We also assume an infinite set $M$ of names to represent memory cells (used to store states). The syntax of processes is:
$\begin{array}{rrl} P, Q & ::= & 0 \\ | & P | Q \\ | & ! P \\ | & n e w n . P \\ | & n e w d . P \end{array} \begin{aligned} | & o u t (c, u) . P \\ | & i n (c, x) . P \\ | & ! n e w d . o u t (c, d) . P \\ | & l e t x = u i n P \\ | & i f u = v t h e n P e l s e Q \end{aligned} \begin{aligned} | & m := u . P \\ | & r e a d m a s x . P \\ | & a p p e n d (c, u, m) . P \\ | & p h a s e i . P \end{aligned}$
where $n \in N$ , $x \in X$ , $m \in M$ , $u \in T (Σ^{+}, X \cup N)$ , $d \in {C h}_{p r i}$ , $c \in C h$ , and $i \in N$ .

This syntax is rather standard, except for the memory cell operations. Intuitively, $r e a d m a s x$ stores the content of $m$ in the variable $x$ , whereas $a p p e n d (c, u, m)$ represents the agent with channel $c$ appending $u$ to memory $m$ . In addition, we use a special construct $! n e w d . o u t (c, d) . P$ , to generate as many times as needed a new public channel $d$ and link it to channel $c$ , in a single step. This could be encoded using the other instructions, but having a separate construction lets us mark it in the execution traces, which is convenient for the proofs. The constructs $i n (c, x) . P$ , $l e t x = u i n; P$ , and $r e a d m a s x . P$ bind $x$ in $P$ . Note that destructor symbols are not allowed in the syntax of processes. In case the recipe used by the attacker contains such a destructor, the hypothesis that a computation never fails ensures that the resulting term is indeed a message. Given a process $P$ , $f v (P)$ denotes its free variables, and we say that it is ground when $f v (P) = \emptyset$ . Moreover, we usually omit the final $0$ in processes.

Example 4
Continuing our running example, we consider the process $P$ :
$\begin{array}{l} P = i n (c, b) . i f ⟨ {c h e c k}_{z k p} ({p r o j}_{3}^{3} (b), {p r o j}_{2}^{3} (b), p k (s k)), {p r o j}_{1}^{3} (b) ⟩ = ⟨ t r u e, i d_{D} ⟩ \\ t h e n o u t (c, b) . a p p e n d (c, b, m_{b b}) e l s e o u t (b, {e r r}_{i n v a l i d}) . \end{array}$
where $b \in X$ , $s k \in N$ , and $i d_{D} \in Σ_{0}$ . This represents an agent that receives a ballot $b$ as input and then checks the validity of the zero-knowledge proof contained in $b$ , as well as the identity of the voter. Depending on the outcome of this test, it either outputs the ballot and appends it in the cell $m_{b b}$ modelling the ballot box, or simply outputs an error message.
Definition 1
A configuration is a tuple $(i; P; ϕ; M)$ , composed of an integer $i$ , a multiset $P$ of ground processes, a frame $ϕ$ , and a mapping $M$ from a subset of memory names $M$ to messages. We write $P$ instead of $(0; P; \emptyset; \emptyset)$ .

The semantics of our calculus is defined as a transition relation $\Rightarrow a$ on configurations. Each transition step is labelled with an action $a$ representing what the attacker can observe when performing it (it can be an input, an output, an append action, or a silent action $ϵ$ ). This relation is defined in a standard manner and is fully displayed in Figure 1.

Figure 1.
Semantics of our calculus.

For instance, considering an input on a public channel, that is, the rule In, the attacker can inject any message $R ϕ$ he is able to build using his current knowledge $ϕ$ . The outputs performed on a public channel are made available to the attacker either directly through the label when it corresponds to an error message (rule Out-Err), or indirectly through the frame (rule Out). The rule Append corresponding to our new append action $a p p e n d (c, u, m)$ simply consists in appending a term $u$ to the memory cell $m$ .
Definition 2
The set of traces of a configuration $K$ is defined as $t r a c e s (K) = {(t r, ϕ) | \exists i, P, M such that K \Rightarrow {t r}^{⋆} (i; P; ϕ; M)}$ , where $\Rightarrow {t r}^{⋆}$ is the reflexive transitive closure of $\Rightarrow t r$ , concatenating all (non-silent) actions into the sequence $t r$ .
Example 5
Continuing Example 4 with $ϕ_{y e s} = {w_{0} \mapsto p k (s k), w_{1} \mapsto b_{y e s}^{i d_{H}}}$ , and the configuration $K_{0}^{y e s} = (2; {P}; ϕ_{y e s}; {m_{b b} \mapsto n i l})$ . We have:
$\begin{array}{rcl} K_{0}^{y e s} & \overset{i n (c, w_{1}) . o u t (c, {e r r}_{i n v a l i d})}{= = = = = = = = = = = = = = = = = = = ⟹} & (2; \emptyset; {w_{0} \mapsto p k (s k), w_{1} \mapsto b_{y e s}^{i d_{H}}}; {m_{b b} \mapsto n i l}) \\ K_{0}^{y e s} & \overset{i n (c, R_{0}) . o u t (c, w_{2}) . a p p e n d (c)}{= = = = = = = = = = = = = = = = = = = = = ⟹} & (2; \emptyset; {w_{0} \mapsto p k (s k), w_{1} \mapsto b_{y e s}^{i d_{H}}, w_{2} \mapsto b_{y e s}^{i d_{D}}}; {m_{b b} \mapsto b}) \end{array}$
with $R_{0} = ⟨ i d_{D}, {p r o j}_{2}^{3} (w_{1}), {p r o j}_{3}^{3} (w_{1}) ⟩_{3}$ , and $b_{y e s}^{i d_{D}} = R_{0} ϕ_{y e s}^{i d_{H}} =_{E_{e x}} ⟨ i d_{D}, e_{y e s}, z k p ⟩_{3}$ . The term $z k p$ here denotes the zero-knowledge proof from $b_{y e s}^{i d_{H}}$ . It does not contain the identity of the voter who computes it, and can therefore be reused by a dishonest voter to cast the ballot in her own name.
2.3. Equivalences

Our definition of the BPRIV property relies on two usual notions of equivalence in the symbolic model: static equivalence, for the indistinguishability of sequences of messages, and trace equivalence, for the indistinguishability of processes.

Definition 3
Two frames $ϕ$ and $ϕ^{'}$ are statically equivalent, denoted by $ϕ \sim ϕ^{'}$ , if $d o m (ϕ) = d o m (ϕ^{'})$ and for any recipes $R_{1}, R_{2} \in T (Σ^{+} \cup Σ_{d}, d o m (ϕ))$ , we have: $R_{1} ϕ =_{E} R_{2} ϕ \Leftrightarrow R_{1} ϕ^{'} =_{E} R_{2} ϕ^{'}$ .

When establishing our reduction result, we will reason on the notion of static equivalence. In particular, we will assume an attack trace exists, and that this attack comes from publishing the result of the election, that is, that the two processes are in trace equivalence until the result is output. In such cases, we will deduce that the results output by the tally on either side are different (modulo $E$ ). This result is formally stated and proved below and will be used in the proof of our main result.
Lemma 1
Let $t_{L}$ and $t_{R}$ be two public terms, that is, $t_{L}, t_{R} \in T (Σ_{c}, Σ_{0})$ . Let $ϕ_{L}, ϕ_{R}$ be two frames such that $ϕ_{L} \sim ϕ_{R}$ , and $w_{t a l l} \in W ∖ d o m (ϕ_{L})$ . We have: $ϕ_{L} \cup {w_{t a l l} \mapsto t_{L}} ≁ ϕ_{R} \cup {w_{t a l l} \mapsto t_{R}}$ if, and only if, $t_{L} \neq_{E} t_{R}$ .
Proof.
First, assume that $t_{L} \neq_{E} t_{R}$ . In such a case, let $M = w_{t a l l}$ and $N = t_{L} \in T (Σ_{c}, Σ_{0})$ . We have that the test $M = N$ holds in $ϕ_{L} \cup {w_{t a l l} \mapsto t_{L}}$ and not in $ϕ_{R} \cup {w_{t a l l} \mapsto t_{R}}$ . Indeed, we have that: $M ϕ_{L} = w_{t a l l} ϕ_{L} = t_{L} = N ϕ_{L}$ ; and $M ϕ_{R} = w_{t a l l} ϕ_{R} = t_{R} \neq_{E} t_{L} = N ϕ_{R}$ . Therefore, we have that $ϕ_{L} \cup {w_{t a l l} \mapsto t_{L}} ≁ ϕ_{R} \cup {w_{t a l l} \mapsto t_{R}}$ .

Now, we assume that $ϕ_{L} \sim ϕ_{R}$ , and $t_{L} =_{E} t_{R}$ . Consider w.l.o.g. a test $M = N$ that holds in $ϕ_{L} \cup {w_{t a l l} \mapsto t_{L}}$ . Let $M^{'} = M {w_{t a l l} \mapsto t_{L}}$ , and $N^{'} = N {w_{t a l l} \mapsto t_{L}}$ . Then, $M^{'} = N^{'}$ is a test that holds in $ϕ_{L}$ , and thus in $ϕ_{R}$ (thanks to our hypothesis $ϕ_{L} \sim ϕ_{R}$ ). Since, $t_{L} =_{E} t_{R}$ , we easily conclude that $M = N$ holds in $ϕ_{R} \cup {w_{t a l l} \mapsto t_{R}}$ . This allows us to conclude.

Trace equivalence is the active counterpart of static equivalence. Two configurations are in trace equivalence if, however, the attacker behaves, the resulting sequences of messages observed by the attacker are in static equivalence.
Definition 4
Two ground processes $P$ , $Q$ are in trace inclusion, denoted by $P ⊑_{t} Q$ , if for all $(t r, ϕ) \in t r a c e s (P)$ , there exists $ϕ^{'}$ such that $(t r, ϕ^{'}) \in t r a c e s (Q)$ and $ϕ \sim ϕ^{'}$ . We say that $P$ and $Q$ are trace equivalent, denoted by $P \approx_{t} Q$ , if $P ⊑_{t} Q$ and $Q ⊑_{t} P$ .
Example 6
We can consider a configuration $K_{0}^{n o}$ similar to $K_{0}^{y e s}$ but with $n o$ instead of $y e s$ in the initial frame. We can establish that $K_{0}^{n o} \approx_{t} K_{0}^{y e s}$ . This is a non-trivial equivalence. Now, let us replace $P$ with $P^{+}$ in both configurations, adding a simple process modelling the tally (for one vote), for example,

$P^{+} = P ∣ p h a s e 3. r e a d m_{b b} a s b b . l e t r e s = a d e c ({p r o j}_{2}^{3} (b b), s k) i n o u t (c_{r}, r e s)$ .

The resulting trace equivalence does not hold. This is simply due to the fact that $t r = i n (c, R_{0}) . o u t (c, w_{2}) . a p p e n d (c) . p h a s e 3. o u t (c_{r}, w_{3})$ can be executed starting from both configurations, and the resulting frames contain $w_{3} \mapsto n o$ on the left and $w_{3} \mapsto y e s$ on the right. This breach of equivalence is not, strictly speaking, an attack, as the processes do not formalise the BPRIV property. However, it follows the same idea as the ballot copy attack against Helios from Cortier and Smyth (5): a dishonest voter copies an honest voter’s ballot, introducing an observable difference in the result. This attack can be prevented by patching Helios, either by weeding out duplicate ballots from the ballot box or by adding the voter’s $i d$ to the ZKP, which then becomes invalid for any other voter.

In the following, we will consider action-deterministic configurations. Intuitively, for an action-deterministic configuration $K$ , once the trace $t r$ is fixed, the configurations that are reachable following the trace $t r$ are equal up to some $α$ -renaming.
Definition 5
A configuration $K$ is action-deterministic if for any $t r$ , any configurations $K_{1} = (i_{1}; P_{1}; ϕ_{1}; M_{1})$ and $K_{2} = (i_{2}; P_{2}; ϕ_{2}; M_{2})$ such that $K \Rightarrow t r K_{1}$ and $K \Rightarrow t r K_{2}$ , we have $i_{1} = i_{2}$ , and $ϕ_{1}$ and $ϕ_{2}$ are equal modulo $α$ -renaming of names generated during the execution.

Consider two ground processes $P$ and $Q$ whose associated configurations $(0; {P}; \emptyset; \emptyset)$ and $(0; {Q}; \emptyset; \emptyset)$ are action-deterministic. A witness of non-inclusion for $P ⋢_{t} Q$ is actually a trace $t r$ for which there exists $ϕ_{P}$ such that $(t r, ϕ_{P}) \in t r a c e s (P_{P})$ , and
either there does not exist $ϕ_{Q}$ such that $(t r, ϕ_{Q}) \in t r a c e s (P_{Q})$ ;

or such a $ϕ_{Q}$ exists and $ϕ_{P} ≁ ϕ_{Q}$ .

Indeed, once $t r$ is fixed, the resulting configuration is unique up to $α$ -renaming, thus there is no need to consider all the frames $ϕ_{Q}$ such that $(t r, ϕ_{Q}) \in t r a c e s (Q)$ to establish that they are not in static equivalence with $ϕ_{Q}$ . It is sufficient to consider one representative.
3. Modelling the general BPRIV notion

In this section, we present our formal model of e-voting protocols and our BPRIV privacy notion. While BPRIV itself is not novel, our symbolic formalisation is.

3.1. Modelling e-voting protocols

When modelling voting systems, we often need to encode some computations (e.g. performed by the ballot box) that cannot be represented by recipes (e.g. iterating through an arbitrary-sized list). We encode these computations as processes that do not share any names, channels, or memory cells with the rest of the process, except for a channel to return the result of the computation.

Definition 6
A computation is a process $C_{d} (\vec{p})$ without free names, channels, or variables (not counting those in $d$ , $\vec{p}$ ), without memory cell operations and phases. It is parametrised by a channel $d$ , and terms $\vec{p}$ , meant to be the channel where the result is output, and the terms are given as input parameters.

This process must be such that for all inputs $\vec{p}$ , there exists a ground term $t_{0}$ such that for all channel name $d$ , we have
$t r a c e s (C_{d} (\vec{p})) = {(ϵ, \emptyset)} \cup {(o u t (d, w), {w \mapsto t_{0}}) | w \in W} .$
We then call $t_{0}$ the result of the computation. As it does not depend on the channel, we will often omit it and let $C (\vec{p})$ denote the result.

To use such a process to compute a term inside a process $P$ , we will typically run it in parallel with an input waiting to retrieve the result on $d$ , followed by the continuation process. We will write it as a shortcut $l e t x = C (\vec{p}) i n P$ for $n e w d . (C_{d} (\vec{p}) | i n (d, x) . P)$ , where $d$ is a fresh private channel name (i.e. that does not appear anywhere else in the ambient process).

We assume a set $V o t e s \subseteq T (Σ, Σ_{0})$ of public ground terms representing the possible values of the votes. A voting system is modelled as a collection of processes that model the behaviour of voters, and a process representing the tallying authority. The election process is composed of several phases.

Phases 0 and 1: Setup. In the first two phases of the process, the election material is generated and published. More precisely, the election public key is published in the initial phase and the public credentials of voters in phase 1.

Phase 2: Casting. The voters send their ballots to the ballot box. In our model, a memory $m_{b b}$ will play the role of the ballot box, recording all ballots received by the voting server. This ballot box will be tallied at the end of the election. In fact, as we will see later on, when writing the BPRIV property, we will rather store the lists of ballots $(b b_{0}, b b_{o b s})$ in $m_{b b}$ , containing real and ‘observable’ (sometimes fake) ballots. The voters’ processes will first publish their ballot on a dedicated public channel, and then append it to the memory cell $m_{b b}$ . This models the fact that voters are authenticated when they submit their ballot, and the ballot cannot be modified on its way to the ballot box. While the attacker can modify messages on the public channel, he cannot directly access the memory cell, and thus he cannot impersonate the voter to submit a different ballot. However, the attacker is able to block a ballot before it reaches the ballot box.

Each voter has a private credential $c r \in N$ , with an associated public credential computed by a recipe $P u b (c r, u)$ , that may use a random value $u$ . Some protocols, such as Civitas, use this value to randomise the public credential, while others, such as Belenios, do not use it – in such cases, we can omit it. We will, in addition, use different channel names for the public channels used by each voter. This is more convenient when reasoning about traces, as it makes it easier to observe which voters have voted in a given trace.

To model the construction of ballots, we assume a recipe $V o t e$ with five variables: the term $V o t e (p k, i d, c r, v, r)$ represents a ballot generated for voter $i d$ with credential $c r$ , public election key $p k$ , randomness $r$ , and containing a vote $v$ .

When modelling vote privacy, the attacker chooses the vote $v$ he wants the voter to use to construct the ballot. Hence, we will need to check that $v$ is indeed a possible value for a vote, that is, $v \in V o t e s$ . If the set of candidates is finite, this can be tested exhaustively. In other cases, such as write-in votes, it can be done, for example, if legal votes have a specific format (start with a tag, etc.), or trivially if any value is legal. In a voting scheme, once a ballot is received by the voting server, another check is performed to ensure the ballot is valid, for example, correctly constructed. The exact nature of this validity test depends on the construction of the ballot, and thus on the protocol considered. Typically, it can consist of verifying signatures or zero-knowledge proofs included in the ballot. To keep our model generic, we simply assume a recipe $V a l i d$ with four variables: $V a l i d (i d, p c r, b, p k)$ represents the validity test performed for the agent $i d$ , whose public credential is $p c r$ , who submits a ballot $b$ . The term it computes is meant to be equal to $t r u e$ if, and only if, ballot $b$ cast by $i d$ is valid w.r.t. her public credential $p c r$ and the election public key $p k$ . We incorporate this validity check directly in the process of modelling the voter, before publishing and adding the ballot to $m_{b b}$ . In reality, it is performed by the ballot box, but this modelling choice is simpler (no need for an extra process) and closer to the cryptographic game (where the voting oracle performs the test).

The formal definition of the voter’s process is given in Section 3.2 as it incorporates elements specific to the modelling of the property.
Example 7
Continuing Example 2, for Helios, we use the following recipes:

$\begin{aligned} \begin{array}{rcl} {V o t e}_{H e l i o s} (p k, i d, v, r) & = & ⟨ i d, a e n c (v, p k, r), z k p (a e n c (v, p k, r), v, r, p k) ⟩_{3}, \\ [0.2 e m] {V a l i d}_{H e l i o s} (i d, b, p k) & = & {c h e c k}_{z k p} ({p r o j}_{3}^{3} (b), {p r o j}_{2}^{3} (b), p k) . \end{array} \end{aligned}$

Phase 3: Tallying. In the final phase, the $T a l l y (s k)$ process is in charge of reading the contents of the ballot box and using the key $s k$ to compute and publish the result on a dedicated channel $c_{r}$ . To leave it as generic as possible, we simply assume a computation $C_{T a l l y} (b b, s k)$ , that takes as parameters a list $b b$ of ballots, and $s k$ , and computes the result as specified by the protocol. We then assume the following form for $T a l l y$ :
$T a l l y (s k) = r e a d m_{b b} a s b b . l e t r e s = C_{T a l l y} (b b, s k) i n o u t (c_{r}, r e s) .$

Example 8
We continue Example 7 and we consider for simplicity the case of a referendum with two possible votes $y e s$ and $n o$ . We assume function symbols $z e r o / 0$ and $i n c r / 1$ , without any associated equations, that we use to count in unary. Slightly abusing notations with the use of pattern-matching in input, the tallying computation can be written as follows:
$\begin{aligned} C_{T a l l y} (b b, s k) = \\ n e w c . ( & o u t (c, ⟨ z e r o, z e r o, b b ⟩_{3}) \\ ∣ & i n (c, ⟨ x, y, n i l ⟩_{3}) . o u t (c_{r}, ⟨ x, y ⟩) \\ ∣ & ! i n (c, ⟨ x, y, ⟨ i d, b, p ⟩_{3} :: l) ⟩_{3}) . l e t v = a d e c (b, s k) i n \\ i f v = y e s t h e n o u t (c, ⟨ i n c r (x), y, l ⟩_{3}) e l s e o u t (c, ⟨ x, i n c r (y), l ⟩_{3}) .) . \end{aligned}$

3.2. A symbolic definition of BPRIV

We model vote privacy by adapting the BPRIV notion, originally formulated as a cryptographic game (11), to our symbolic setting. The idea remains the same as for the original notion: an attacker should not learn any information on the votes contained in the ballots, other than the final result of the election. This is modelled by letting the attacker suggest two possible values for the vote of each honest voter: a ‘real’ one and a ‘fake’ one. The attacker then sees the honest voters’ ballots, containing either the real or fake votes, and then in the end the real result of the election, computed on the real votes. We model the behaviour of honest voter $i d$ , who uses channel $c$ , private and public credentials $c r, p c r$ , and election public key $p k$ in these two scenarios by the two following processes:
$\begin{array}{rcl} \begin{array}{l} {H V o t e r}^{L} (c, i d, c r, p c r, p k) = \\ i n (c, z) . \\ l e t (v^{0}, v^{1}) = ({p r o j}_{1}^{2} (z), {p r o j}_{2}^{2} (z)) i n \\ i f v^{0}, v^{1} \in V o t e s t h e n \\ n e w r^{0} . n e w r^{1} . \\ l e t b^{0} = V o t e (p k, i d, c r, v^{0}, r^{0}) i n \\ l e t b^{1} = V o t e (p k, i d, c r, v^{1}, r^{1}) i n \\ i f V a l i d (i d, p c r, b^{0}, p k) = t r u e \\ t h e n o u t (c, b^{0}) . a p p e n d (c, b^{0}, m_{b b}) \\ e l s e o u t (c, {e r r}_{i n v a l i d}) \\ e l s e o u t (c, {e r r}_{v o t e}) . \end{array} & \begin{array}{l} {H V o t e r}^{R} (c, i d, c r, p c r, p k) = \\ i n (c, z) . \\ l e t (v^{0}, v^{1}) = ({p r o j}_{1}^{2} (z), {p r o j}_{2}^{2} (z)) i n \\ i f v^{0}, v^{1} \in V o t e s t h e n \\ n e w r^{0} . n e w r^{1} . \\ l e t b^{0} = V o t e (p k, i d, c r, v^{0}, r^{0}) i n \\ l e t b^{1} = V o t e (p k, i d, c r, v^{1}, r^{1}) i n \\ i f V a l i d (i d, p c r, b^{1}, p k) = t r u e \\ t h e n o u t (c, b^{1}) . a p p e n d (c, b^{0}, m_{b b}) \\ e l s e o u t (c, {e r r}_{i n v a l i d}) \\ e l s e o u t (c, {e r r}_{v o t e}) . \end{array} \end{array}$
In both cases, the process receives the two possible vote instructions $(v^{0}, v^{1})$ from the attacker, and constructs two corresponding ballots $b^{0}, b^{1}$ . It then tests for validity, and publishes, either the real $b^{0}$ (on the left) or the fake $b^{1}$ (on the right). However, since the result is always computed on the real votes, the ballot secretly added to the ballot box $m_{b b}$ is always $b^{0}$ . If any of the tests fail, we return error messages ${e r r}_{i n v a l i d}, {e r r}_{v o t e} \in Σ_{e r r}$ .

The attacker has complete control over the ballots submitted by dishonest voters. Hence, we model them by a process that receives an arbitrary ballot from the attacker, and adds it to the ballot box $m_{b b}$ after checking its validity:
$\begin{aligned} D V o t e r (c, i d, c r, p c r, p k) & = i n (c, b) . i f V a l i d (i d, p c r, b, p k) = t r u e \\ t h e n o u t (c, b) . a p p e n d (c, b, m_{b b}) e l s e o u t (c, {e r r}_{i n v a l i d}) . \end{aligned}$
To a reader used to symbolic modelling of protocols, it may seem strange that dishonest voters are modelled by a process, rather than being left completely under the control of the attacker. It may similarly be surprising that the voters’ processes include the validity checks and write directly to the ballot box, while these operations are not actually performed by the voter but by an independent entity (typically the server storing the ballot box). While not essential for our results, we decided to adopt this style of modelling to follow more closely the original formulation as a cryptographic game. In that formalism, the protocol and the scenario considered are modelled as oracles. The attacker has access to an oracle for each voter, and the oracle takes care of everything that happens when the voter votes. For honest voters, the attacker may submit two possible votes to the oracle, and the oracle constructs ballots accordingly, checks their validity, and records them in the ballot box. For dishonest voters, he may submit any ballot, and the oracle checks its validity and adds it to the box. Our symbolic processes are written in the same spirit: they should be seen as models of what happens when a voter votes, rather than directly models of the voter’s behaviour.

We then consider $n$ voters: for each $i \in ⟦ 1, n ⟧$ , we let $\vec{v_{i}} = (c_{i}, {i d}_{i}, {c r}_{i}, {p c r}_{i})$ , where $c_{i} \in {C h}_{p u b}$ is a dedicated public channel, ${i d}_{i} \in Σ_{0}$ is the voter’s identity, ${c r}_{i} \in N$ her private credential, and ${p c r}_{i} = P u b ({c r}_{i}, u_{i})$ her public credential randomised with $u_{i} \in N$ . We will say that for $i \neq j$ , $\vec{v_{i}}$ and $\vec{v_{j}}$ are distinct voters, to signify that they have different identities, credentials, and channels, that is, $c_{i} \neq c_{j} \land {i d}_{i} \neq {i d}_{j} \land {c r}_{i} \neq {c r}_{j} \land u_{i} \neq u_{j} \land u_{i} \neq {c r}_{j} \land {c r}_{i} \neq u_{j}$ .

We then define the BPRIV property as follows.

Definition 7
A voting scheme is BPRIV for $p$ honest voters and $n - p$ dishonest voters, written $B P R I V (p, n - p)$ , if ${E l e c t i o n}_{p, n - p}^{L} (\vec{v_{1}}, \dots, \vec{v_{n}}) \approx_{t} {E l e c t i o n}_{p, n - p}^{R} (\vec{v_{1}}, \dots, \vec{v_{n}})$ where
$\begin{array}{ll} {E l e c t i o n}_{p, n - p}^{X} (\vec{v_{1}}, \dots, \vec{v_{n}}) & = n e w s k . m_{b b} := n i l . o u t (c h, p k (s k)) . \\ (p h a s e 1. o u t (c_{1}, {p c r}_{1}) . p h a s e 2. {H V o t e r}^{X} (\vec{v_{1}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{p}, {p c r}_{p}) . p h a s e 2. {H V o t e r}^{X} (\vec{v_{p}}, p k (s k)) \\ | p h a s e 1. o u t (c_{p + 1}, ⟨ {c r}_{p + 1}, {p c r}_{p + 1} ⟩) . p h a s e 2. D V o t e r ({\vec{v}}_{p + 1}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{n}, ⟨ {c r}_{n}, {p c r}_{n} ⟩) . p h a s e 2. D V o t e r (\vec{v_{n}}, p k (s k)) \\ | p h a s e 3. T a l l y (s k)) \end{array}$
with $c h \in {C h}_{p u b}$ , $X \in {L, R}$ .

While we designed our symbolic definition to follow as closely as possible the original computational formulation of the property, there are two notable differences.

First, in the original notion, the oracle modelling honest voters was executed atomically: once the adversary submits his vote instructions, the generated ballot is immediately placed in the ballot box. In contrast, in our formalism, we allow executions where the process $H V o t e r$ is not executed until its end: the attacker could send vote instructions, receive the ballot on the public channel, and leave the process at that point, without executing the end, so that the ballot is never added to the ballot box. This difference is an important one, and is fully intentional: we wanted to model a scenario where the attacker can intercept and block ballots on their way to the ballot box. This gives him more power and thus makes for a stronger privacy property. A consequence of that choice, however, is that our definition is not suited to studying protocols that rely on weeding out duplicate ballots from the ballot box (e.g. some fixed versions of Helios). Indeed, the weeding operation only makes sense when assuming that all generated ballots have reached the ballot box – otherwise, some duplicates could be missed, if the original was blocked.

Second, many voting schemes include mechanisms allowing everyone to check that the tallying authority computed the result correctly. Typically, the talliers publish, alongside the result itself, zero-knowledge proofs showing that they, for example, correctly decrypted the ballots in the ballot box. In BPRIV, however, having them output this proof would immediately break the property. The proof only holds for the actual ballots being tallied, so the attacker could just check it against the ballots he saw, which would succeed on the left but fail on the right. The original formalisation handles this by using a simulator for the proof on the right. This sort of operation does not really have a counterpart in the symbolic model, and we decided (for now) to simply abstract this proof away and not model it.
3.3. Auxiliary properties

In (11), the authors propose two companion properties to BPRIV, called strong correctness and strong consistency. Together with BPRIV, they imply a strong simulation-based notion of vote privacy. Although we do not prove such a simulation – these are not really used in the symbolic model – we still define symbolic counterparts to the original computational side conditions. They are useful when establishing our reduction result, and we will from now on assume they hold.

Strong correctness. Honest voters should always be able to cast their vote, that is, their ballots are always valid. Formally, for any $i d, c r, r, u, s k \in Σ_{0} \cup N$ , $v \in V o t e s$ , we must have: $V a l i d (i d, P u b (c r, u), V o t e (p k (s k), i d, c r, v, r), p k (s k)) =_{E} t r u e$ .

Strong consistency. The tally itself should only compute the result of the election, and nothing else – it cannot accept hidden commands from the attacker coded as special ballots, etc. Formally, we assume two functions $e x t r a c t$ and $c o u n t$ :
$e x t r a c t (b, s k)$ is meant to extract the vote, and the voter’s $i d$ and credential from $b$ , using key $s k$ , or return $⊥$ if $b$ is not readable (ill-formed, etc.).

$c o u n t$ is the counting function, meant to compute the result from the list of votes. It is assumed to always return a public term in $T (Σ, Σ_{0})$ .

We assume that: if $V a l i d (i d, P u b (c r, u), b, p k (s k)) =_{E} t r u e$ then $e x t r a c t (b, s k) = (i d, c r, v)$ for some $v \in V o t e s$ . In other words, extraction always succeeds on valid ballots. Moreover, $e x t r a c t$ must behave as expected on honestly generated ballots, that is, $v = v_{0}$ when $b = V o t e (p k (s k), c r, v_{0}, r)$ . We let $e x t r a c t ([b_{1}, \dots, b_{n}], s k)$ be the list of non- $⊥$ values in $[e x t r a c t (b_{1}, s k), \dots, e x t r a c t (b_{n}, s k)]$ .

Lastly, we assume that these functions characterise the behaviour of the $C_{T a l l y}$ computation, that is, for all list $b b$ of messages, for all $s k \in N$ , we have:

$C_{T a l l y} (b b, s k) = c o u n t (l s t (e x t r a c t (b b, s k))),$
where $l s t$ is a function that only keeps the vote in each tuple returned by $e x t r a c t$ . Later on, when considering the case of a revote, $l s t$ will be replaced with a function applying a re-voting policy to determine which vote to keep for each voter.

Example 9
The $V a l i d$ recipe and $C_{t a l l y}$ computation from Examples 7 and 8 satisfy these assumptions, where $e x t r a c t$ simply decrypts the ciphertext in the ballot, and $c o u n t$ returns the pair of the numbers of votes for $y e s$ and $n o$ .
4. Reduction result

We first establish our reduction in the case where voters vote only once. Some systems allow voters to vote again by submitting a new ballot that will, for example, replace their previous one, in the interest of coercion-resistance. We extend our result to that setting in Section 5. Our BPRIV definition stated in Section 3 is parametrized by the number $n$ of voters among which $p$ are assumed to be honest. We prove our reduction result in two main steps. We first establish that it is enough to consider the case where $p = 1$ , that is, one honest voter is enough (see Section 4.3), and then we prove that the number of dishonest voters can be bounded as well (see Section 4.4). Before detailing these two parts, we first formally state our reduction result in Section 4.1, and we give in Section 4.2 a precise characterisation of an attack trace regarding the property BPRIV (when such a trace exists).

4.1. Main result

In order to reduce the number of dishonest voters needed to mount an attack against BPRIV, we need an additional assumption on the counting function used in the e-voting protocol. Roughly, as formally stated below, we have to ensure that when there is a difference in the result when considering $n$ votes, then a difference still exists when considering at most $k$ votes.

Definition 8
A counting function $c o u n t$ is $k$ -bounded if for all $n$ , for all lists $l_{t a l l y} = [v_{1}, \dots, v_{n}]$ and $l_{t a l l y}^{'} = [v_{1}^{'}, \dots, v_{n}^{'}]$ of size $n > k$ of elements in $V o t e s$ , such that $c o u n t (l_{t a l l y}) \neq_{E} c o u n t (l_{t a l l y}^{'})$ , there exist $k^{'} \leq k$ , and $i_{1} < \dots < i_{k^{'}}$ , such that $c o u n t ([v_{i_{1}}, \dots, v_{i_{k^{'}}}]) \neq_{E} c o u n t ([v_{i_{1}}^{'}, \dots, v_{i_{k^{'}}}^{'}])$ .

This assumption needed to establish our reduction results captures the most common counting functions such as multiset, sum, and majority presented below.

Multiset. The result is the multiset of all votes. Formally, in our setting, a term representing that multiset is computed: for all $n$ , ${c o u n t}_{#} ([v_{1}, \dots, v_{n}]) = f ({| v_{1}, \dots, v_{n} |)$ , where $f$ is a function such that $f (M_{1}) =_{E} f (M_{2})$ (equality on terms) iff $M_{1} =_{#} M_{2}$ (equality on multisets). For instance, if we just output the list of all votes, the order cannot matter, that is, ${c o u n t}_{#} ([a, b]) =_{E} {c o u n t}_{#} ([b, a])$ .

Sum. A total of points $t o t a l$ is given to each voter who decides to distribute them among the candidates of his choice. The result is a vector of integers representing the total of points obtained by each candidate. Assuming $c$ candidates, for all $n$ , we have: ${c o u n t}_{Σ} ([v_{1}, \dots, v_{n}]) = f (\sum_{i = 1}^{n} v_{i})$ where $v_{i} = (p_{1}, \dots, p_{c})$ with $1 \leq i \leq n$ , and $p_{1}, \dots, p_{c} \in N$ with $p_{1} + \dots + p_{c} \leq t o t a l$ , and $f$ is a function from vectors of $c$ integers to terms such that $f (\vec{u_{1}}) =_{E} f (\vec{u_{2}})$ (equality on terms) iff $\vec{u_{1}} = \vec{u_{2}}$ (equality on vectors of integers).

Majority. The majority function between two choices $y e s$ and $n o$ simply outputs $y e s$ if $# y e s > n / 2$ where $n$ is the number of votes, and $n o$ otherwise. For all $n$ , ${c o u n t}_{M a j} ([v_{1}, \dots, v_{n}]) = y e s$ if $# {i | v_{i} = y e s} > n / 2$ ; and ${c o u n t}_{M a j} ([v_{1}, \dots, v_{n}]) = n o$ otherwise. Here, $y e s$ and $n o$ are two public constants ( $y e s \neq_{E} n o$ ).
Lemma 2
The functions ${c o u n t}_{#}$ , ${c o u n t}_{Σ}$ and ${c o u n t}_{M a j}$ are $1$ -bounded.
Proof.
Let $[v_{1}, \dots, v_{n}]$ and $[v_{1}^{'}, \dots, v_{n}^{'}]$ be two lists of votes with $n > 1$ , such that ${c o u n t}_{#} ([v_{1}, \dots, v_{n}]) \neq {c o u n t}_{#} ([v_{1}^{'}, \dots v_{n}^{'}])$ . Since ${c o u n t}_{#}$ is a function, we have ${| v_{1}, \dots, v_{n} | \neq {| v_{1}^{'}, \dots, v_{n}^{'} |}$ , and thus there exists $i_{0}$ such that $v_{i_{0}} \neq v_{i_{0}}^{'}$ . Hence, $c o u n t ([v_{i_{0}}]) \neq c o u n t ([v_{i_{0}}^{'}])$ , which concludes the proof for ${c o u n t}_{#}$ . A similar reasoning applies for ${c o u n t}_{Σ}$ , and ${c o u n t}_{M a j}$ .

We can now state our main reduction theorem establishing that to study $B P R I V$ , it suffices to consider one honest voter, and at most $k$ dishonest ones, as soon as the counting function is $k$ -bounded.
Theorem 1
Let $V$ be a voting scheme whose associated counting function is $k$ -bounded for some $k \geq 1$ , and $p, n$ be two integers such that $1 \leq p \leq n$ . If $V$ does not satisfy $B P R I V (p, n - p)$ , then $V$ does not satisfies $B P R I V (1, k)$ . Moreover, in that case, there exists a witness of this attack where no more than $k$ ballots reached the ballot box.

This theorem is an easy consequence of Propositions 2 and Proposition 4 stated and proved in Section 4.3 and inSection 4.4.
Example 10
The ballot copy attack on Helios (with the 1-bounded multiset count) from Cortier and Smyth (5), mentioned in Example 6, can be performed against $B P R I V (p, n - p)$ : an honest voter is told to vote $y e s$ or $n o$ , her ballot is copied by a dishonest voter but remains valid, and the result is then ${| y e s, y e s |}$ on the left (as the ‘ $y e s$ ’ ballot was seen and copied), and ${| y e s, n o |}$ on the right (as the ‘ $n o$ ’ ballot was seen).

In accordance with Theorem 1, one honest voter, one dishonest, and one accepted ballot are actually sufficient: the attacker can simply block the honest ballot, so that only the copy is counted leading to ${| y e s |}$ on the left and ${| n o |}$ on the right, which suffices for the attack.
4.2. Characterisation of an attack trace

In the proofs in the next two sections (i.e. Sections 4.3 and 4.4), we will start with an attack trace on the election process involving $n$ voters, and show that an attack trace still exists considering less (honest) voters. To ease the proofs of these reduction results, we start by giving a precise characterisation of an attack trace (when such a trace exists). This characterisation is stated in Proposition 1. We first show that the election processes we study are action-deterministic.

Lemma 3
The two ground processes ${E l e c t i o n}_{p, n - p}^{L} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}})$ and ${E l e c t i o n}_{p, n - p}^{R} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}})$ are action-deterministic for any $n$ , and any $p \leq n$ .
Proof.
For these two processes, until phase $3$ , each process in parallel has its own public dedicated channel. Thus, the action mentioned on the trace $t r$ indicates which action will be triggered, there is no ambiguity, and it is therefore clear that the resulting frames are equal up to $α$ -renaming.

Now, when reaching phase $3$ , the process $T a l l y$ is a computation process that may involve private channels and thus leads to non-determinism. However, by definition of a computation process, we know that this process will result in a unique output on the public channel $c_{r}$ , and the value of this output only depends on the parameters given to the computation process, here $s k$ and the content of $m_{b b}$ . The content of $m_{b b}$ is entirely determined by $t r$ and the content of the frame. When considering the same trace $t r$ , we obtain frames, which are equal up to $α$ -renaming, and we will obtain the same public term for the tally.

We can now show that when considering an attack trace $t r$ , that is, a witness of non-inclusion between two election processes, the attack trace can be considered w.l.o.g. to be $Σ_{e r r}$ -free. That is, $t r$ does not contain any occurrence of $c_{e r r}$ for any $c_{e r r} \in Σ_{e r r}$ . We can also assume that the non-equivalence comes from static non-equivalence and that inputs in phase $2$ are messages representing valid voting options.
Proposition 1
Let $V$ be a voting scheme such that
${E l e c t i o n}_{p, n - p}^{L} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}}) ≉_{t} {E l e c t i o n}_{p, n - p}^{R} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}}) .$
Let $t r$ be a witness of this non-equivalence of minimal length. Then $t r$ is such that:
${E l e c t i o n}_{p, n - p}^{L} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{L}; P_{L}; ϕ_{L}; M_{L})$ for some $(i_{L}; P_{L}; ϕ_{L}; M_{L})$ ;

${E l e c t i o n}_{p, n - p}^{R} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{R}; P_{R}; ϕ_{R}; M_{R})$ for some $(i_{R}; P_{R}; ϕ_{R}; M_{R})$ ;

$i_{L} = i_{R}$ , $ϕ_{L} ≁ ϕ_{R}$ , and $t r$ is $Σ_{e r r}$ -free.
Moreover, for any $i \in {1, \dots, p}$ , if $i n (c_{i}, R)$ occurrs in $t r$ in phase 2 (for some $R$ ), then there exists $(v_{0}, v_{1}) \in V o t e s \times V o t e s$ such that $R ϕ_{L} =_{E} R ϕ_{R} =_{E} (v_{0}, v_{1})$ .
Proof.
Assume first that the minimal witness of this non-equivalence is actually a witness for the following non-inclusion: ${E l e c t i o n}_{p, n - p}^{L} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}}) ⋢_{t} {E l e c t i o n}_{p, n - p}^{R} (\vec{v_{1}}, \vec{v_{2}}, \dots, \vec{v_{n}})$ . As the processes under consideration are action-deterministic (Lemma 3), this witness is a trace $t r$ such that ${E l e c t i o n}_{p, n - p}^{L} (\vec{v_{1}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{L}; P_{L}; ϕ_{L}; M_{L})$ , and for which: (1)
there does not exist $(i_{R}; P_{R}; ϕ_{R}; M_{R})$ such that ${E l e c t i o n}_{p, n - p}^{R} (\vec{v_{1}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{R}; P_{R}; ϕ_{R}; M_{R})$ ; or
(2)
such a trace exists, that is, ${E l e c t i o n}_{p, n - p}^{R} (\vec{v_{1}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{R}; P_{R}; ϕ_{R}; M_{R})$ but $ϕ_{L} ≁ ϕ_{R}$ (note that we necessarily have that $i_{L} = i_{R}$ ).

We first assume that such a witness of minimal length satisfies the requirements stated in item (1), that is, there does not exist $(i_{R}; P_{R}; ϕ_{R}; M_{R})$ such that ${E l e c t i o n}_{1, n}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{R}; P_{R}; ϕ_{R}; M_{R})$ . Note that it means that, at some point, the outcome of a test is not the same on both sides, and this leads to an output that cannot be mimicked on the other side. When the test under consideration is public (i.e. corresponds to a computation that can be performed by the attacker), we get a contradiction since the trace $t r$ without its last output will already lead to a witness of non-inclusion. The only remaining case is the validity test performed by the honest voter but here we know that such a test cannot fail. Indeed, we have assumed strong correctness, that is:
$V a l i d (i d, P u b (c r, u), V o t e (p k (s k), i d, c r, v, r), p k (s k)) =_{E} t r u e .$
Therefore, we know that such a minimal witness is due to a problem regarding static equivalence: there exists $(i_{L}; P_{L}; ϕ_{L}; M_{L})$ such that ${E l e c t i o n}_{1, n}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{R}; P_{R}; ϕ_{R}; M_{R})$ but $ϕ_{L} ≁ ϕ_{R}$ .

It remains to establish that $t r$ can be considered to be $Σ_{e r r}$ -free. Assume that $t r$ contains an action of the form $o u t (c_{i}, c_{e r r})$ for some $c_{i}$ and some $c_{e r r} \in Σ_{e r r}$ . Then, the trace ${t r}^{'}$ without this action still passes on both sides and leads to the exact same frames. Indeed, in the processes considered, the errors are always placed at the end of a branch, and hence not executing them does not change the remaining trace. Therefore such an action cannot occur in a minimal witness.

Finally, for any honest voter $i$ , if $i n (c_{i}, R)$ occurs in $t r$ in phase 2, it must be that the test ‘ $i f v^{0}, v^{1} \in V o t e s$ ” succeeds on the left and eventually the corresponding output is performed, or the test fails on the left and eventually an error message is the output. In the first case, there exist $(v_{0}, v_{1}) \in {V o t e s}^{2}$ such that $R ϕ_{L} =_{E} (v_{0}, v_{1})$ , and thus by minimality of the witness $R ϕ_{R} =_{E} (v_{0}, v_{1})$ . In the second case, we have $R ϕ_{L} \neq_{E} (v_{0}, v_{1})$ for any $(v_{0}, v_{1}) \in {V o t e s}^{2}$ , and, again by minimality of the witness, $R ϕ_{R} \neq_{E} (v_{0}, v_{1})$ for any $(v_{0}, v_{1})$ . Since $t r$ is $Σ_{e r r}$ -free, we know that the corresponding error message is not output in the trace, but in this case, by minimality of $t r$ , we know that this input is not useful to get a witness of non-equivalence.
4.3. Reduction to one honest voter

When designing symbolic definitions that formalise security properties, even when an arbitrary number of participants are involved, a common modelling choice is to particularise the definition on a small number of honest agents, on which the property should hold. For instance, a key agreement property is often formalised by requiring that two fixed (but arbitrary) honest agents agree on the key at the end of their session, even in the presence of arbitrarily many dishonest agents. A more general definition would require that the same holds for any number of honest agents running the protocol in parallel, so that any two honest agents agree on a key once they finish a session together. The choice of fixing the honest agents when formalising the property produces a simpler property, with fewer honest sessions in parallel, which is usually easier on the automated tools. It is usually justified by arguing (more or less formally) that it implies the more general version: given an arbitrary number of honest agents, for any pair of agents, we can see from their point of view all other agents as potentially corrupted, and thus the simpler property applies and shows they agree.

A similar choice is implicitly made when considering the swapping definition for vote privacy. Indeed, the more general version would require that two scenarios, where the votes of any number of honest voters have been permuted, are always indistinguishable. This general formulation would in fact be closer to the one used in the computational setting. In contrast, the symbolic swapping definition considers two particular honest voters Alice and Bob, whose votes are exchanged. To justify this choice, it could be argued that, as any permutation can be decomposed in a finite sequence of swaps of two elements, by applying the seemingly weaker property as many times as needed, we can recover the general version. This argument is however not often formalised.

In order to remain faithful to the original computational BPRIV notion, and to define a strong privacy property, we decided to write our symbolic BPRIV property in a general way, that is, considering an arbitrary number of honest voters. Each voter receives two vote instructions $(v_{0}, v_{1})$ from the attacker, and shows him the ballot for one or the other. Reducing the number of honest voters by replacing them with dishonest ones is non-trivial as the behaviour of an honest voter cannot be mimicked by a dishonest one, or simply compensated by some steps performed by the attacker. This comes from the fact the behaviour of an honest voter is not exactly the same on both sides of the equivalence, as is the case for a dishonest voter. Nevertheless, we establish the following result: one honest voter is enough.

Proposition 2
Consider a voting scheme $V$ , and $p, n$ such that $1 \leq p \leq n$ . If $V$ does not satisfy $B P R I V (p, n - p)$ , then it does not satisfy $B P R I V (1, n - 1)$ .

The general idea of this proof is to show we can isolate one specific honest voter whose ballot is the one causing $B P R I V (p, n - p)$ to break. We then leave that voter as the only honest one and use dishonest voters to simulate the $p - 1$ others and obtain an attack against $B P R I V (1, n - 1)$ .

The difficulties are (i) how to find this particular voter and (ii) how to simulate honest voters with dishonest ones. The simulation would be easy for an honest voter $i d$ voting for the same candidate $v$ on both sides: simply use the dishonest voter to submit a ballot $V o t e (p k, i d, c r, v, r)$ for some random $r$ , and the correct credential $c r$ . However, in the $E l e c t i o n$ processes, $i d$ uses different values $v_{0}, v_{1}$ on the left and on the right, so that we cannot easily construct a single dishonest ballot simulating $i d$ ’s on both sides at the same time.

To solve both issues, the main idea is to go gradually from the ${E l e c t i o n}^{L}$ process, where all $H V o t e r$ s are ${H V o t e r}^{L}$ and use the real vote (their $v_{0}$ ), to the ${E l e c t i o n}^{R}$ process, where they are ${H V o t e r}^{R}$ and use the fake one (their $v_{1}$ ). We consider intermediate processes $P_{0}, \dots, P_{p}$ : as displayed in Figure 2, in $P_{i}$ , the first $i$ $H V o t e r$ s are ${H V o t e r}^{R}$ , and the others are ${H V o t e r}^{L}$ . Since $B P R I V (p, n - p)$ does not hold, $P_{0} = {E l e c t i o n}^{L}$ and $P_{p} = {E l e c t i o n}^{R}$ are not equivalent. Hence, there must exist some $i_{0}$ such that $P_{i_{0} + 1}$ and $P_{i_{0}}$ are not equivalent. These two processes differ only by the $i_{0} + 1^{th}$ $H V o t e r$ , who is ${H V o t e r}^{L}$ in $P_{i_{0}}$ , and ${H V o t e r}^{R}$ in $P_{i_{0} + 1}$ . This voter will be our particular voter, who will remain honest, solving issue (i). All other $H V o t e r$ s behave the same in $P_{i_{0}}$ and $P_{i_{0} + 1}$ : they vote with their right vote for the first $i_{0}$ , and their left for the last $p - i_{0} - 1$ . For them, issue (ii) is thus solved, and we can simulate them with dishonest voters. This way, we recover an attack with only one honest voter, and $(n - p) + (p - 1) = n - 1$ dishonest voters.

Figure 2.
Proof of Proposition 2 – intermediate processes $P_{i}$ .

Note that, in the case of the earlier reduction result from Arapinis et al.(6) for the SWAP definition, a simple version of vote privacy is used from the start. They consider only two honest voters who swap their votes, and not the general definition (as stated, e.g., in Benaloh(10) and Bernhard et al.(11)) involving an arbitrary permutation between an arbitrary number of honest voters. Due to this, in (6), this first step was trivial. The argument in our case is more involved, as we start from the general notion.

Before proving the reduction result, let us first observe that since the $V a l i d$ recipe and the $C_{T a l l y}$ computation process do not use any private names, and always return public values, their output cannot depend on the random values used in the ballots/credentials. More precisely, these random values can be renamed and/or replaced with public fresh names without changing the outcome of $V a l i d$ or $C_{T a l l y}$ . This property, which we will refer to as randomness independence, is a direct consequence of the construction of terms and semantics of processes in our symbolic model. We will use it in the proof of the reduction theorem, and for this reason, we state it formally below.
Lemma 4
Consider a key $s k \in N$ , with the associated $p k = p k (s k)$ , and $n$ distinct voters ${i d}_{1}, \dots, {i d}_{p}, {i d}_{p + 1}, \dots, {i d}_{n} \in Σ_{0}$ , meant to represent $p$ honest voters and $n - p$ dishonest ones, each with their credential ${c r}_{i} \in N$ . Let $ϕ_{0}$ denote the frame of public keys and credentials
$\begin{aligned} ϕ_{0} = { & w_{0} \mapsto p k, w_{1} \mapsto P u b ({c r}_{1}, u_{1}), \dots, w_{p} \mapsto P u b ({c r}_{p}, u_{p})), \\ w_{p + 1} \mapsto ⟨ {c r}_{p + 1}, P u b ({c r}_{p + 1}, u_{p + 1}) ⟩, \dots, w_{n} \mapsto ⟨ {c r}_{p + 1}, P u b ({c r}_{p + 1}, u_{p + 1}) ⟩} . \end{aligned}$
Consider a frame $ϕ_{1}$ of $m$ ballots, honestly generated by honest voters ${i d}_{i_{1}}, \dots, {i d}_{i_{m}}$ (two ballots can potentially be generated by the same voter):
$ϕ_{1} = {w_{1}^{'} \mapsto V o t e (p k, {i d}_{i_{1}}, {c r}_{i_{1}}, v_{1}, r_{1}), \dots, w_{m}^{'} \mapsto V o t e (p k, {i d}_{i_{m}}, {c r}_{i_{m}}, v_{m}, r_{m})}$
with votes $v_{1}, \dots, v_{n} \in V o t e s$ , using distinct random values $r_{1}, \dots, r_{m} \in N ∖ {s k, u_{1}, \dots, u_{n}}$ . Let $ϕ$ denote $ϕ_{0} \cup ϕ_{1}$ . Consider recipes $R_{1}, R_{2}, R_{3}, R_{4}$ on $d o m (ϕ)$ . Also consider an arbitrary injective renaming $σ : {r_{1}, \dots, r_{m}, u_{1}, \dots, u_{m}} \to Σ_{0} \cup N ∖ {s k}$ , such that for any $r$ in its domain, $σ (r)$ does not appear in any $R_{1}, R_{2}, R_{3}, R_{4}, V a l i d, C_{T a l l y}$ . Then, we have:
$V a l i d (R_{1} ϕ, R_{2} ϕ, R_{3} ϕ, p k) =_{E} t r u e \Leftrightarrow V a l i d (R_{1} ϕ σ, R_{2} ϕ σ, R_{3} ϕ σ, p k) =_{E} t r u e$ ; and

$C_{t a l l y} (R_{4} ϕ, s k) =_{E} C_{t a l l y} (R_{4} ϕ σ, s k)$ .

We can now recall and give a detailed proof of Proposition 3.
Proposition 3
Consider a voting scheme $V$ , and $p, n$ such that $1 \leq p \leq n$ . If $V$ does not satisfy $B P R I V (p, n - p)$ , then it does not satisfy $B P R I V (1, n - 1)$ .
Proof.
We will show that under our assumptions we have $P_{i} \approx_{t} P_{i + 1}$ for any $i \in {0, \dots, p - 1}$ , where $P_{i}$ are the processes displayed in Figure 2. Since $P_{0} = {E l e c t i o n L}_{p, n - p} (\vec{v_{1}}, \dots, \vec{v_{n}})$ and $P_{p} = {E l e c t i o n R}_{p, n - p} (\vec{v_{1}}, \dots, \vec{v_{n}})$ , by transitivity of $\approx_{t}$ , this property suffices to prove the theorem.

Fix some index $i \in {0, \dots, p - 1}$ . Observe that $P_{i}$ and $P_{i + 1}$ differ only in the behaviour of the $(i + 1)$ ^th voter ${i d}_{i + 1}$ , which is modelled by the process $H V o t e r L (\vec{v_{i + 1}}, p k (s k))$ in process $P_{i}$ , and by the process $H V o t e r R (\vec{v_{i + 1}}, p k (s k))$ in $P_{i + 1}$ . All other honest voters are identical in $P_{i}$ and $P_{i + 1}$ : they always follow the attacker’s instructions in the same way, either always voting for the right vote (for voters ${i d}_{j}$ , $j \leq i$ ) or the left vote (for voters ${i d}_{j}$ , $j \geq i + 2$ ). Therefore, the main idea of the proof is that all these other voters can be simulated by the attacker, since their behaviour is known and the same on both sides. The only remaining honest voter will be ${i d}_{i + 1}$ , to which we will apply the assumption that $B P R I V$ holds for one honest voter.

To prepare the terrain for applying this assumption later on, we define two additional processes $Q_{L}$ and $Q_{R}$ , where this ‘simulation’ is performed, that is, where all voters except ${i d}_{i + 1}$ are controlled by the attacker. Formally, the processes for these voters are replaced by instances of process $D V o t e r$ . The process $Q_{X}$ with $X \in {L, R}$ is as follows:
$\begin{aligned} Q_{X} & = n e w s k . m_{b b} := n i l . o u t (c h, p k (s k)) . \\ (p h a s e 1. o u t (c_{1}, ⟨ {c r}_{1}, {p c r}_{1} ⟩) . p h a s e 2. D V o t e r (\vec{v_{1}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{i}, ⟨ {c r}_{i}, {p c r}_{i} ⟩) . p h a s e 2. D V o t e r (\vec{v_{i}}, p k (s k)) \\ | p h a s e 1. o u t (c_{i + 1}, {p c r}_{i + 1}) . p h a s e 2. {H V o t e r}^{X} (\vec{v_{i + 1}}, p k (s k)) \\ | p h a s e 1. o u t (c_{i + 2}, ⟨ {c r}_{i + 2}, {p c r}_{i + 2} ⟩) . p h a s e 2. D V o t e r (\vec{v_{i + 2}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{n}, ⟨ {c r}_{n}, {p c r}_{n} ⟩) . p h a s e 2. D V o t e r (\vec{v_{n}}, p k (s k)) \\ | p h a s e 3. T a l l y (s k)) . \end{aligned}$
In fact, up to permutation of the parallel branches, these two processes are instances of the generic election process, with one honest voter ( ${i d}_{i + 1}$ ) and $n - 1$ dishonest voters ( ${i d}_{j}, j \neq i + 1$ ):
$Q_{X} = E l e c t i o n X_{1, n - 1} (\vec{v_{i + 1}}, \vec{v_{1}}, \dots, \vec{v_{i}}, \vec{v_{i + 2}}, \dots, \vec{v_{n}}) .$

Thanks to the assumption that $B P R I V$ holds for one honest voter, we have $Q_{L} \approx_{t} Q_{R}$ .

By contradiction, let us now assume that $P_{i} ≉_{t} P_{i + 1}$ . Using Lemma 3, $P_{i}$ , $P_{i + 1}$ , $Q_{L}$ , $Q_{R}$ are action-determinate. Let $t r$ be a witness of this non-equivalence of minimal length. Thanks to Proposition 1, $t r$ is such that:
$P_{i} \Rightarrow t r (i; P_{L}; ϕ_{L}; M_{L})$ for some $i, P_{L}, ϕ_{L}, M_{L}$ ;

$P_{i + 1} \Rightarrow t r (i; P_{R}; ϕ_{R}; M_{R})$ for some $P_{R}, ϕ_{R}, M_{R}$ ; and

$ϕ_{L} ≁ ϕ_{R}$ , and $t r$ is $Σ_{e r r}$ -free.
Moreover, for any $j \in {1, p}$ , if $i n (c_{j}, R)$ occurs in $t r$ in phase 2 (for some $R$ ), then there exist $(v_{0}, v_{1}) \in V o t e s \times V o t e s$ such that $R ϕ_{L} = R ϕ_{R} =_{E} (v_{0}, v_{1})$ . When such an input exists, let $i n s t r (j)$ denote this pair of votes, which is the instruction given by the attacker to voter $j$ in $t r$ .

In addition, by action-determinacy, $ϕ_{L}$ and $ϕ_{R}$ are unique up to $α$ -renaming of fresh names – without loss of generality, let us assume that the same symbols are used for matching private fresh names in both frames, that is the random values used for constructing an honest ballot on either side are given the same name, and similarly for the election key.

Our next step is to construct a sequence of actions $\bar{t r}$ that describes how to simulate the execution $t r$ of $P_{i}$ (respectively, $P_{i + 1}$ ) in an execution of $Q_{L}$ (respectively, $Q_{R}$ ).

Intuitively, the attacker interacting with $Q_{L}$ or $Q_{R}$ performs the same actions as the original one interacting with $P_{i}$ or $P_{i + 1}$ , except that all honest voters but ${i d}_{i + 1}$ are simulated using dishonest voters. Hence, whenever the attacker (for $P_{i}$ , $P_{i + 1}$ ) provides two votes $(v_{0}, v_{1})$ to an honest voter ${i d}_{j}$ (with $1 \leq j \leq p$ and $j \neq i + 1$ ), we instead let the attacker (for $Q_{L}$ , $Q_{R}$ ) construct the corresponding ballot $V o t e (p k, {i d}_{j}, {c r}_{j}, v_{0}, r_{0})$ and provide it to the process for ${i d}_{j}$ , who is now dishonest. Note that, since the result computed at the end by the tally always counts the ‘left’ vote $v_{0}$ , we must construct the ballot containing that vote, so that the result obtained in the end is the right one.

A subtle detail is that when constructing this ballot, the attacker will not be able to use the same private name $r_{0}$ originally used by the honest voter in $t r$ . He must instead use a public name. To keep notations relatively light, we introduce, for each private name $r$ generated by the process for an honest voter other than ${i d}_{i + 1}$ in $P_{i}$ or $P_{i + 1}$ an associated public name, that the attacker may use instead, which we will call $\tilde{r}$ . This name must be fresh, that is, not appear in any of the processes or recipes considered until now (including those used in the inputs in $t r$ ). We also let $σ$ denote the function mapping each such public $\tilde{r}$ to the corresponding private $r$ .

Due to the form of the processes, we can assume w.l.o.g. that $t r$ is a prefix of:
$o u t (c h, w_{0}) . p h a s e 1. o u t (c_{i_{1}}, w_{i_{1}}) . \dots . o u t (c_{i_{p}}, w_{i_{p}}) . p h a s e 2. {t r}_{c a s t} . p h a s e 3. o u t (c_{r e s}, w_{t a l l}),$
where ${t r}_{c a s t}$ contains only inputs and outputs on the channels ${c_{i}}_{1 \leq i \leq n}$ , with at most one input on each $c_{i}$ , and, when this input is present, at most one output on $c_{i}$ , placed after the input. Without loss of generality, call $R_{i}$ the recipe provided in the input on $c_{i}$ in ${t r}_{c a s t}$ , and $w_{i}^{'}$ the frame variable recording the output on $c_{i}$ (if they exist).

We now define recipes that we will use to let the attacker compute ballots for honest voters simulated by dishonest ones. For any $j \in ⟦ 1, p ⟧$ with $j \neq i + 1$ such that an input $i n (c_{j}, R_{j})$ occurs in ${t r}_{c a s t}$ , we let $B_{j}^{0} = V o t e (w_{0}, {i d}_{j}, {p r o j}_{1}^{2} (w_{j}), v_{0}, {\tilde{r}}_{0})$ and $B_{j}^{1} = V o t e (w_{0}, {i d}_{j}, {p r o j}_{1}^{2} (w_{j}), v_{1}, {\tilde{r}}_{1})$ , where $(v_{0}, v_{1}) = i n s t r (j)$ and ${\tilde{r}}_{0}$ , ${\tilde{r}}_{1}$ are fresh public names associated by $σ$ to the private names $r_{0}$ , $r_{1}$ used to construct the ballots for voter $j$ in $P_{i}$ and $P_{i + 1}$ .

Let $\bar{t r}$ be the trace containing the same actions as $t r$ , except that in ${t r}_{c a s t}$ (if $t r$ reaches ${t r}_{c a s t}$ ),
any input $i n (c_{j}, R_{j})$ for $1 \leq j \leq p, j \neq i + 1$ , that is, the input of the attacker’s instructions for honest voter $j$ , is replaced with $i n (c_{j}, B_{j}^{0})$ .

any input $i n (c_{j}, R_{j})$ for $j > p$ , that is, the attacker’s instruction for dishonest voter $j$ , os replaced with $i n (c_{j}, S_{j})$ , where
$S_{j} = R_{j} {w_{k}^{'} \mapsto B_{k}^{1}}_{1 \leq k \leq i} {w_{k}^{'} \mapsto B_{k}^{0}}_{i + 1 < k \leq p} .$

By construction of $\bar{t}$ , and from the shape of the processes $Q_{L}$ , $Q_{R}$ , it is clear that $\bar{t}$ is executable in $Q_{L}$ and $Q_{R}$ . All inputs and outputs in phases 0, 1, and 3 can be performed as expected. There are only two points where $\bar{t}$ might a priori be non-executable in phase 2 that are related to the validity checks:
If the validity check in a $D V o t e r$ process for a voter ${i d}_{j}$ with $j > p$ failed, preventing an output on $c_{j}$ that was possible in $t r$ : by construction, the ballot $b^{'}$ on which the validity check fails in $\bar{t r}$ and the ballot $b$ output by this voter in $t r$ , on which the test succeeds, are obtained by the same recipe applied to two frames of honest ballots that differ only on the random values used (the $\tilde{r}$ or the $r$ ). By the randomness independence property (Lemma 4), this is not possible.

If the validity check in a $D V o t e r$ process for a voter ${i d}_{j}$ with $j \leq p$ failed, preventing an output on $c_{j}$ that was possible in $t r$ : by the consistency assumption (Section 3.3), validity tests always succeed on honestly generated ballots, and this is not possible.

Executing $\bar{t r}$ in $Q_{L}$ and $Q_{R}$ , respectively, produces frames ${\bar{ϕ}}_{L}$ , ${\bar{ϕ}}_{R}$ . By action-determinacy, they are unique up to $α$ -renaming fresh names – without loss of generality, let us assume that the same symbols are used for matching private fresh names in both frames, that is, the random values used for constructing an honest ballot on either side are given the same name, and similarly for the election key. In addition, we will also assume these symbols are the same as for the corresponding names in $ϕ_{L}$ , $ϕ_{R}$ .

Note that, by construction, the recipes $B_{j}^{0}$ , $B_{j}^{1}$ from earlier, when applied to ${\bar{ϕ}}_{L}$ and ${\bar{ϕ}}_{R}$ , compute ballots $b_{0}$ , $b_{1}$ such that $b_{0} σ$ and $b_{1} σ$ are the two ballots computed by honest voter $j$ in $t r$ in $P_{i}$ and $P_{i + 1}$ , respectively. Similarly, the recipe $S_{j}$ used in $\bar{t r}$ to compute dishonest ballots produces, when applied to ${\bar{ϕ}}_{L}$ and ${\bar{ϕ}}_{R}$ , a ballot $b$ such that $b σ$ is the ballot provided by the attacker to dishonest voter $j$ in $t r$ in $P_{i}$ and $P_{i + 1}$ , respectively.

The last step of our proof will be to describe the relation between ${\bar{ϕ}}_{L}$ , ${\bar{ϕ}}_{R}$ , and $ϕ_{L}$ , $ϕ_{R}$ . As we will see, this will bring out a contradiction, as the first two are assumed statically equivalent and the other two are not.

We construct a frame of recipes $R$ , giving for each variable $w \in d o m (ϕ_{L}) = d o m (ϕ_{R})$ a recipe $R (w)$ with variables in $d o m ({\bar{ϕ}}_{L}) = d o m ({\bar{ϕ}}_{R})$ , such that $ϕ_{L} = (R {\bar{ϕ}}_{L}) σ$ and $ϕ_{R} = (R {\bar{ϕ}}_{R}) σ$ , that is,
$\forall w \in d o m (ϕ_{L}) . ϕ_{L} (w) = (R (w) {\bar{ϕ}}_{L}) σ \land ϕ_{R} (w) = (R (w) {\bar{ϕ}}_{R}) σ .$
(1)

$R$ is constructed as follows:
For $w_{0}$ , storing the election key output in phase 0: this output is also performed in $t r$ , and $R (w_{0}) = w_{0}$ is adequate.

For all $w_{j}$ present in $d o m (ϕ_{L})$ , storing credentials output in phase 1: $$
if $j = i + 1$ , $ϕ_{L}$ and $ϕ_{R}$ as well as ${\bar{ϕ}}_{L}$ , ${\bar{ϕ}}_{R}$ contain the public credential ${p c r}_{j}$ in $w_{j}$ , and thus $R (w_{j}) = w_{j}$ works;
$$
if $1 \leq j \leq p$ and $j \neq i + 1$ , $ϕ_{L}$ and $ϕ_{R}$ contain the public credential ${p c r}_{j}$ in $w_{j}$ , while ${\bar{ϕ}}_{L}$ and ${\bar{ϕ}}_{R}$ contain $⟨ {c r}_{j}, {p c r}_{j} ⟩$ ; thus $R (w_{j}) = {p r o j}_{2}^{2} (w_{j})$ works;
$$
if $j > p$ , $ϕ_{L}$ and $ϕ_{R}$ as well as ${\bar{ϕ}}_{L}$ , ${\bar{ϕ}}_{R}$ contain the credentials $⟨ {c r}_{j}, {p c r}_{j} ⟩$ in $w_{j}$ , and thus $R (w_{j}) = w_{j}$ works.

For all $w_{j}^{'}$ present in $d o m (ϕ_{L})$ , storing all ballots output during phase 2: $$
If $j < i + 1$ , according to the processes, $ϕ_{L}$ and $ϕ_{R}$ contain in $w_{j}^{'}$ the ballot $V o t e (p k, {i d}_{j}, {c r}_{j}, v_{1}, r_{1})$ , where $(v_{0}, v_{1}) = i n s t r (j)$ , and $r_{1}$ is the nonce generated by the voter. Thus, $R (w_{j}^{'}) = B_{j}^{1}$ is adequate.
$$
If $j = i + 1$ , according to the processes, $ϕ_{L}$ as well as ${\bar{ϕ}}_{L}$ contain in $w_{j}^{'}$ the ballot $V o t e (p k, {i d}_{j}, {c r}_{j}, v_{0}, r_{0})$ , while $ϕ_{R}$ and ${\bar{ϕ}}_{R}$ contain the ballot $V o t e (p k, {i d}_{j}, {c r}_{j}, v_{1}, r_{1})$ , where $(v_{0}, v_{1}) = i n s t r (j)$ , and $r_{0}$ , $r_{1}$ the random values used. Thus $R (w_{j}^{'}) = w_{j}^{'}$ is appropriate.
$$
If $i + 1 < j \leq p$ , according to the processes, $ϕ_{L}$ and $ϕ_{R}$ contain $V o t e (p k, {i d}_{j}, {c r}_{j}, v_{0}, r_{0})$ in $w_{j}^{'}$ , where $(v_{0}, v_{1}) = i n s t r (j)$ and $r_{0}$ is the nonce generated by the voter. Thus, $R (w_{j}^{'}) = B_{j}^{0}$ is adequate.
$$
If $j > p$ , according to the processes, $ϕ_{L}$ , $ϕ_{R}$ , ${\bar{ϕ}}_{L}$ , and ${\bar{ϕ}}_{R}$ each contain in $w_{j}^{'}$ the ballot received as an input from the attacker earlier by voter $j$ ’s process. As explained earlier, the recipe used in $\bar{t r}$ to construct that input is such that this ballot verifies ${\bar{ϕ}}_{L} (w_{j}^{'}) σ = ϕ_{L} (w_{j}^{'})$ and ${\bar{ϕ}}_{R} (w_{j}^{'}) σ = ϕ_{R} (w_{j}^{'})$ . Hence, picking $R (w_{j}^{'}) = w_{j}^{'}$ satisfies (1).

Finally, the only remaining variable is $w_{t a l l}$ , storing the result output in phase 3. Our argument is that the tally actually outputs the same result in the execution of $t r$ in $P_{i}$ and $\bar{t r}$ in $Q_{L}$ , and similarly for $P_{i + 1}$ and $Q_{R}$ . Indeed, consider the inputs received by $T a l l y$ on the private channel containing the internal state. In $P_{i}$ and $t r$ , these are the ‘left’ ballots computed by all honest voters and the dishonest ballots. In $Q_{L}$ and $\bar{t r}$ , they are $$
the left ballot of voter $i + 1$ ;
$$
the ballots given as input to dishonest voters $j \in ⟦ 1, p ⟧$ computed using $B_{j}^{0}$ , which, as explained earlier, are the left ballots of the original honest voters where $r_{0}$ is replaced with $r_{0}^{'}$ ; and
$$
the ballots given as input to dishonest voters $j > p$ , computed using $R R_{j}$ , which, as explained earlier, are computed in the same way as the ballots of the original dishonest voters, from the list of honest ballots where all random values $r$ are replaced with the corresponding $\tilde{r}$ .

Hence, the randomness-independence property (Lemma 4) applies and guarantees that tallying the ballots in $P_{i}$ with $t r$ , and in $Q_{L}$ with $\bar{t r}$ produces the same result. The same argument applies to $P_{i + 1}$ and $Q_{R}$ . Thus, $R (w_{t a l l}) = w_{t a l l}$ satisfies (1).

Using property (1), we can now conclude the proof. Indeed, we know that $Q_{L} \approx_{t} Q_{R}$ , which, applied to $\bar{t r}$ , implies that ${\bar{ϕ}}_{L} \sim {\bar{ϕ}}_{R}$ . Since $R$ is a frame of recipes, it follows immediately from the definition of static equivalence that $R {\bar{ϕ}}_{L} \sim R {\bar{ϕ}}_{R}$ .

On the other hand, $t r$ was obtained as a non-equivalence witness for $P_{i}$ and $P_{i + 1}$ , meaning that $ϕ_{L} ≁ ϕ_{R}$ . Thus, there exist recipes $M$ , $N$ such that $M ϕ_{L} = N ϕ_{L}$ and $M ϕ_{R} \neq N ϕ_{R}$ , that is,
$M ((R {\bar{ϕ}}_{L}) σ) = N ((R {\bar{ϕ}}_{L}) σ) and M ((R {\bar{ϕ}}_{R}) σ) \neq N ((R {\bar{ϕ}}_{R}) σ) .$
Since none of the public names $r^{'}$ appear in $ϕ_{L}$ or $ϕ_{R}$ , we may always w.l.o.g. choose $M$ and $N$ that do not contain these names either. We then have
$(M (R {\bar{ϕ}}_{L})) σ = (N (R {\bar{ϕ}}_{L})) σ and (M (R {\bar{ϕ}}_{R}) σ) \neq (N (R {\bar{ϕ}}_{R}) σ) .$
Since $σ$ is a bijective renaming, this means
$M (R {\bar{ϕ}}_{L}) = N (R {\bar{ϕ}}_{L}) and M (R {\bar{ϕ}}_{R}) \neq N (R {\bar{ϕ}}_{R}),$
that is, $M R \overset{?}{=} N R$ is a test distinguishing ${\bar{ϕ}}_{L}$ and ${\bar{ϕ}}_{R}$ . This contradicts the fact $Q_{L} \approx_{t} Q_{R}$ . Therefore, our assumption was false, that is, $P_{i} \approx_{t} P_{i + 1}$ , which concludes the proof.
4.4. Bounding the number of dishonest voters

This second reduction result allows one to bind the number of dishonest voters when considering BPRIV. More precisely, we consider a unique honest voter, and we show that $k$ dishonest voters are sufficient to mount an attack against vote privacy (if such an attack exists). Here, we reduce the number of voters from $n$ to $k + 1$ ( $k$ dishonest voters plus one honest voter), and the resulting bound depends on the counting function.

Proposition 4
Let $V$ be a voting scheme whose associated counting function is $k$ -bounded for $k \geq 1$ . If $V$ does not satisfy $B P R I V (1, n)$ for some $n \geq 0$ , then $V$ does not satisfy $B P R I V (1, k)$ . Moreover, in that case, there exists a witness of this attack where no more than $k$ ballots reached the ballot box.

Roughly, if $B P R I V (1, n - 1)$ does not hold, the difference appears either (i) when the honest voter outputs her ballot, or (ii) when outputting the result. Indeed, the behaviour of a dishonest voter who simply outputs the message he received does not help to mount an attack. Moreover, the only test that a dishonest voter performs is a public test from which the attacker will not infer anything. In case (i), no dishonest voters are even needed and the claim holds.

In case (ii), we know that the public terms representing the final result are different on both sides. We apply our $k$ -boundedness hypothesis, and we know that a difference is still there when considering $k$ voters (or even less). Removing the corresponding actions performed by dishonest voters, the trace still corresponds to an execution assuming that the validity tests do not depend on the the other ballots on the bulletin board. Hence, we have a witness of non-equivalence with at most $k$ ballots, and thus at most $k$ dishonest voters.

We now give a detailed proof of Proposition 4.
Proof.
First, relying on Lemma 3, we know that the processes under study are action-deterministic, and therefore, thanks to Proposition 1, we can assume that a witness of an attack of minimal length has some specific shape. Following the notation introduced in Section 3, we consider $n + 1$ distinct voters $\vec{v_{0}}, \dots, \vec{v_{n}}$ , and we consider a witness $t r$ of non-equivalence of minimal length. We know that:
${E l e c t i o n}_{1, n}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{L}; P_{L}; ϕ_{L}; M_{L})$ for some $(i_{L}; P_{L}; ϕ_{L}; M_{L})$ ;

${E l e c t i o n}_{1, n}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}}) \Rightarrow t r (i_{R}; P_{R}; ϕ_{R}; M_{R})$ for some $(i_{R}; P_{R}; ϕ_{R}; M_{R})$ ; and

$i_{L} = i_{R}$ , $ϕ_{L} ≁ ϕ_{R}$ , and $t r$ is $Σ_{e r r}$ -free.

We are going to show that this minimal witness $t r$ is also a witness of the following non-equivalence: ${E l e c t i o n}_{1, k}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}}) ≉_{t} {E l e c t i o n}_{1, k}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}})$ .

In the following, we will distinguish cases depending on the form of $t r$ . Due to the form of the processes, we can assume w.l.o.g. that $t r$ is a prefix of:
$o u t (c h, w_{0}) . p h a s e 1. o u t (c_{i_{1}}, w_{i_{1}}) . \dots . o u t (c_{i_{p}}, w_{i_{p}}) . p h a s e 2. {t r}_{c a s t} . p h a s e 3. o u t (c_{r e s}, w_{t a l l}) .$
Case 1:
$t r$ only contains actions from phase $0$ and phase $1$ . In such a case, $t r$ cannot be a witness of non-equivalence. Indeed, the frames on both sides are necessarily in static equivalence.
Case 2:
$t r$ contains actions from phases $0$ , $1$ , and $2$ (but no action from phase $3$ ). We distinguish two cases.
We first consider the case where some actions in phase 2 are performed by a dishonest voter ${i d}_{j}$ , that is there is $i n (c_{j}, R_{j}) \in t r$ and possibly $o u t (c_{j}, w_{j}) \in t r$ , and $a p p e n d (c_{j})$ as well. Then, we consider ${t r}^{'} = \bar{t r} {w_{j} \mapsto R_{j}}$ where $\bar{t r}$ is $t r$ in which the input, output, and append actions performed during phase 2 on channel $c_{j}$ have been removed. The resulting trace ${t r}^{'}$ is smaller than $t r$ . To conclude, it remains to show that ${t r}^{'}$ is a witness of non-equivalence, thus contradicting the minimality of the witness $t r$ .It is easy to see that this trace ${t r}^{'}$ still passes in ${E l e c t i o n}_{1, n}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ . Note that the action $a p p e n d (c_{j})$ has no impact since the tallying phase has not been executed. The frame $ϕ_{L}^{'}$ resulting from this new execution ${t r}^{'}$ is such that $ϕ_{L} = ϕ_{L}^{'} \cup {w_{j} \mapsto b_{L}^{0}}$ , where $b_{L}^{0} = R_{j} ϕ_{L}^{'}$ and $R_{j}$ is the recipe mentioned above such that $v a r s (R_{j}) \subseteq d o m (ϕ_{L}^{'})$ .Similarly to the reasoning performed on the left side, this trace ${t r}^{'}$ also passes in ${E l e c t i o n}_{1, n}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ (since $t r$ passes too). Moreover, the frame $ϕ_{R}^{'}$ resulting from this execution ${t r}^{'}$ is such that $ϕ_{R} = ϕ_{R}^{'} \cup {w_{j} \mapsto b_{R}^{0}}$ , where $b_{R}^{0} = R_{j} ϕ_{R}^{'} ↓$ considering the exact same recipe $R_{j}$ as the one mentioned above. We know that $ϕ_{L}^{'} \sim ϕ_{R}^{'}$ implies that $ϕ_{L} \sim ϕ_{R}$ , and thus since $ϕ_{L} ≁ ϕ_{R}$ , we deduce that $ϕ_{L}^{'} ≁ ϕ_{R}^{'}$ . This allows us to conclude that ${t r}^{'}$ is a witness of non-inclusion, and this leads to a contradiction as ${t r}^{'}$ is smaller than $t r$ .

We now assume that there is no input/output/append action performed by a dishonest voter during the casting phase (phase $2$ ). In such a case, we have that either ${t r}_{c a s t} = i n (c_{0}, R_{0}) . o u t (c_{0}, w_{0}) . a p p e n d (c_{0})$ or ${t r}_{c a s t} = i n (c_{0}, R_{0}) . o u t (c_{0}, w_{0})$ or ${t r}_{c a s t} = i n (c_{0}, R_{0})$ . Note that actually the first and the last cases are impossible since the input and the append actions do not modify the frame, and thus are not necessary to obtain a witness of non-equivalence (of the shape mentioned above) leading to a contradiction regarding minimality.In case phase $1$ contains an output on $c_{i}$ with $i > 0$ , that is, $o u t (c_{i}, w_{i})$ occurs in phase $1$ , and $w_{i} ϕ_{L} = ⟨ {c r}_{i}, P u b ({c r}_{i}, u_{i}) ⟩$ , we consider ${t r}^{'} = \bar{t r} {w_{i} \mapsto ⟨ {c r}_{i}^{'}, P u b ({c r}_{i}^{'}, u_{i}^{'}) ⟩}$ , where $\bar{t r}$ is $t r$ in which this output has been removed, and ${c r}_{i}^{'}$ and $u_{i}^{'}$ are fresh public constants. Then ${t r}^{'}$ passes in ${E l e c t i o n}_{1, n}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ and also in ${E l e c t i o n}_{1, n}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ . Indeed, ${c r}_{i}$ and $u_{i}$ do not occur anymore in the remaining process to be executed since $D V o t e r$ is not executed for ${i d}_{j}$ .This trace ${t r}^{'}$ leads to the frames $ϕ_{L}^{'}$ (on the left) and $ϕ_{R}^{'}$ (on the right) such that $ϕ_{X} = ϕ_{X}^{'} {{c r}_{i}^{'} \mapsto {c r}_{i}} {u_{i}^{'} \mapsto u_{i}} \cup {w_{i} \mapsto ⟨ {c r}_{i}, P u b ({c r}_{i}, u_{i}) ⟩}$ for $X \in {L, R}$ . Since, we know that $ϕ_{L} ≁ ϕ_{R}$ , we conclude that $ϕ_{L}^{'} ≁ ϕ_{R}^{'}$ , which proves this case. Note that, in case the distinguishing test relies on $w_{i}$ , we can easily reconstruct the corresponding term $⟨ {c r}_{i}^{'}, P u b ({c r}_{i}^{'}, u_{i}^{'}) ⟩$ to obtain a witness of $ϕ_{L}^{'} ≁ ϕ_{R}^{'}$ .Otherwise (no output on $c_{i}$ with $i > 0$ during phase $1$ ), the trace $t r$ also passes starting from ${E l e c t i o n}_{1, k}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}})$ , or from ${E l e c t i o n}_{1, k}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}})$ , and the resulting frames are the same as those obtained when starting the executions from ${E l e c t i o n}_{1, n}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ , and ${E l e c t i o n}_{1, k}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ . Therefore, $t r$ is a witness of non-equivalence for ${E l e c t i o n}_{1, k}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}}) n o t \approx_{t} {E l e c t i o n}_{1, k}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}})$ contradicting our main hypothesis.

Case 3:
$t r$ contains actions from phase $3$ (actually only one). We distinguish three cases.
If during phase $2$ , some action occurs on channel $c_{i}$ with $i > 0$ – $i n (c_{i}, R)$ , and $o u t (c_{i}, w)$ but not the $a p p e n d (c_{i})$ one – then we can consider ${t r}^{'} = \bar{t r} {w \mapsto R}$ , where $\bar{t r}$ is equal to $t r$ without these actions (input and output) on channel $c_{i}$ , and we can show that this trace ${t r}^{'}$ is a witness of non-equivalence obtaining a contradiction regarding the minimality of $t r$ .

Otherwise, if phase $1$ contains an action of the form $o u t (c_{i}, w_{i})$ corresponding to the output of a credential of a dishonest voter ${i d}_{i}$ (i.e. $i > 0$ ), whereas there is no $i n (c_{i}, R_{i})$ during phase $2$ for this particular (dishonest) voter, then we consider the trace ${t r}^{'}$ which is equal to $t r$ without this output $o u t (c_{i}, w_{i})$ , and we also replace the occurrences of $w_{i}$ in $t r$ by $⟨ {c r}_{i}^{'}, P u b ({c r}_{i}^{'}, u_{i}^{'}) ⟩$ , where ${c r}_{i}^{'}$ and $u_{i}^{'}$ are fresh public constants. As before, we conclude that ${t r}^{'}$ is a smaller witness.

We now consider the case of a trace $t r$ that is composed of phase $1$ during which only dishonest voters who cast their ballot (action $a p p e n d$ ) participate in phase 1, then phase $2$ , and then phase 3 containing the output on channel $c_{r e s}$ . We also know that the last output (the one on $c_{r e s}$ ) is needed to get a witness of non-equivalence and that $ϕ_{L} ≁ ϕ_{R}$ , where $ϕ_{L}$ and $ϕ_{R}$ are the two resulting frames. Thus, the test distinguishing these two frames relies on $w_{t a l l}$ (the message output on $c_{r e s}$ ). Actually, relying on Lemma 1, we have $w_{t a l l} ϕ_{L} \neq_{E} w_{t a l l} ϕ_{R}$ . Moreover, we know that $w_{t a l l} ϕ_{L} = c o u n t (e x t r a c t ({B B}_{L}))$ and $w_{t a l l} ϕ_{R} = c o u n t (e x t r a c t ({B B}_{R}))$ , where ${B B}_{L}$ (respectively, ${B B}_{R}$ ) is the bulletin board (i.e. the content of the memory cell $m_{b b}$ ) resulting from trace $t r$ on the left (respectively, on the right).If at most $k$ voters voted (i.e. cast their vote – action $a p p e n d$ ), then, as we know that only the dishonest voters who cast a vote output their credential during the initialisation phase, we can deduce that this witness $t r$ is also a witness of ${E l e c t i o n}_{1, k}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}}) ≉_{t} {E l e c t i o n}_{1, k}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}})$ .Otherwise, we know that $n^{'}$ voters with $n^{'} > k$ have cast their vote. Thanks to our $k$ -bounded hypothesis, we know that there exists $k^{'} \leq k$ , and $0 \leq i_{1} < \dots < i_{k^{'}} \leq n$ such that counting the votes of ${i d}_{i_{1}}, \dots, {i d}_{i_{k^{'}}}$ still leads to a difference in the result.In the trace $t r$ , we know that there are actions $a p p e n d (c_{i_{1}}), \dots, a p p e n d (c_{i_{k^{'}}})$ corresponding to the append actions of these voters ${i d}_{i_{1}}, \dots, {i d}_{i_{k^{'}}}$ . We consider ${t r}^{'}$ obtained from $t r$ by removing all these actions. It is easy to see that this smaller trace ${t r}^{'}$ still passes in ${E l e c t i o n}_{1, n}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ and in ${E l e c t i o n}_{1, n}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ . The resulting bulletin board ${B B}_{L}^{'}$ (respectively, ${B B}_{R}^{'}$ ) contain few ballots than before, and these ballots have been chosen such that:
$c o u n t (e x t r a c t ({B B}_{L}^{'})) \neq c o u n t (e x t r a c t ({B B}_{R}^{'})) .$
Therefore, the resulting frames $ϕ_{L}^{'}$ and $ϕ_{R}^{'}$ are almost the same as $ϕ_{L}$ and $ϕ_{R}$ , except for the resulting output during the tallying phase, which we know are different public terms. As our processes are action-deterministic (Lemma 3), there is no other choice of obtaining another frame, and thus ${t r}^{'}$ is a smaller witness of ${E l e c t i o n}_{1, n}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}}) ≉_{t} {E l e c t i o n}_{1, n}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{n}})$ , leading again to a contradiction.

Hence the result.
5. Dealing with re-voting

We now consider the case where re-voting is allowed. We first adapt the BPRIV definition to this setting (see Section 5.1) before stating and discussing our reduction result in Sections 5.2 and 5.3.

5.1. Modelling BPRIV with re-voting

The processes $H V o t e r$ , $D V o t e r$ , and $T a l l y$ are left unchanged. Only the main $E l e c t i o n$ processes, and the consistency assumption change. The tallying now takes into account a revote policy, indicating how to proceed when a voter casts multiple votes. A revote policy is a function:
$p o l i c y : (Σ_{0} \times N_{p r i v} \times V o t e s) l i s t \to V o t e s l i s t .$
This $p o l i c y$ function replaces $l s t$ in the strong consistency assumption (Section 3.3). We consider here the two most common revote policies. The $l a s t$ and $f i r s t$ policies select, respectively, the last or the first vote from each voter.

We reuse the notations from Section 3.2, and we introduce in addition $\vec{w_{i}} = (d_{i}, i d_{i}, {c r}_{i}, p c r_{i})$ for each $i \in {1, \dots, n}$ where $d_{i}$ are different private channel names. The privacy property $B P R I V R (p, n - p)$ is written as follows:
${E l e c t i o n R e v o t e}_{p, n - p}^{L} (\vec{v_{1}}, \dots, \vec{v_{n}}) \approx_{t} {E l e c t i o n R e v o t e}_{p, n - p}^{R} (\vec{v_{1}}, \dots, \vec{v_{n}}),$
where ${E l e c t i o n R e v o t e}_{p, n - p}^{X} (\vec{v_{1}}, \dots, \vec{v_{n}}) = n e w s k . m_{b b} := n i l . o u t (c h, p k (s k)) .$

$\begin{array}{l} (p h a s e 1. o u t (c_{1}, p c r_{1}) . p h a s e 2.! n e w d_{1} . o u t (c_{1}, d_{1}) . {H V o t e r}^{X} (\vec{v_{1}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{p}, p c r_{p}) . p h a s e 2.! n e w d_{p} . o u t (c_{p}, d_{p}) . {H V o t e r}^{X} (\vec{w_{p}}, p k (s k)) \\ | p h a s e 1. o u t (c_{p + 1}, p c r_{p + 1}) . p h a s e 2.! n e w d_{p + 1} . o u t (c_{p + 1}, d_{p + 1}) . D V o t e r (\vec{w_{p + 1}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{n}, p c r_{n}) . p h a s e 2.! n e w d_{n} . o u t (c_{n}, d_{n}) . D V o t e r (\vec{w_{n}}, p k (s k)) \\ | p h a s e 3. T a l l y (s k)), \end{array}$
with $c h \in {C h}_{p u b}$ , $X \in {L, R}$ .

Note that a replication operator has been added in front of the voter processes to model the fact that revote is now possible.

5.2. Reduction result with re-voting

We are now able to state our reduction result when considering re-voting.

Theorem 2
Let $V$ be a voting scheme whose associated counting function is $k$ -bounded for some $k \geq 1$ , and $p, n$ be two integers such that $1 \leq p \leq n$ . If $V$ does not satisfy $B P R I V R (p, n - p)$ , then $V$ does not satisfy $B P R I V R (1, k)$ . Moreover, in that case, there exists a witness of this attack where no more than $k$ ballots reached the ballot box (each from a different voter).

The proof of this theorem follows the same lines as the one when revote is not allowed and is composed of two main reduction steps. Before performing these two reduction steps, we may note that our election processes are still action-deterministic. Actually, the construction $n e w d . o u t (c, d) . P$ is there for that, and Proposition 1 characterising the form of a minimal attack trace is still valid for these election processes where revote is allowed. Rather than redoing the proof completely, we highlight the differences with the ‘no revote’ case for these two steps.

Step 1:
Reducing the number of honest voters to $1$ . We show that if $B P R I V R (1, n - 1)$ holds, then so does $B P R I V (p, n - p)$ . The proof for this step has the same structure as the one for Proposition 2. The only difference, essentially, is that instead of each honest voter only submitting one ballot, which we have to simulate for a dishonest voter, they may submit any number of ballots. Thanks to the actions $s e s s (c_{j}, d)$ added to the trace, we know, however, which voter each ballot belongs to. Using this information, we can simulate the honest ballots, just as in the previous proof. As in the ‘no revote’ proof, we define intermediate processes $P_{i}$ for $i \in {0, \dots, p}$ ), and we assume by contradiction that there exists $i_{0}$ such that $P_{i_{0}} ≉_{t} P_{i_{0} + 1}$ . We consider a minimal trace $t r$ witnessing $P_{i} ≉_{t} P_{i + 1}$ , with associated frames $ϕ_{L}$ , $ϕ_{R}$ . Its shape is slightly different from the one in the previous proof, because of the $s e s s (c_{j}, d)$ actions added whenever voter $j$ is replicated for a new session. However, the ideas are the same.
Step 2:
Reducing the number of dishonest voters to $k$ . Again, the shape of the witness of non-equivalence that we consider is a bit different from the one used in Proposition 4 as we now have $s e s s (c_{j}, d)$ actions that will occur. Nevertheless, the reasoning remains the same. We only focus on the case where $t r$ contains actions from phase $3$ (actually only one), and we distinguish three cases:

If, during phase 2, some actions (e.g. $s e s s (c_{i}, d)$ , $i n (d, R)$ , $o u t (d, w)$ ) occur on channel $c_{i}$ (with $i > 0$ ) but not the corresponding $a p p e n d (d)$ actions, then we can consider ${t r}^{'} = \bar{t r} {w \mapsto R}$ , where $\bar{t r}$ is equal to $t r$ without these actions, and we can show that ${t r}^{'}$ is a witness of non-equivalence obtaining a contradiction regarding the minimality of $t r$ .

Now, in case phase 1 contains an action of the form $o u t (c_{i}, w_{i})$ with $i > 0$ , whereas there is no $s e s s (c_{i}, d)$ in phase 2, then we can consider the trace ${t r}^{'}$ which is equal to $t r$ without this output $o u t (c_{i}, w_{i})$ , and where the occurrences of $w_{i}$ are replaced with $⟨ {c r}_{i}^{'}, P u b ({c r}_{i}^{'}, u_{i}^{'}) ⟩$ for fresh public constants ${c r}_{i}^{'}$ and $u_{i}^{'}$ . As before, we conclude that ${t r}^{'}$ is a smaller witness.

We now consider the case of a trace $t r$ composed of phase 1 (only voters who output a ballot participate in this phase 1), then phase 2, and then the output of the result during phase 3. We have $ϕ_{L} ≁ ϕ_{R}$ where $ϕ_{L}$ and $ϕ_{R}$ are the two resulting frames, and in fact, relying on Lemma 1, we have $w_{t a l l} ϕ_{L} \neq_{E} w_{t a l l} ϕ_{R}$ . Moreover, we know that:
$\begin{matrix} w_{t a l l} ϕ_{L} = c o u n t (p o l i c y (e x t r a c t ({B B}_{L}))) and w_{t a l l} ϕ_{R} = c o u n t (p o l i c y (e x t r a c t ({B B}_{R}))), \end{matrix}$
where ${B B}_{L}$ (respectively, ${B B}_{R}$ ) is the bulletin board (i.e. the content of the memory cell $m_{b b}$ ) resulting from the trace $t r$ on the left (respectively, on the right).If at most $k$ distinct voters cast their vote (action $a p p e n d$ ), then we know that only these dishonest voters have output their credentials during the initialisation phase, and thus this witness is also a witness of
${E l e c t i o n R e v o t e}_{1, k}^{L} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}}) ≉_{t} {E l e c t i o n R e v o t e}_{1, k}^{R} (\vec{v_{0}}, \vec{v_{1}}, \dots, \vec{v_{k}}) .$
Moreover, this witness satisfies our requirements, which concludes the proof for this case.Otherwise, we know that $n^{'}$ votes with $n^{'} > k$ have been cast (possibly by the same voter), that is, that ${B B}_{L} = [b_{1}^{L}, \dots, b_{n^{'}}^{L}]$ and ${B B}_{R} = [b_{1}^{R}, \dots, b_{n^{'}}^{R}]$ . Moreover, we know that for each pair of ballots $(b_{j}^{L}, b_{j}^{R})$ , there exists $i d$ , $c r$ , $v^{L}$ , and $v^{R}$ such that: $e x t r a c t (b_{j}^{L}) = (i d, c r, v^{L})$ and $e x t r a c t (b_{j}^{R}) = (i d, c r, v^{R})$ . In case a voter casts more than one ballot, then we know that only one has been taken into account due to the revote policy, and thus there is $i_{0}$ such that $b_{i_{0}}^{L}$ and $b_{i_{0}}^{R}$ do not influence the result (since it has been removed by the revote policy). Therefore, we can remove the corresponding $a p p e n d (d)$ action, and we obtain a smaller trace ${t r}^{'}$ leading to the exact same frames, and the same result.Otherwise, each voter has voted only once, but $n^{'} > k$ . Therefore the policy will consider all ballots to compute the result. Thanks to our $k$ -bounded hypothesis, we know that there exists $k^{'} \leq k$ , and $0 \leq i_{1} < \dots < i_{k^{'}} \leq n$ such that
$c o u n t (e x t r a c t ([b_{i_{1}}^{L}, \dots, b_{i_{k^{'}}}^{L}])) \neq c o u n t (e x t r a c t ([b_{i_{1}}^{R}, \dots, b_{i_{k^{'}}}^{R}])) .$
Note that, since each voter only votes once, this implies that
$c o u n t (p o l i c y (e x t r a c t ([b_{i_{1}}^{L}, \dots, b_{i_{k^{'}}}^{L}]))) \neq c o u n t (p o l i c y (e x t r a c t ([b_{i_{1}}^{R}, \dots, b_{i_{k^{'}}}^{R}]))) .$
We now consider ${t r}^{'}$ , which is $t r$ without the actions $a p p e n d (d)$ corresponding to all the ballots that have been removed. Note that, if we want to remove the $i_{0}^{th}$ ballot from the bulletin board, this corresponds to removing the $i_{0}^{th}$ $a p p e n d$ actions from the trace $t r$ . The resulting trace ${t r}^{'}$ is smaller than $t r$ , and leads to the exact same frames, except for their last element corresponding to the output of the result. We have ensured a difference is maintained between the two sides, and thus ${t r}^{'}$ is still a witness of non-equivalence, which concludes the proof.

5.3. Discussion

Even after applying our reduction result, we may note that replication operators are still there, and thus establishing such an equivalence property (even when $p = 1$ , and $k = 1$ ) is not trivial. Traces of unbounded length still must be considered. However, as we are able to establish that, in a minimal attack trace, at most $k$ ballots reached the ballot box (each by a different voter), we can easily remove the replication operator in front of a dishonest voter. This reasoning does not apply to the honest voter, as the output she performed may be useful to mount an attack (contrary to the output of a dishonest voter who outputs a term known by the attacker). This has been overlooked in the reduction result presented in Arapinis et al.(6) The security analysis of Helios with revote has been done without considering this replication operator, leading to erroneous security analysis.

6. Extension to the case of a dishonest ballot box

We now consider the case where the ballot box is no longer trusted. As in the previous section, we first adapt the BPRIV definition to this setting before stating and proving our reduction result.

6.1. Symbolic BPRIV with a dishonest ballot box

The symbolic definition we propose in Section 3.2, based on the original game-based formulation of Bernhard et al. (11), considers a setting where the ballot box is trusted. Indeed, it does not give the attacker complete control over the contents of the ballot box: the attacker cannot arbitrarily write to the ballot box, but rather can only see and block honest ballots, and cast ballots in the name of dishonest voters only.

In (12), an extension of BPRIV that features a fully dishonest ballot box is introduced: the attacker can arbitrarily choose the content of the ballot box. This creates additional difficulties compared to the honest ballot box case. In BPRIV, on the left-hand side, the attacker is shown the ‘real’ ballots, that is, the ones that will be tallied. On the right-hand side, he sees a ‘fake’ ballot for each honest voter, while using the corresponding ‘real’ ballot when tallying. Adapting naively this behaviour to the dishonest ballot box setting produces an unsatisfying definition. Indeed, if the attacker can modify arbitrarily the ‘fake’ ballots he received before sending them to be tallied, simply using (on the right-hand side) the unmodified ‘real’ ballots to compute the election result would let him trivially distinguish the two sides. Instead, Cortier et al. (12) propose to observe how the attacker modified the ‘fake’ ballots, and to apply the same modifications to the ‘real’ ballots before tallying. This leads (12) to an extension of BPRIV, in the form of a cryptographic game that relies on a so-called recovery algorithm, which performs the operation of finding out what modifications the attacker did on the ‘fake’ ballots.

We propose here an adaptation of our symbolic BPRIV definition, that incorporates this idea. To simplify the presentation, we restrict ourselves to the case where voters do not revote.

Voter processes

We update the ${H V o t e r}^{L}$ and ${H V o t e r}^{R}$ processes as follows.
$\begin{array}{rcl} \begin{array}{l} {H V o t e r}^{L} (c, i d, c r, p c r, p k) = \\ i n (c, z) . \\ l e t (v^{0}, v^{1}) = ({p r o j}_{1}^{2} (z), {p r o j}_{2}^{2} (z)) i n \\ i f v^{0}, v^{1} \in V o t e s t h e n \\ n e w r^{0} . n e w r^{1} . \\ l e t b^{0} = V o t e (p k, i d, c r, v^{0}, r^{0}) i n \\ l e t b^{1} = V o t e (p k, i d, c r, v^{1}, r^{1}) i n \\ i f V a l i d (i d, p c r, b^{0}, p k) = t r u e \\ t h e n a p p e n d (c, ⟨ i d, ⊥, ⊥ ⟩_{3}, m_{b b}^{r e f}) . \\ o u t (c, b^{0}) \\ e l s e o u t (c, {e r r}_{i n v a l i d}) \\ e l s e o u t (c, {e r r}_{v o t e}) . \end{array} & \begin{array}{l} {H V o t e r}^{R} (c, i d, c r, p c r, p k) = \\ i n (c, z) . \\ l e t (v^{0}, v^{1}) = ({p r o j}_{1}^{2} (z), {p r o j}_{2}^{2} (z)) i n \\ i f v^{0}, v^{1} \in V o t e s t h e n \\ n e w r^{0} . n e w r^{1} . \\ l e t b^{0} = V o t e (p k, i d, c r, v^{0}, r^{0}) i n \\ l e t b^{1} = V o t e (p k, i d, c r, v^{1}, r^{1}) i n \\ i f V a l i d (i d, p c r, b^{1}, p k) = t r u e \\ t h e n a p p e n d (c, ⟨ i d, b^{0}, b^{1} ⟩_{3}, m_{b b}^{r e f}) . \\ o u t (c, b^{1}) \\ e l s e o u t (c, {e r r}_{i n v a l i d}) \\ e l s e o u t (c, {e r r}_{v o t e}) . \end{array} \end{array}$
They are very similar to the honest ballot box case, except that the $m_{b b}$ list, which was used to store the list of ‘real’ ballots to be tallied, is replaced with a list $m_{b b}^{r e f}$ , that stores no information on the left-hand side, and the correspondence between ‘real’ and ‘fake’ ballots on the right-hand side. Note that ballots are added to $m_{b b}^{r e f}$ before being publicly output: indeed, we wish $m_{b b}^{r e f}$ to store the list of all generated ballots, even ones the attacker may block later by choosing not to add them to the ballot box he will compute.

Since we give the attacker complete control over the ballot box, there is no longer a need for a $D V o t e r$ process to cast ballots in the name of dishonest voters.

Validity check

The ballot box to be tallied will be input directly from the attacker. Since the attacker has direct write access to the ballot box, we first check he has not added invalid ballots to it, and that only one ballot has been submitted per voter (as we exclude revote here).To do so, we will use the $V a l i d (i d, p c r, b, p k)$ recipe. To make the processes more legible, we ask that the attacker provide for each ballot the identity of the voter allegedly casting it. This information is public, so asking that does not restrict the attacker. We thus consider a computation $C_{V a l i d} (b b, c r e d s, p k)$ that takes as parameters a list $b b$ of pairs $(i d, b)$ of an identity and a ballot, a list $c r e d s$ of pairs $(i d, p c r)$ of all identities and public credentials, and the public election key $p k$ . The computation $C_{V a l i d}$ iterates through list $b b$ , and for each element $(i d, b)$ of $b b$ (an element not of that form causes it to fail), goes through $c r e d s$ to:
(i)
check that $i d$ is indeed the identity of an actual voter,
(ii)
retrieve the associated $p c r$ , and
(iii)
check that $V a l i d (i d, p c r, b, p k) = t r u e$ .
In addition, for each $(i d, b)$ in $b b$ , it checks that no other $(i d, b^{'})$ (with the same $i d$ ) is present in $b b$ . We do not extensively write the process $C_{V a l i d}$ here – we have already shown earlier how all the operations it performs (iteration on lists and comparisons) can be implemented as computation processes.

Recovery

Before actually performing the tally, the recovery operation must be performed on the right-hand side. Depending on the way this recovery is done, the resulting definition expresses stronger or weaker guarantees. For this reason, the computational $B P R I V D$ notion from Cortier et al. (12) is defined parametrically w.r.t. the recovery algorithm.

In order to keep our symbolic definition similarly generic, we simply assume a computation $C_{R e c} (b b, {b b}_{r e f})$ . It takes as parameter a list $b b$ of pairs $⟨ i d, b ⟩$ of identities and ballots (to be instantiated with the list produced by the attacker), and a list ${b b}_{r e f}$ of tuples $⟨ i d, b^{0}, b^{1} ⟩_{3}$ (where $b^{0}, b^{1}$ are ballots or $⊥$ ), and computes the list ${b b}_{t a l}$ to be tallied. The recovery and tallying will then be performed in the following process:
$\begin{array}{ll} T a l l y R e c o v e r (c, s k) = & i n (c, b b) . \\ i f C_{V a l i d} (b b, p k (s k)) = t r u e t h e n \\ r e a d m_{b b}^{r e f} a s {b b}_{r e f} . \\ l e t {b b}_{t a l} = C_{R e c} (b b, {b b}_{r e f}) i n \\ l e t r e s = C_{T a l l y} ({b b}_{t a l}, s k) i n \\ o u t (c_{r}, r e s) \\ e l s e o u t (c, {e r r}_{v o t e}) . \end{array}$

Example 11
A typical recovery algorithm consists of going through the list submitted by the attacker, and, for each ballot, checking if it is equal to a ‘fake’ ballot generated by an honest voter. If so, the ballot is replaced with the corresponding ‘real’ ballot for that voter, otherwise, it is left unchanged. That algorithm, as discussed in Cortier et al. (12), leads to a property expressing that the attacker cannot modify honest ballots, but only choose to include them or to remove them – essentially, the ballots must be non-malleable.

We can encode it as the following recovery computation $C_{R e c}^{0} (b b, {b b}_{r e f})$ .[To keep the order of the list unchanged, which is required later on, we write $C_{R e c}^{0}$ using a $r e v$ computation that reverses a list, which is straightforward to construct.]
$\begin{aligned} C_{R e c}^{0} (b b, {b b}_{r e f}) = \\ n e w c . ( & o u t (c, ⟨ b b, n i l ⟩) \\ ∣ & i n (c, ⟨ n i l, {b b}_{t a l} ⟩) . o u t (c_{b}, r e v ({b b}_{t a l})) \\ ∣ & ! i n (c, ⟨ ⟨ i d, b ⟩_{3} :: l, {b b}_{t a l} ⟩) . \\ n e w c^{'} . ( \\ o u t (c^{'}, {b b}_{r e f}) . \\ ∣ i n (c^{'}, n i l) . o u t (c, ⟨ l, b :: {b b}_{t a l} ⟩) \\ ∣! i n (c^{'}, ⟨ {i d}^{'}, b_{0}, b_{1} ⟩_{3} :: l l) . \\ i f b_{1} = b \land ⟨ b_{0}, b_{1} ⟩ \neq ⟨ ⊥, ⊥ ⟩ t h e n o u t (c, ⟨ l, b_{0} :: {b b}_{t a l} ⟩) \\ e l s e o u t (c^{'}, l l))) . \end{aligned}$
As another example, we could encode a variant of that algorithm, useful, for example, in the case of the original Helios protocol, where instead of comparing the entire ballot $b$ to ballots in ${b b}_{r e f}$ , only the ciphertext ${p r o j}_{2} (b)$ is compared. (Recall that in our model of Helios, ballots are $(i d, c i p h e r t e x t)$ – see Example 7). This would express a weaker property overall, as discussed in Cortier et al. (12): the ciphertexts are non-malleable, but the identity included in the ballot is – which makes for a very weak notion of privacy, but accurately characterises the level of security provided by the unpatched Helios.

Assumptions on the recovery computation

Verification tools tend to reason more easily on processes with a similar structure: for this reason, we include the recovery computation on both sides of the equivalence. On the left-hand side, ${b b}_{r e f}$ will only contain $⟨ i d, ⊥, ⊥ ⟩_{3}$ elements, and the recovery should not change the provided ballot box. Hence, we require that $⊥$ values are ignored: $C_{R e c} (b b, {b b}_{r e f})$ and $C_{R e c} (b b, {b b}_{r e f}^{'})$ should return the same result if ${b b}_{r e f}$ and ${b b}_{r e f}^{'}$ are equal up to $⟨ i d, ⊥, ⊥ ⟩_{3}$ elements, and $C_{R e c} (b b, n i l)$ must return $b b$ .

Moreover, we will need for our reduction result to assume that $C_{R e c}$ has the following property, which we call partial recovery. Consider a list $b b$ of terms, and a list
${b b}_{r e f} = [({i d}_{1}, b_{1}^{0}, b_{1}^{1}); \dots; ({i d}_{n}, b_{n}^{0}, b_{n}^{1})]$
containing $n$ honestly generated ballots for distinct voters ${i d}_{i}$ (i.e. computed by the $V o t e$ recipe, with fresh randoms each time). Then we assume

for any permutation ${b b}_{r e f}^{'}$ of ${b b}_{r e f}$ , $C_{R e c} (b b, {b b}_{r e f}^{'}) = C_{R e c} (b b, {b b}_{r e f})$ ;

for any partition ${b b}_{r e f} = {b b}_{r e f}_{1} @ {b b}_{r e f}_{2}$ , $C_{R e c} (b b, {b b}_{r e f}) = C_{R e c} (C_{R e c} (b b, {b b}_{r e f}_{1}), {b b}_{r e f}_{2})$ .

Intuitively that property means that the recovery operation does not depend on the order in which ballots are cast, and can be computed piecewise on a partition of the ballots.

In addition, we assume that $C_{R e c}$ is computable by recipes, in the sense that for any integers $l_{1}$ , $l_{2}$ , there exists a recipe $R_{l_{1}, l_{2}}$ with only two variables $x_{b b}$ , $x_{r e f}$ , such that for all $b b$ of length $l_{1}$ and ${b b}_{r e f}$ of length $l_{2}$ , the result returned by the computation $C_{R e c} (b b, {b b}_{r e f})$ is equal to $R_{l_{1}, l_{2}} [x_{b b} \mapsto b b, x_{r e f} \mapsto {b b}_{r e f}]$ . The recipe $R_{l_{1}, l_{2}}$ may of course depend on the length of the lists – typically, if $C_{R e c}$ iterates through the list $b b$ , it will likely use $h d ({t l}^{n} (x_{b b}))$ to access the $n$ th.

Finally, we add another, more restrictive assumption on the recovery computation.

$C_{R e c}$ preserves the length of the list of ballots it is given: for all $b b, {b b}_{r e f}$ , $C_{R e c} (b b, {b b}_{r e f})$ has the same length as $b b$ ;

$C_{R e c}$ is stable by sub-list: for any $b b$ , ${b b}_{r e f}$ , any sequence $s$ of distinct integers in ${1, \dots, l e n g t h (b b)}$ , if we denote ‘ $\cdot |_{s}$ ’ the operation of keeping in a list only the elements at the positions indicated by the indices in $s$ , then $C_{R e c} (b b |_{s}, {b b}_{r e f}) = C_{R e c} (b b, {b b}_{r e f}) |_{s}$ .

These assumptions, up to the last one, do not seem overly restrictive and hold for all recovery algorithms considered in (12). The final assumption, on the other hand, is much more restrictive: it typically prevents the recovery computation from adding back to the ballot box some ballots that may have been removed by the attacker. Cortier et al. (12) make use of such recovery when modelling variants of the property that express additional verifiability guarantees – basically, by having the recovery add all ballots from the voters who check their vote. We forbid such recovery computations here, meaning that our reduction result does not hold when considering verifiability guarantees. These typically require that a subset of honest voters perform verifications, and get additional assurance that their vote is counted. It is not particularly surprising that these guarantees cannot be captured by only one honest voter.
Example 12
The computation $C_{R e c}^{0} (b b, {b b}_{r e f})$ given in Example 11 satisfies these assumptions. That is clear from its construction for most of them: the partial recovery, ignoring $⊥$ values, length preservation and stability by sublists. The condition that it is computable by recipes is less obvious. In practical examples, such as this one, it is convenient, in order to establish that property, to use an equational theory that includes the term level if–then–else $i t e$ equation introduced in section 2.1. Indeed, with that construction, it becomes quite clear how to construct a (very large) recipe that compares each element of $b b$ with each element of ${b b}_{r e f}$ (for fixed-size lists) and keeps the appropriate ballots. Note that, when the processes we consider do not rely on the term level $i t e$ equation (but only the recipes), adding it does not actually give more distinguishing power to the attacker. Indeed, the attacker could only gain power by using it to produce a recipe that takes different branches on either side, but in that case, only considering the condition of the construction would already produce a boolean that distinguishes the two sides.

$B P R I V D$ against a dishonest ballot box

Overall, the $B P R I V D$ property against a dishonest ballot box is as follows.
Definition 9
A voting scheme is BPRIV D for $p$ honest voters and $n - p$ dishonest voters, written $B P R I V D (p, n - p)$ , if ${E l e c t i o n D}_{p, n - p}^{L} (\vec{v_{1}}, \dots, \vec{v_{n}}) \approx_{t} {E l e c t i o n D}_{p, n - p}^{R} (\vec{v_{1}}, \dots, \vec{v_{n}})$ , where
$\begin{array}{ll} {E l e c t i o n D}_{p, n - p}^{X} (\vec{v_{1}}, \dots, \vec{v_{n}}) = & n e w s k . m_{b b}^{r e f} := n i l . o u t (c h, p k (s k)) . \\ (p h a s e 1. o u t (c_{1}, {p c r}_{1}) . p h a s e 2. {H V o t e r}^{X} (\vec{v_{1}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{p}, {p c r}_{p}) . p h a s e 2. {H V o t e r}^{X} (\vec{v_{p}}, p k (s k)) \\ | p h a s e 1. o u t (c_{p + 1}, ⟨ {c r}_{p + 1}, {p c r}_{p + 1} ⟩) \\ | \dots \\ | p h a s e 1. o u t (c_{n}, ⟨ {c r}_{n}, {p c r}_{n} ⟩) \\ | p h a s e 3. T a l l y R e c o v e r (c h, s k)), \end{array}$
with $c h \in {C h}_{p u b}$ , $X \in {L, R}$ .
6.2. Reduction result with dishonest ballot box

We are now able to state our reduction result when considering a dishonest ballot box.

Theorem 3
Let $V$ be a voting scheme whose associated counting function is $k$ -bounded for some $k \geq 1$ , and $p, n$ be two integers such that $1 \leq p \leq n$ . If $V$ does not satisfy $B P R I V D (p, n - p)$ , then $V$ does not satisfy $B P R I V D (1, k)$ . Moreover, in that case, there exists a witness of this attack where no more than $k$ ballots are present in the ballot box computed by the attacker (each from a different voter).

The proof of this result follows the same steps as the one for the honest ballot box, with the same two main reductions. Note first that the election processes we defined for the dishonest ballot box case are still action-deterministic. In fact, Proposition 1 still holds for these new election processes. Rather than redoing the entire reduction proof, we detail here only the differences with the honest ballot box case.

Step 1:
Reducing the number of honest voters to $1$ . We first show that, assuming $B P R I V D (1, n - 1)$ holds, then $B P R I V D (p, n - p)$ also does. The main idea for this proof is similar to the one for Proposition 2: we define hybrid election processes $P_{i}$ , where the first $i$ honest voters behave like ${H V o t e r}^{R}$ , while the other $p - i$ behave like ${H V o t e r}^{L}$ , going gradually from ${E l e c t i o n D}_{p, n - p}^{L}$ to ${E l e c t i o n D}_{p, n - p}^{R}$ as $i$ increases. Formally, fixing $n$ distinct voters $\vec{v_{1}}, \dots, \vec{v_{n}}$ , with $\vec{v_{i}} = (c_{i}, {i d}_{i}, {c r}_{i}, {p c r}_{i})$ , ${p c r}_{i} = P u b ({c r}_{i}, u_{i})$ for all $i$ , and $p \in {1, \dots, n}$ , we define:
$\begin{array}{l} P_{i} = n e w s k . m_{b b}^{r e f} := n i l . o u t (c h, p k (s k)) . \\ (p h a s e 1. o u t (c_{1}, {p c r}_{1}) . p h a s e 2. {H V o t e r}^{R} (\vec{v_{1}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{i}, {p c r}_{i}) . p h a s e 2. {H V o t e r}^{R} (\vec{v_{i}}, p k (s k)) \\ | p h a s e 1. o u t (c_{i + 1}, {p c r}_{i + 1}) . p h a s e 2. {H V o t e r}^{L} (\vec{v_{i + 1}}, p k (s k)) \\ | \dots \\ | p h a s e 1. o u t (c_{p}, {p c r}_{p}) . p h a s e 2. {H V o t e r}^{L} (\vec{v_{p}}, p k (s k)) \\ | p h a s e 1. o u t (c_{p + 1}, ⟨ {c r}_{p + 1}, {p c r}_{p + 1} ⟩) \\ | \dots \\ | p h a s e 1. o u t (c_{n}, ⟨ {c r}_{n}, {p c r}_{n} ⟩) \\ | p h a s e 3. T a l l y R e c o v e r (c h, s k)) . \end{array}$
We then show that for all $i \in {0, \dots, p - 1}$ , we have that $P_{i} \approx_{t} P_{i + 1}$ . Since the two extreme processes $P_{0}$ , $P_{p}$ are in fact ${E l e c t i o n D}_{p, n - p}^{L}$ and ${E l e c t i o n D}_{p, n - p}^{R}$ , this will prove by transitivity that $B P R I V D (p, n - p)$ holds. Let $i \in {0, \dots, p - 1}$ and $Q_{X} = {E l e c t i o n D}_{1, n - 1}^{X} (\vec{v_{i + 1}}, v e c v_{1}, \dots, \vec{v_{i}}, \vec{v_{i + 2}}, \dots, \vec{v_{n}})$ for $X = L, R$ . By assumption, $B P R I V D (1, n - 1)$ holds, and thus $Q_{L} \approx_{t} Q_{R}$ . To prove that $P_{i} \approx_{t} P_{i + 1}$ , we will show that from a (minimal) witness $t r$ of non-equivalence of these two processes, we can construct a trace $\bar{t r}$ showing the non-equivalence of $Q_{L}$ and $Q_{R}$ . The construction of $\bar{t r}$ is quite similar to the one in the proof of Proposition 2, with some added difficulties. In the honest case, we had to show that the attacker can use dishonest voters to simulate the behaviour of the honest ones and cast the appropriate ballots to obtain the same election result in $Q_{X}$ as in $P_{i}$ , $P_{i + 1}$ . In the case of the dishonest ballot box, this part of the proof is easier: the attacker can reconstruct the ballots from honest voters, except $\vec{v_{i + 1}}$ , in the same way as in the honest case, and simply use these in the recipe that constructs the final ballot box $b b$ . The difficulty comes next: in ${E l e c t i o n D}^{X} (1, n - 1)$ , for all these simulated honest voters, no binding will be added to $m_{b b}^{r e f}$ . Thus, the recovered ballot box ${b b}_{t a l}$ , obtained after the recovery computation, will differ from the one obtained in $P_{i}$ . To avoid this issue, the attacker needs to apply part of the recovery computation himself before submitting the ballot box.

From Proposition 1, $t r$ is $Σ_{e r r}$ -free, is executable in $P_{i}$ , $P_{i + 1}$ , and produces frames $ϕ_{L}$ , $ϕ_{R}$ such that $ϕ_{L} ≁ ϕ_{R}$ . From the form of the processes, we may w.l.o.g. assume that $t r$ is (a prefix of)
$o u t (c h, w_{0}) . p h a s e 1. o u t (c_{i_{1}}, w_{i_{1}}) . \dots . o u t (c_{i_{p}}, w_{i_{p}}) . p h a s e 2. {t r}_{c a s t} . p h a s e 3. i n (c h, R_{b b}) . o u t (c_{r e s}, w_{t a l l}),$
where ${t r}_{c a s t}$ only contains at most one input (recipe $R_{i}$ ) then one output (frame variable $w_{i}^{'}$ ) on each channel $c_{i}$ , and no operation on other channels.

We can define for each $j \in {1, \dots, p}$ with $j \neq i + 1$ recipes $B_{j}^{0}$ , $B_{j}^{1}$ that compute the ballots $b_{0}$ , and $b_{1}$ produced by the honest voter $\vec{v_{j}}$ . We omit the details of that construction, as they are similar to the honest ballot box case. Note that Lemma 4, regarding randomness independence, extends to the $C_{R e c}$ computation, and allows us to rename all private names with fresh public names, as in the previous proof – we will omit the details of that renaming from now on, for better legibility.

Just as in the previous proof, we let $\bar{t r}$ be the trace containing the same actions as $t r$ , except that in ${t r}_{c a s t}$ , all inputs on $c_{j}$ with $j \neq i + 1$ are removed, and the recipe $R_{b b}$ used by the attacker to compute the ballot box for the input in phase 3 is replaced with a new recipe $\bar{R_{b b}}$ , which we will define shortly. Note, first, that regardless of how $\bar{R_{b b}}$ is defined, $\bar{t r}$ is executable in $Q_{L}$ , $Q_{R}$ up to the input in phase 3, and produces at that stage frames ${\bar{ϕ}}_{L}^{'}$ , ${\bar{ϕ}}_{R}^{'}$ .

We first let $R_{b b}^{'} = R_{b b} {w_{j}^{'} \mapsto B_{j}^{1}}_{1 \leq j \leq i} {w_{j}^{'} \mapsto B_{k}^{0}}_{i + 1 \leq j \leq p}$ . Intuitively, $R_{b b}^{'}$ represents the same computation as $R_{b b}$ , except that all ballots produced by the honest voters $\vec{v_{j}}$ , with $j \neq i + 1$ , are replaced with the appropriate recipe (recall that these voters vote the same way in $P_{i}$ , $P_{i + 1}$ ). Just as in the honest case proof, it can be shown that the recipes $B_{j}^{0}$ , $B_{j}^{1}$ produce the expected ballots when applied to both ${\bar{ϕ}}_{L}^{'}$ and ${\bar{ϕ}}_{R}^{'}$ , and thus $R_{b b}^{'}$ , applied to these frames, produces the same ballot boxes ${b b}_{L}$ , ${b b}_{R}$ that $R_{b b}$ computes on $ϕ_{L}$ , $ϕ_{R}$ .

Our goal is to choose $\bar{R_{b b}}$ in such a way that the ballot boxes ${\bar{b b}}_{L}$ , ${\bar{b b}}_{R}$ it produces on ${\bar{ϕ}}_{L}^{'}$ , ${\bar{ϕ}}_{R}^{'}$ will lead, when given to the $T a l l y R e c o v e r$ process, to the same result being output in $Q_{X}$ as the one for ${b b}_{L}$ , ${b b}_{R}$ in $P_{i}$ , $P_{i + 1}$ . The $T a l l y R e c o v e r$ part in these processes differs only in the $C_{R e c}$ computation. Indeed, in $P_{i}$ , $P_{i + 1}$ , that computation operates on a list ${b b}_{r e f, L}$ , ${b b}_{r e f, R}$ (read from $m_{b b}^{r e f}$ ), containing all honest ballots from $\vec{v_{1}}, \dots, \vec{v_{p}}$ . In $Q_{L}$ (respectively, $Q_{R}$ ), the list ${\bar{b b}}_{r e f, L}$ (respectively, ${\bar{b b}}_{r e f, R}$ ) only contains the honest ballot for voter $\vec{v_{i + 1}}$ . Let ${b b}_{r e f}^{'}$ be the list obtained from ${b b}_{r e f, L}, {b b}_{r e f, R}$ by removing the ballot for $\vec{v_{i + 1}}$ . Note that by the construction of $P_{i}$ , $P_{i + 1}$ , that list only contains ballots from voters that behave the same in both processes and is thus the same starting from ${b b}_{r e f, L}$ or ${b b}_{r e f, R}$ . By the partial recovery assumption, the recovery computation can be performed first on ${\bar{b b}}_{r e f, X}$ , (for $X = L, R$ ) and then on ${b b}_{r e f}^{'}$ :
$C_{R e c} ({b b}_{X}, {b b}_{r e f, X}) = C_{R e c} (C_{R e c} ({b b}_{X}, {b b}_{r e f}^{'}), {\bar{b b}}_{r e f, X}) .$
Thus, our goal is achieved if we find a $\bar{R_{b b}}$ that produces the list $C_{R e c} ({b b}_{X}, {b b}_{r e f}^{'})$ when applied to ${\bar{ϕ}}_{X}$ . By assumption, $C_{R e c}$ is computable by recipes, and thus there exists a recipe $R$ with two variables $x_{b b}$ , $x_{r e f}$ such that $C_{R e c} ({b b}_{X}, {b b}_{r e f}^{'}) = R [x_{b b} \mapsto {b b}_{X}, x_{r e f} \mapsto {b b}_{r e f}^{'}]$ for $X = L, R$ . We have already constructed a recipe $R_{b b}^{'}$ producing $b b_{X}$ from ${\bar{ϕ}}_{X}$ . Using the recipes $B_{j}^{0}$ , $B_{j}^{1}$ , and variable $w_{i + 1}^{'}$ , we can easily construct a recipe $R_{2}$ that produces ${b b}_{r e f}^{'}$ from ${\bar{ϕ}}_{X}$ . Choosing $\bar{R_{b b}} = R [x_{b b} \mapsto R_{b b}^{'}, x_{r e f} \mapsto R_{2}]$ then achieves our goal. The trace $\bar{t r}$ obtained using $\bar{R_{b b}}$ as input in phase 3 is executable in $Q_{L}$ , $Q_{R}$ , and produces frames ${\bar{ϕ}}_{L}$ , ${\bar{ϕ}}_{R}$ . Moreover, it leads to the same result being output in ${\bar{ϕ}}_{L}$ (respectively, ${\bar{ϕ}}_{R}$ ) as in $ϕ_{L}$ (respectively, $ϕ_{R}$ ).

The end of the proof is then just as in the honest ballot box case: we show that $ϕ_{L}$ and $ϕ_{R}$ can be reconstructed from ${\bar{ϕ}}_{L}$ , ${\bar{ϕ}}_{R}$ using the same recipe, and thus deduce that since $ϕ_{L} ≁ ϕ_{R}$ , we have ${\bar{ϕ}}_{L} ≁ {\bar{ϕ}}_{R}$ , meaning that $\bar{t r}$ is indeed a witness of non-equivalence of $Q_{L}$ , $Q_{R}$ .
Step 2:
Reducing the number of dishonest voters to $k$ . The second step of the proof is to show that for a $k$ -bounded counting function, if $B P R I V D (1, n)$ does not hold, then neither does $B P R I V D (1, k)$ . We in fact show that there is then a witness of an attack against $B P R I V D (1, k)$ where the ballot box submitted for tallying by the attacker contains at most $k$ ballots.

The proof is very similar to the one for Proposition 4, in the case of an honest ballot box.

Consider a minimal-length attack trace $t r$ on $B P R I V D (1, n)$ , that is, one that distinguishes ${E l e c t i o n D}_{1, n}^{L} (\vec{v_{0}}, \dots, \vec{v_{n}})$ and ${E l e c t i o n D}_{1, n}^{R} (\vec{v_{0}}, \dots, \vec{v_{n}})$ for some distinct voters $\vec{v_{0}}, \dots, \vec{v_{n}}$ . By Proposition 1, we know that the sequence of actions $t r$ is $Σ_{e r r}$ -free, is executable (and reaches the same phase) in both elections processes, where it produces, respectively, frames $ϕ_{L}$ , $ϕ_{R}$ such that $ϕ_{L} ≁ ϕ_{R}$ . Moreover, from the form of the processes, we may assume w.l.o.g. that $t r$ is a prefix of
$o u t (c h, w_{0}) . p h a s e 1. o u t (c_{i_{1}}, w_{i_{1}}) . \dots . o u t (c_{i_{p}}, w_{i_{p}}) . p h a s e 2. {t r}_{c a s t} . p h a s e 3. i n (c h, R_{b b}) . o u t (c_{r e s}, w_{t a l l}),$
where ${t r}_{c a s t}$ only contains at most one input (recipe $R_{0}$ ), then one append, then one output (frame variable $w_{0}^{'}$ ) on channel $c_{0}$ , and no operation on other channels.

We will now show that $t r$ is in fact also a witness that ${E l e c t i o n D}_{1, k}^{L} (\vec{v_{0}}, \dots, \vec{v_{k}}) ≉_{t} {E l e c t i o n D}_{1, k}^{R} (\vec{v_{0}}, \dots, \vec{v_{k}})$ , which will conclude the proof.

As in the case of the honest ballot box, we can distinguish three cases, depending on which point of the execution $t r$ reaches.

Case 1:
$t r$ only contains actions in phases 0 and 1. That is not possible: all messages output in these phases are the same on both sides and thus $t r$ could not be a witness of non-equivalence.
Case 2:
$t r$ contains actions in phases 0, 1, and 2, and potentially the input in phase 3, but not the output in phase 3. In other words, it reaches the casting phase, and the attacker may submit a ballot box, but the execution stops before the result is received. We can immediately discard the case where the input in phase 3 is performed: if that were so, then stopping the execution just before that input would still be an attack witness, since the input itself does not gain the attacker any new information. Hence, $t r$ would not be minimal. In addition, ${t r}_{c a s t}$ necessarily contains an output on $c_{0}$ : otherwise, simply removing it and stopping $t r$ at the end of phase 1 would yield a shorter attack trace, as inputs and appends do not modify the frame. Thus, ${t r}_{c a s t} = i n (c_{0}, R_{0}) . a p p e n d (c_{0}) . o u t (c_{0}, w_{0}^{'})$ . We then conclude with the same argument as in the honest ballot box case. In summary, any dishonest voters outputting their credentials in phase 1 are not needed to construct the frame, as the attacker could obtain the same frame (up to renaming) by using a credential he generated himself. Removing them would produce a shorter attack trace, hence by minimality there are none in $t r$ . Thus, the attack only involves one honest voter, and $t r$ is already an attack trace witnessing ${E l e c t i o n D}_{1, k}^{L} (\vec{v_{0}}, \dots, \vec{v_{k}}) ≉_{t} {E l e c t i o n D}_{1, k}^{R} (\vec{v_{0}}, \dots, \vec{v_{k}})$ .
Case 3:
$t r$ contains all actions from phase $3$ , that is, reaches the final output of the election result. Let us call $R_{b b}$ the recipe provided by the attacker in phase 3, and ${b b}_{L} = R_{b b} ϕ_{L}$ , ${b b}_{R} = R_{b b} ϕ_{R}$ the ballot boxes submitted on the left and right side. Let also ${b b}_{r e f, L}$ , ${b b}_{r e f, R}$ be the lists recording the (only) honest ballot on the left and on the right. With these notations, the election results output on each side is $w_{t a l l} ϕ_{L} = c o u n t (e x t r a c t (C_{R e c} ({b b}_{L}, {b b}_{r e f, L}))$ and $w_{t a l l} ϕ_{R} = c o u n t (e x t r a c t (C_{R e c} ({b b}_{R}, {b b}_{r e f, R})))$ .

By construction of the election process, both ballot boxes pass the validity checks of $C_{V a l i d}$ . Thus, ${b b}_{L}$ and ${b b}_{R}$ are two lists of pairs $⟨ i d, b ⟩$ , where $i d$ is one of the voters’ identities, and $b$ a valid ballot for the credential output for $i d$ in phase 1. Moreover, the $C_{V a l i d}$ computation ensures that all identities in each list are distinct.

By the same reasoning as in the honest ballot box case, the static non-equivalence of $ϕ_{L}$ and $ϕ_{R}$ necessarily comes from the result of the election: $c o u n t (e x t r a c t (C_{R e c} ({b b}_{L}, {b b}_{r e f, L})) \neq c o u n t (e x t r a c t (C_{R e c} ({b b}_{R}, {b b}_{r e f, R})))$ .

The two lists ${b b}_{L}$ , ${b b}_{R}$ have the same length – otherwise, checking their length instead of submitting them as input would let the attacker obtain a smaller non-equivalence witness. Thus, by assumption on $C_{R e c}$ , so do $C_{R e c} ({b b}_{L}, {b b}_{r e f, L})$ and $C_{R e c} ({b b}_{R}, {b b}_{r e f, R})$ . Thus, by the $k$ -boundedness assumption on $c o u n t$ , there exists a sequence $s$ of $k^{'} \leq k$ indices, such that $c o u n t (e x t r a c t (C_{R e c} ({b b}_{L}, {b b}_{r e f, L}) |_{s}) \neq c o u n t (e x t r a c t (C_{R e c} ({b b}_{R}, {b b}_{r e f, R}) |_{s}))$ (recall that ‘ $l |_{s}$ ’ denotes the list obtained by keeping only the elements of indices in $s$ of a list $l$ ).

Then, by assumption on $C_{R e c}$ , we get that keeping only the ballots pointed by $s$ in the ballot box submitted by the attacker leads to a different result: $c o u n t (e x t r a c t (C_{R e c} ({b b}_{L} |_{s}, {b b}_{r e f, L})) \neq c o u n t (e x t r a c t (C_{R e c} ({b b}_{R} |_{s}, {b b}_{r e f, R})))$ . Let $R_{b b}^{'}$ denote the recipe that constructs the list of elements of $R_{b b}$ pointed by indices in $s$ .

These indices point to $k^{'}$ elements of ${b b}_{L}$ , ${b b}_{R}$ , each of the form $(i d, b)$ , where the $i d s$ are distinct voter identities (in $\vec{v_{0}}, \dots, \vec{v_{n}}$ ). Moreover, for each index $i$ , the $i$ th elements of ${b b}_{L}$ and ${b b}_{R}$ necessarily contain the same $i d$ – otherwise, again, as the identities are public values, the attacker could build a shorter attack witness by simply looking at that element. Consequently, the ballots in $R_{b b}^{'} ϕ_{L}$ and $R_{b b}^{'} ϕ_{R}$ are recorded for the same $k^{'}$ distinct voter identities.

Consider the trace $\bar{t r}$ , obtained from $t r$ by keeping in phase 1 only the actions related to those $k^{'}$ voters, and replacing $R_{b b}$ with $R_{b b}^{'}$ – using public names instead of $w_{i}$ variables for removed voters, if they were used in that recipe.

Consider also the ${E l e c t i o n D}_{1, k}^{L}$ and ${E l e c t i o n D}_{1, k}^{R}$ processes featuring the $k^{'}$ voters we kept, plus $\vec{v_{0}}$ (if that voter was not already one of the $k^{'}$ ), and $k - k^{'}$ additional dishonest voters (that are unused in $\bar{t r}$ ). $\bar{t r}$ can be executed in those processes. That is clear up to the input in phase 3. That input is instantiated with ${b b}_{L} |_{s}$ on the left, and ${b b}_{R} |_{s}$ on the right. The validity test is then performed on that ballot box and succeeds – indeed, it succeeded on ${b b}_{L}$ and ${b b}_{R}$ in $t r$ , and by construction the removal of some of the dishonest voters cannot make it fail. The final result election output when executed $\bar{t r}$ is $c o u n t (e x t r a c t (C_{R e c} ({b b}_{L} |_{s}, {b b}_{r e f, L}))$ on the left, and $c o u n t (e x t r a c t (C_{R e c} ({b b}_{R} |_{s}, {b b}_{r e f, R}))$ on the right – two different public values. $\bar{t r}$ is therefore an attack witness on $B P R I V D (1, k)$ , in which the submitted ballot box has length $k^{'} \leq k$ , which concludes the proof.

7. Applications and case studies

To illustrate the generality of our result, and to showcase how useful it can be in practice, we apply it to several well-known voting protocols from the literature considering different counting functions. In this section, we first present the counting functions, as well as the e-voting protocols that we consider for our analysis. Then, we discuss the results we obtained relying on the Proverif tool. Note that the analysis performed using Proverif is only rendered possible thanks to our reduction results that allow one to obtain a bound on the number of voters and on the number of ballots that reach the ballot box.

7.1. Counting functions under study

We apply our results to several case studies considering different counting functions. We have already introduced some classical counting functions in Section 4.1, namely multiset, sum, and majority, and we have shown that they are $1$ -bounded. We now add an example of more involved counting functions: STV, used, for example, in the Australian legislative elections, for which we establish that it is five-bounded when considering three candidates for one seat.

STV is a system where each voter casts a single ballot containing a total ordering of all candidates. A vote goes to the voter’s first choice. If that choice is later eliminated, instead of being thrown away, the vote is transferred to her second choice, and so on. In each round, the least popular candidate is eliminated. His votes are transferred based on voters’ subsequent choices. The process is repeated until one candidate remains, who is declared the winner. We assume a total order $≺$ on candidates is picked beforehand and is used to break ties. The STV counting function outputs a term representing the winning candidate; it is parametrised by the set of candidates and the order $≺$ . Let ${C o u n t}_{S T V}^{3}$ the STV function for candidates ${a, b, c}$ with $a ≺ b ≺ c$ . Votes are 3-tuples: $(c_{1}; c_{2}; c_{3}),$ where ${c_{1}, c_{2}, c_{3}} = {a, b, c}$ and $c_{i}$ denotes the $i^{th}$ choice.

Example 13
Let $v = (a; b; c)$ and $v^{'} = (a; c; b)$ . We have $v \neq v^{'}$ , however, ${C o u n t}_{S T V}^{3} ([v]) = {C o u n t}_{S T V}^{3} ([v^{'}]) = a$ . Thus, the previous reasoning to establish $1$ -boundedness does not apply here.
Lemma 5
${C o u n t}_{S T V}^{3}$ is $5$ -bounded.
Proof.
We assume that $a ≺ b ≺ c$ . Let $ℓ = [v_{1}, \dots, v_{n}]$ and $ℓ^{'} = [v_{1}^{'}, \dots, v_{n}^{'}]$ be two lists of $V o t e s$ such that ${C o u n t}_{S T V}^{3} (ℓ) \neq {C o u n t}_{S T V}^{3} (ℓ^{'})$ . For each $1 \leq i \leq n$ , we denote $(c_{i, 1}; c_{i, 2}; c_{i, 3})$ the vote $v_{i}$ and $(c_{i, 1}^{'}; c_{i, 2}^{'}; c_{i, 3}^{'})$ the vote $v_{i}^{'}$ .

Case 1:
There exists $1 \leq i_{0} \leq n$ such that $v_{i_{0}} = (c_{i_{0}, 1}; c_{i_{0}, 2}; c_{i_{0}, 3})$ and $v_{i_{0}}^{'} = (c_{i_{0}, 1}^{'}; c_{i_{0}, 2}^{'}; c_{i_{0}, 3}^{'})$ with $c_{i_{0}, 1} \neq c_{i_{0}, 1}^{'}$ . In such a case, we keep this vote, and we have $c_{i_{0}, 1} = {C o u n t}_{S T V}^{3} ([v_{i_{0}}]) \neq {C o u n t}_{S T V}^{3} ([v_{i_{0}}^{'}]) = c_{i_{0}, 1}^{'} .$
Case 2:
Otherwise, for $1 \leq i \leq n$ , we have $c_{i, 1} = c_{i, 1}^{'}$ . Thus, in the first round, the eliminated candidate is the same on both sides. Call it $c_{0}$ . If $c_{0}$ does not occur as the first choice on a vote,that is, $c_{0} \neq c_{i, 1}$ for all $i$ (and thus $c_{0} \neq c_{i, 1}^{'}$ , as $c_{i, 1} = c_{i, 1}^{'}$ ), then the eliminated candidate at the second round will be the same on both sides and the winner as well, contradicting our hypothesis.

Hence, $c_{0}$ occurs as the first choice in some votes. Let $i_{0}, \dots, i_{k}$ denote the indices of all such votes. We have $c_{i_{j}, 1} = c_{i_{j}, 1}^{'} = c_{0}$ for any $j \in {0, \dots, k}$ . If the second choice is the same in all these votes, that is, for $j \in {0, \dots, k}$ , we have $c_{i_{j}, 2} = c_{i_{j}, 2}^{'}$ , then the eliminated candidate at the second round, and thus the winner, would be the same on both sides, which contradicts our hypothesis.
Therefore, there exists $j \in {i_{0}, \dots, i_{k}}$ such that $v_{j} = (c_{0}, c_{1}, c_{2})$ , $v_{j}^{'} = (c_{0}, c_{2}, c_{1})$ where ${c_{0}, c_{1}, c_{2}} = {a, b, c}$ . We keep $v_{j}$ , but we need more, as ${C o u n t}_{S T V}^{3} ([v_{j}]) = {C o u n t}_{S T V}^{3} ([v_{j}^{'}]) = c_{0}$ . Since $c_{0}$ is eliminated at the first round: (1)
Either $c_{0} = a$ and there exist $j_{1}, j_{2}$ such that $c_{j_{1}, 1} = c_{j_{1}, 1}^{'} = b$ , and $c_{j_{2}, 1} = c_{j_{2}, 1}^{'} = c$ . Keeping these two votes in addition to $v_{j} / v_{j}^{'}$ , we get ${C o u n t}_{S T V}^{3} ([v_{j}, v_{j_{1}}, v_{j_{2}}]) \neq {C o u n t}_{S T V}^{3} ([v_{j}^{'}, v_{j_{1}}^{'}, v_{j_{2}}^{'}])$ .
(2)
Or $c_{0} = b$ and there exist $j_{1}, j_{2}, j_{3}$ (all distinct) such that $c_{j_{1}, 1} = c_{j_{1}, 1}^{'} = a$ , $c_{j_{2}, 1} = c_{j_{2}, 1}^{'} = a$ , and $c_{j_{3}, 1} = c_{j_{3}, 1}^{'} = c$ . Keeping these three votes in addition to $v_{j} / v_{j}^{'}$ , we have ${C o u n t}_{S T V}^{3} ([v_{j}, v_{j_{1}}, v_{j_{2}}, v_{j_{3}}]) \neq {C o u n t}_{S T V}^{3} ([v_{j}^{'}, v_{j_{1}}^{'}, v_{j_{2}}^{'}, v_{j_{3}}^{'}])$ .
(3)
Or $c_{0} = c$ and there exist distinct $j_{1}, j_{2}, j_{3}, j_{4}$ such that $c_{j_{1}, 1} = c_{j_{1}, 1}^{'} = a$ , $c_{j_{2}, 1} = c_{j_{2}, 1}^{'} = a$ , $c_{j_{3}, 1} = c_{j_{3}, 1}^{'} = b$ , and $c_{j_{4}, 1} = c_{j_{4}, 1}^{'} = b$ . Keeping these four votes in addition to $v_{j} / v_{j}^{'}$ , we get ${C o u n t}_{S T V}^{3} ([v_{j}, v_{j_{1}}, v_{j_{2}}, v_{j_{3}}, v_{j_{4}}]) \neq {C o u n t}_{S T V}^{3} ([v_{j}^{'}, v_{j_{1}}^{'}, v_{j_{2}}^{'}, v_{j_{3}}^{'}, v_{j_{4}}^{'}])$ .
We conclude that at most five votes are needed to ensure the result will be different.

In the following, we consider majority, multiset, sum, and STV (restricted to three candidates).
7.2. E-voting protocols under study

For our case study, we chose the following protocols: two variants of Helios (1), corresponding to its original version, subject to the attack discussed earlier, and a fixed version that includes identities in the ZKP; Belenios (28), and the related BeleniosRF (29) and BeleniosVS (20); Civitas (30); and Prêt-à-Voter (31; 32). Some of the protocols (notably Helios and Belenios) can make use of homomorphic encryption, so that all encrypted votes can be summed before decryption. In our case study, however, we only consider the mixnet version of these protocols, where ballots are instead mixed in a random order before decryption. Indeed, even if our reduction results apply in the presence of homomorphic encryption, Proverif does not support the equations needed to define such a primitive.

Several versions of Helios. We consider several versions of the Helios protocol depending on whether the identity of the voter is part of the zero-knowledge proof (ZKP) or not (1). The original version of Helios is the one without the identity of the voter in the ZKP, which we described in our running example. Note that this protocol is subject to a replay attack, described in Cortier and Smyth,(5) where the attacker submits, in the name of a dishonest voter, a copy of an honest voter’s ballot, which lets him break that voter’s privacy. We do indeed find this attack, even with two voters.

This attack can be mitigated in two ways. The first one consists of adding the voter’s identity to the ZKP, preventing the attacker from replaying it in his name. The second one is weeding, that is, adding a mechanism allowing the server to remove duplicate ballots. However, this operation is only effective if we assume that the ballots emitted by honest voters correctly reach the ballot box. Indeed, the attacker can otherwise simply block the original ballot, and still break the privacy property without the server being able to detect the copy. In our communication model, we decided not to make such a strong assumption, and the attacker is thus able to block messages. Therefore, in our framework, weeding is not a solution to prevent the replay attack mentioned above. We do not study this version of Helios, as the validity test with weeding does not fall in our framework described in Section 3, since we require that the validity test does not depend on the current content of the ballot box.

Note that the framework proposed in (6) makes the assumption that the ballots meant to be counted for each honest voter (typically the last one emitted), which are the ones swapped to express the privacy property, reach the ballot box. Against that weaker attacker, Helios with weeding is secure, as long as voters only vote once. It is not, though, if they revote: the replay could be performed using a previous ballot, which the attacker is allowed to block. Their security analysis correctly finds Helios with weeding secure when revote is disallowed. However, due to a misunderstanding of the reduction result, a replication operator is missing in the case of revote, which leads to the attack being missed in that case.

Several versions of Belenios. The Belenios system (28) builds on Helios and relies on an additional authority who is in charge of distributing to each voter a key pair. The signature key is given to each voter, and the list of associated public keys constitutes the list of eligible voters. Recently, a variant of Belenios, BeleniosRF, designed to ensure receipt-freeness has been proposed (29). It is based on a cryptographic primitive called signatures on randomizable ciphertexts. We also propose an analysis of BeleniosVS that has been designed to achieve both privacy and verifiability against a dishonest voting server (20).

Civitas (30; 33). This system relies on anonymous credentials to enforce privacy. They consist of random values encrypted with the public key of the election authority. Comparison between credentials (e.g. the one used to cast a ballot and those composing the list of legitimate voters) is done by relying on plaintext equivalence tests.

Prêt-à-Voter (34). The ballot contains a detachable list of candidate names, given in a random order (usually the left part), and their corresponding encryption in the same order on the right. Once the voter marked the candidate of his choice, he posts the encrypted part of the ballot (the right part) on the bulletin board. Then, the design of Prêt-à–Voter is similar to other voting systems.

7.3. Results

We conducted the analysis for different counting functions, using our result to bind the number of agents and ballots. We considered majority, multiset, sum, and STV (restricted to three candidates). In fact, in the case of 1-bounded functions, since only one ballot needs to be accepted by the ballot box, the tallying is trivial and ends up being the same for different functions (majority, multiset, etc.). Thus, a single Proverif file is enough to model several counting functions at once. The encoding for modelling STV (5-bounded for three candidates) is more complex, with 6 voters and 5 ballots. We only model this counting function when considering an honest ballot box (with or without revote). In the presence of a dishonest ballot box, the recovery process for 6 voters and 5 ballots will require several nested conditionals, and we anticipate that Proverif (or rather, the recent prototype developed to go beyond diff-equivalence, which is required to conclude on this case) will not be able to obtain results in $< 1 h$ (the timeout we consider here).

We modelled the protocols briefly presented in Section 7.2 as processes satisfying our assumptions, and analysed them using Proverif. We only prove BPRIV itself with Proverif. Strong correctness only involves terms, and can easily be proved by hand. Strong consistency requires us to show that the tallying process rightly computes the tally, which Proverif is not well-suited to do, as it requires (1) modelling the tally in the general case, i.e. with no bounds on the lengths of lists and (2) comparing it to the abstract definition of the counting function, which Proverif cannot really manipulate. The property clearly holds though, and could be proved by hand. We considered both the cases without and with revote, for protocols that support re-voting (except Civitas, which in that case uses rather complex mechanisms that do not fit our setting). [While Civitas does support revote, it uses rather complex mechanisms, in that case, to determine which ballot replaces which, which we chose not to model in our case study.] As mentioned earlier, when revote is allowed, our result does not get rid of the replication operator. Bounding the number of voters is still useful in that case, as it simplifies our models. More importantly, bounding the number of ballots means we can encode the ballot box as a fixed-length list, which is very helpful as Proverif does not support arbitrary length lists. We also performed case studies considering a dishonest ballot box. In that case, our Proverif models are more complex, and we rely on a recent extension of the tool that goes beyond the notion of diff-equivalence (35). Note that this extension of Proverif is a prototype, which is currently unable to exhibit attack traces. Therefore, in case the equivalence does not hold, the result returned is always ‘cannot be proved’.

In some cases, we made slight adjustments to the protocols, so that they fit our framework. Detailed explanations for these modelling choices can be found in the files. All model files for our case study are available in (36). The results are presented in Table 1.

Overall, as can be seen in the table, our result allows for efficient verification of all protocols we considered. Thanks to the small bounds we establish, we get even better performance than previous work (6) in scenarios where that result applies – that is, the first column, for multiset counting. In that case, some analyses took several hours/days in (6), due to the higher bounds. Our result is more general and can handle, for example, STV counting. On most tested protocols, performance remains acceptable in that case. However Proverif did not terminate on three files after 1 h: this is likely due to the combination of the complex equational theories used by these protocols, and the theory for STV, which is itself large. As expected, we find the attack on Helios from Cortier and Smyth (5).

8. Conclusion

We have proposed a symbolic version of the BPRIV vote privacy notion, and established reduction results that help us efficiently verify it on several voting protocols, with different counting functions, using automated tools. We have shown how to extend it to produce a symbolic vote privacy notion against an untrusted ballot box in the symbolic model and proved that our reduction results still hold in that setting.

As mentioned earlier, a limitation of our definition is the modelling of the correct tallying proofs, which we abstracted away. In the computational definition, they are handled using simulators. It remains to be seen whether such techniques can be adapted to the symbolic setting, and how.

Vote privacy is considered a fundamental security property for electronic voting schemes. It is of course not the only desirable one: in particular, receipt-freeness and coercion-resistance can be seen as stronger variants of privacy that require that an attacker should be unable to ascertain the voters’ choice, even when they are willing, or coerced, to reveal their vote. Computational game-based definitions (30) as well as symbolic ones (3) have been proposed for these properties. They are, however, written in the same spirit as SWAP. Proposing formalisations in the style of BPRIV, and establishing similar reduction results to ours for these properties are open questions for future work.

Footnotes

Funding

The author(s) disclosed receipt of the following financial support for the research, authorship, and/or publication of this article: This work received funding from the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.

Declaration of conflicting interests

The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

References

Adida

. Helios: web-based open-audit voting. In: van Oorschot PC (ed.) Proceedings of the 17th USENIX security symposium, San Jose, CA, USA, 28 July–1 August 2008, pp.335–348. Berkeley, CA, USA: USENIX Association.

Benaloh

Yung

. Distributing the power of a government to enhance the privacy of voters (extended abstract). In: Halpern JY (ed.) Proceedings of the 5th annual ACM symposium on principles of distributed computing, Calgary, Alberta, Canada, 11–13 August 1986, pp.52–62. New York, NY, USA: Association for Computing Machinery.

Delaune

Kremer

Ryan

. Verifying privacy-type properties of electronic voting protocols. J Comput Sec 2009; 17: 435–487.

Backes

Hritcu

Maffei

. Automated verification of remote electronic voting protocols in the applied pi calculus. In: Proceedings of the 21st IEEE computer security foundations symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23–25 June 2008, pp.195–209. Los Alamitos, CA, USA: IEEE Computer Society.

Cortier

Smyth

. Attacking and fixing helios: an analysis of ballot secrecy. J Comput Sec 2013; 21: 89–148.

Arapinis

Cortier

Kremer

. When are three voters enough for privacy properties? In: Proceedings of the 21st European symposium on research in computer security (ESORICS’16), Heraklion, Greece, September 26-30, 2016, LNCS, vol. 9879, pp. 241--260. Cham, Switzerland: Springer.

Cortier

Wiedling

. A formal analysis of the Norwegian e-voting protocol. J Comput Sec 2017; 25: 21–57.

Cortier

Galindo

Turuani

. A formal analysis of the Neuchâtel e-voting protocol. In: 3rd IEEE European symposium on security and privacy (Euro S&P’18). London, UK, April 24-26, 2018, pp.430–442. Los Alamitos, CA, USA: IEEE Computer Society.

Basin

Radomirovic

Schmid

. Alethea: a provably secure random sample voting protocol. In: 31st IEEE computer security foundations symposium, (CSF’18), Oxford, UK, July 9-12, 2018, pp. 283--297. Los Alamitos, CA, USA: IEEE Computer Society.

10.

Benaloh

. Verifiable secret-ballot elections. PhD Thesis, Yale University, 1987.

11.

Bernhard

Cortier

Galindo

, et al. A comprehensive analysis of game-based ballot privacy definitions. In: Proceedings of the 36th IEEE symposium on security and privacy (S&P’15), San Jose, CA, USA, May 17-21, 2015, Los Alamitos, CA, USA: IEEE Computer Society.

12.

Cortier

Lallemand

Warinschi

. Fifty shades of ballot privacy: Privacy against a malicious board. In: 33rd IEEE computer security foundations symposium (CSF’20), June 22-26, 2020, Boston, USA, pp.17--32. Los Alamitos, CA, USA: IEEE Computer Society.

13.

Delaune

Hirschi

. A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J Log Algeb Methods Program 2017; 87: 127–144.

14.

Mödersheim

Viganò

. Alpha–beta privacy. ACM Trans Priv Secur 2019; 22: 7:1–7:35, Association for Computing Machinery, New York, NY, USA.

15.

Blanchet

. An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE computer security foundations workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, 11-13 June 2001, pp.82–96. Los Alamitos, CA, USA: IEEE Computer Society.

16.

Blanchet

. Modeling and verifying security protocols with the applied pi calculus and proVerif. Found Trends Privacy Sec 2016; 1: 1–135.

17.

Meier

Schmidt

Cremers

, et al. The TAMARIN prover for the symbolic analysis of security protocols. In: Computer aided verification, 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13-19, LNCS, vol. 8044, 2013, pp.696–701. Cham, Switzerland: Springer.

18.

Blanchet

Abadi

Fournet

. Automated verification of selected equivalences for security protocols. In: 20th IEEE symposium on logic in computer science (LICS 2005), Chicago, IL, 2005, pp.331–340. 26-29 June 2005, Los Alamitos, CA, USA: IEEE Computer Society.

19.

Basin

Dreier

Sasse

. Automated symbolic proofs of observational equivalence. In: Ray I, Li N and Kruegel C (eds.) Proceedings of the 22nd ACM SIGSAC conference on computer and communications security, Denver, CO, USA, 12–16 October 2015, pp.1144-1155. New York, NY, USA: Association for Computing Machinery.

20.

Cortier

Filipiak

Lallemand

. BeleniosVS: Secrecy and verifiability against a corrupted voting device. In: 32nd IEEE computer security foundations symposium, CSF 2019, Hoboken, NJ, USA, 25–28 June 2019. Los Alamitos, CA, USA: IEEE Computer Society.

21.

Blanchet

Smyth

. Automated reasoning for equivalences in the applied pi calculus with barriers. J Comput Sec 2018; 26: 367–422.

22.

Comon-Lundh

Cortier

. Security properties: two agents are sufficient. In: Proceedings of 12th European symposium on programming (ESOP’03), April 7-11, 2003, Warsaw, Poland, LNCS, Vol. 2618, 2003, pp.99–113. Cham, Switzerland: Springer.

23.

Cortier

Dallon

Delaune

. Bounding the number of agents, for equivalence too. In: Proceedings of the 5th International conference on principles of security and Trust (POST’16), April 2-16, 2016, Eindhoven, the Netherlands, LNCS, pp.211–232. Cham, Switzerland: Springer.

24.

Fröschle

. Leakiness is decidable for well-founded protocols? In: Proceedings of the 4th conference on principles of security and trust (POST’15), London, UK, April 11-18, LNCS, vol. 9036, pp. 176–195. Cham, Switzerland: Springer.

25.

D’Osualdo

Ong

Tiu

. Deciding secrecy of security protocols for an unbounded number of sessions: The case of depth-bounded processes. In Proceedings of the 30th computer security foundations symposium, (CSF’17), Santa Barbara, CA, USA, August 21-25, 2017, pp.464–480. Los Alamitos, CA, USA: IEEE Computer Society.

26.

Delaune

Lallemand

. One vote is enough for analysing privacy. In: Atluri V, Pietro RD, Jensen CD, et al. (eds) Computer security – ESORICS 2022 – 27th European symposium on research in computer security, Copenhagen, Denmark, 26–30 September 2022, proceedings, part I, lecture notes in computer science, vol. 13554, 2022, pp.173–194. Cham, Switzerland: Springer. https://doi.org/10.1007/978-3-031-17140-6_9.

27.

Abadi

Fournet

. Mobile values, new names, and secure communication. In: Hankin C and Schmidt D (eds) Conference record of POPL 2001: The 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages, London, UK, 17–19 January 2001, pp.104–115. New York, NY, USA: Association for Computing Machinery.

28.

Cortier

Gaudry

Glondu

. Belenios: A simple private and verifiable electronic voting system. In: Foundations of security, protocols, and equational reasoning – essays dedicated to Catherine A. Meadows, LNCS, 2019, vol. 11565, pp.214–238. Cham, Switzerland: Springer.

29.

Chaidos

Cortier

Fuchsbauer

, et al. BeleniosRF: a non-interactive receipt-free electronic voting scheme. In: 23rd ACM conference on computer and communications security (CCS’16), Vienna, Austria, 2016, pp.1614–1625. New York, NY, USA: Association for Computing Machinery.

30.

Juels

Catalano

Jakobsson

. Coercion-resistant electronic elections. In: Chaum D, Jakobsson M, Rivest RL, et al. (eds) Towards trustworthy elections, new directions in electronic voting, LNCS, vol. 6000, 2010, pp. 37–63. Cham, Switzerland: Springer.

31.

Chaum

Ryan

PYA

Schneider

. A practical voter-verifiable election scheme. In: di Vimercati SDC, Syverson PF and Gollmann D (eds) Computer security – ESORICS 2005, 10th European symposium on research in computer security, Milan, Italy, 12–14 September 2005, proceedings, LNCS, vol. 3679, 2005, pp.118–139. Cham, Switzerland: Springer.

32.

Ryan

PYA

Schneider

. Prêt à voter with re-encryption mixes. In: Gollmann D, Meier J and Sabelfeld A (eds) Computer security – ESORICS 2006, 11th European symposium on research in computer security, Hamburg, Germany, 18–20 September 2006, proceedings, LNCS, vol. 4189, 2006, pp.313–326. Cham, Switzerland: Springer.

33.

Clarkson

Chong

Myers

. Civitas: toward a secure voting system. In: 2008 IEEE symposium on security and privacy (S&P 2008), 18–21 May 2008, Oakland, California, USA, 2008, pp.354–368. Los Alamitos, CA, USA: IEEE Computer Society.

34.

Ryan

PYA

Schneider

35.

Cheval

Rakotonirina

. Indistinguishability beyond diff-equivalence in proverif. In: 36th IEEE computer security foundations symposium, CSF 2023, Dubrovnik, Croatia, 10–14 July 2023, pp.184–199. Los Alamitos, CA, USA: IEEE Computer Society. https://doi.org/10.1109/CSF57540.2023.00036.

36.

Delaune

Lallemand

Outrey

. One vote is enough for analysing privacy. Technical report, CNRS, 2023. https://hal.science/hal-04262499.

Is one vote really enough? Vote privacy with re-voting and a dishonest ballot box

Abstract

Keywords

1. Introduction

Contributions

Related work

2.1. Messages

3.1. Modelling e-voting protocols

Example 9 The V a l i d recipe and C t a l l y computation from Examples 7 and 8 satisfy these assumptions, where e x t r a c t simply decrypts the ciphertext in the ballot, and c o u n t returns the pair of the numbers of votes for y e s and n o . 4. Reduction result

4.1. Main result

5.1. Modelling BPRIV with re-voting

5.2. Reduction result with re-voting

6. Extension to the case of a dishonest ballot box

6.1. Symbolic BPRIV with a dishonest ballot box

Voter processes

Validity check

Recovery

Assumptions on the recovery computation

B P R I V D against a dishonest ballot box

7.1. Counting functions under study

7.3. Results

8. Conclusion

Footnotes

Funding

Declaration of conflicting interests

References

Example 9
The $V a l i d$ recipe and $C_{t a l l y}$ computation from Examples 7 and 8 satisfy these assumptions, where $e x t r a c t$ simply decrypts the ciphertext in the ballot, and $c o u n t$ returns the pair of the numbers of votes for $y e s$ and $n o$ .
4. Reduction result

$B P R I V D$ against a dishonest ballot box