A formal analysis of the Norwegian E-voting protocol

Abstract

Norway used e-voting in its last political election both in September 2011 and September 2013, with more than 28,000 voters using the e-voting option in 2011, and 70,000 in 2013. While some other countries use a black-box, proprietary voting solution, Norway has made its system publicly available. The underlying protocol, designed by Scytl, involves several authorities (a ballot box, a receipt generator, a decryption service, and an auditor). Of course, trusting the correctness and security of e-voting protocols is crucial in that context. In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. ballot secrecy, considering several corruption scenarios. We use a state-of-the-art definition of ballot secrecy, based on equivalence properties and stated in the applied pi-calculus.

Keywords

Ballot secrecy formal methods e-voting

Used in September 2011 and September 2013 for municipality and county elections in Norway [25], e-voting was tested in ten municipalities. During this nationwide local elections, more than 28,000 voters did use internet to cast their vote in 2011 and 70,000 in 2013. While many countries use black-box proprietary solutions, Norway made the protocol publicly available [23]. One key feature of this system is that voters can check that their votes have correctly reached the ballot box (“cast-as-intended” property) without anyone else knowing their vote. The goal of this paper is to conduct a thorough analysis of the Norwegian protocol for the ballot secrecy property: does this system guarantee that no one can know how some voter voted?

Formal methods have been successfully applied to security protocols with the development of several tools such as ProVerif [10], Avispa [4], or Scyther [20] that can automatically analyse both protocols of the literature and fully deployed protocols such as TLS [9]. We therefore chose to model and analyse the Norwegian protocols in a symbolic model named the applied pi-calculus model [1]. A first issue comes from the fact that the underlying encryption primitive is non standard and rather complex. Indeed, the decryption key is split in two shares $a_{1}$ and $a_{2}$ with $a_{3} = a_{1} + a_{2}$ . Each of these three keys $a_{1}$ , $a_{2}$ , $a_{3}$ is given to one administration authority. As further explained in Section 1, this allows for re-encryption and is crucial for the “cast-as-intended” property of the protocol.

Contributions. Our first contribution is a detailed symbolic model for this particular encryption primitive. More precisely, we provide a rewriting system that models El Gamal encryption, re-encryption, blinding function, signatures and zero-knowledge proofs reflecting the primitives used in the protocol. Then, we model the whole system as a process in the applied pi-calculus model. Our second main contribution is a proof of ballot secrecy for several corruption scenarios. Ballot secrecy is typically modeled as follows [21]: an attacker should not be able to distinguish the case where Alice is voting a and Bob is voting b from the converse scenario where Alice is voting b while Bob is voting a. Such a property is typically described by an equivalence of the form $\begin{matrix} Alice (a) ∣ Bob (b) \approx Alice (b) ∣ Bob (a) \end{matrix}$ where $Alice (v)$ represents voter Alice voting for v. Such indistinguishability properties are formalized through behavioral equivalence. Here we use observational equivalence ≈ as defined in [1]. Combined with complex equational theories (in particular equational theories with associative and commutative – AC – operators), no existing tool can check for equivalence. Indeed, dedicated tools such as SPEC [34], APTE [15], or AkisS [13] can only handle standard primitives, with the exception of AkisS which covers more primitives but no AC operators. All three tools are moreover limited to a fixed (and small) number of sessions. Recently, the tool Tamarin has been enhanced to cope with equivalence properties [5] but for the moment it requires a high level of interactions. Therefore, the only natural candidate for an automatic analysis of ballot secrecy is the tool ProVerif [10], one of the most generic tools for security protocols. It can check for equivalence [12] for an unbounded number of sessions. However, ProVerif cannot handle equational theories with AC operators either. [2] devises a technique that transforms an equational theory with AC operators into an equational theory without AC operators, that ProVerif can handle. However, [2] is particular to the re-encryption theory (together with any non AC theory) and it is unclear whether it can be adapted to the complex equational theory needed for the Norwegian protocol. Thus we conducted a preliminary analysis of the Norwegian protocol for a simplified – more abstract – model of the protocol (without AC operators), and finite number of voters.

In order to obtain stronger security guarantees, the full equational theory of the cryptographic primitives should be considered. Therefore, the main contribution of the paper is a proof “by hand” of ballot secrecy for two main corruption scenarios: when all authorities are honest (but all but two voters are corrupted) and when the ballot box is corrupted (and again all but two voters are corrupted). We believe that ballot secrecy can be established in a similar way when the receipt generator is corrupted. A preliminary version of ballot secrecy under the first corruption scenario was presented in [18]. While the encryption scheme used in the Norwegian system is particular to the protocol, the Norwegian system also make use of more standard primitives such as signatures or zero-knowledge proofs. When proving ballot secrecy, we developed generic lemmas that could be re-used in subsequent works (e.g. [3]).

Related Work. Since our initial study of the Norwegian protocol [18], Gjøsteen has proposed a detailed security analysis of the protocol [24] for both ballot secrecy and verifiability, under several trust assumptions (a first model and security definitions already appeared in [23]). A first main difference between the two approaches is the security model: we consider a symbolic model while [23,24] rely on a, more concrete, computational model where the attacker is any polynomial probabilistic Turing machine. In that respect, the study in [23,24] is less abstract and provides more precise security assumptions on the underlying primitives. In contrast, one advantage of symbolic models is that they are more amendable for automation as demonstrated by our use of ProVerif for a simplified model. Ballot secrecy is formalized in two different ways in these two approaches: here, we use a definition of ballot secrecy that is the standard ballot secrecy definition in symbolic models [21]. [23,24] model ballot secrecy (and verifiability) through an ideal functionality that needs to be adapted to the protocol under consideration. Another difference between [23,24] and this work lies in the trust assumptions and the properties that are considered. [23,24] consider both ballot secrecy and verifiability while we focus here on ballot secrecy. Regarding trust assumptions and as it is often the case in other studies of e-voting protocols, at least in symbolic models, we assume that the communications between the voter’s computer and the server can be eavesdropped by an attacker, although in practice, these communications typically happen under some secure channel (e.g. TLS). Whenever possible, it is interesting to prove security without relying on external secure channels since their security is typically not under the control of the authorities, as recently exemplified in an Australian election [26]. In contrast, [23,24] assume private communications between the voter and the server and consider all the cases where one of the authorities is corrupted (while we do not consider the case of a corrupted receipt generator). Interestingly, [23,24] shows that the Norwegian protocol remains secure when the decryption device is corrupted while we show this is not the case. This indicates that, when the decryption device is corrupted, ballot secrecy solely relies on the security of the secure channels used by voters.

Several other e-voting protocols have been studied using formal methods. The FOO [22], Okamoto [32], and Lee et al. [30] voting protocols have been analysed in [21]. Similarly, Helios has been recently proved secure both in a formal [17] and a computational [7,8] model. Helios is actually an implementation of a voting system proposed and analyzed (for the available definitions at that time) by Cramer et al [19]. All these protocols were significantly simpler to analyse in a symbolic model due to the fact that the cryptographic primitives were easier to abstract as a term algebra and due to the fact that these protocols involve less steps. Civitas has been analyzed in [29] in a symbolic model, for a rather rich equational theory. The analysis of this protocol remains simpler than the case of the Norwegian protocol, due to the fact that in Civitas, the voting phase does not involve any interaction with the bulletin board. Our study (together with [23,24]) forms the first security proof of a fully deployed Internet protocol in politically binding elections. Enlarging the scope to voting systems that may take place in polling stations (that is not just Internet voting), security analyses include Scantegrity II [14,29,33], Prêt-à-voter [27], and STAR-Vote [6].

Outline of the paper. We provide an informal description of the protocol in Section 1, including details about the different phases of the voting process. Section 3 presents our formal model of the protocol in the applied pi-calculus. The protocol makes use of a special encryption function in combination with signatures, zero-knowledge proofs, blinding functions, and coding functions. We therefore propose a new equational theory reflecting the unusual behavior of the primitives. The main results and corresponding proofs are presented in Section 4. Section 5 gathers the main lemmas needed for the proofs. We believe these lemmas to be of independent interest in the sense they can be useful for further formal studies of different protocols. Most of the proofs are detailed in Sections F and 6 with some additional lemmas postponed to the appendix. Finally, in Section 7, we present a simplified model of the Norwegian protocol and the corresponding security analysis using ProVerif.

1. The Norwegian e-voting protocol

The Norwegian protocol features four players that define the electronic poll’s infrastructure: a Ballot box (B), a Receipt generator (R), a Decryption service (D) and an Auditor (A). Each Voter (V) can log in using a Computer (P) in order to submit his vote. Channels between computers (voters) and the Ballot box are considered to be authenticated channels, channels between infrastructure’s player are untappable, and channels between voters and receipt generator are unidirectional out-of-band channels. (Example of SMS is given in [23].) The protocol can be divided in three phases: the setting phase, the submission phase, where voters submit their votes, and the counting phase, where ballots are counted and the auditor verifies the correctness of the election.

1.1. Setting phase

Before the election, a finite cyclic group G of some prime order q and generator by $g$ is selected, three private keys $a_{1}$ , $a_{2}$ , and $a_{3}$ (such that $a_{1} + a_{2} \equiv a_{3} [q]$ ) are generated and distributed over respectively D, B, and R, while the corresponding public keys $y_{1} = g^{a_{1}}$ , $y_{2} = g^{a_{2}}$ and $y_{3} = g^{a_{3}}$ are made publicly available Each voter V is assumed to have a signing key $i d_{V}$ , with a corresponding verification key, $vk (i d_{V})$ , which is public. The Ballot box B is provided with a table $V \mapsto s_{V}$ that associates each voter with a blinding factor $s_{V}$ . The Receipt generator R is also assumed to have a signing key $i d_{R}$ , with a corresponding public verification key, $vk (i d_{R})$ ; and it is given, for each voter V, a pseudo-random function $d_{V} : G \to C$ , where $C$ is the set of receipts. Finally, each voter V is assumed to receive by surface mail a table that associates to any voting option $o$ (from the set $O$ ), a precomputed receipt code $d_{V} (f {(o)}^{s_{V}}) \in C$ , where $f : O \to G$ is an injective encoding function.

1.2. Submission phase

Fig. 1.

Submission of one vote.

The submission phase is summarized in Fig. 1. We detail in this section the expected behavior of each participant.

Voter (V). Each voter tells his computer what voting option $o$ to submit and allows it to sign the corresponding ballot on his behalf. Then, he has to wait for an acceptance message coming from the computer and a receipt $\overset{ˇ}{r}$ sent by the receipt generator through some out-of-band channel (typically a SMS message). Using the receipt, he verifies that the correct vote was submitted, that is, he checks that $\overset{ˇ}{r} = d_{V} (f {(o)}^{s_{V}})$ by verifying that the receipt code $\overset{ˇ}{r}$ indeed appears in the line associated to the voting option $o$ he has chosen.

This check ensures in particular the “cast-as-intended” property. In case the voter’s computer is corrupted and encrypts another vote (say the computer wishes to cast a vote for the Pirate party) then this would be eventually discovered by the voter when receiving the receipt.

Computer (P). Voter’s computer encrypts voter’s ballot with the public key $y_{1}$ using standard El Gamal encryption. The resulting ballot is $⟨ g^{r}, y_{1}^{r} f (o) ⟩$ . P also proves that the resulting ciphertext corresponds to a valid voting option, by computing a standard proof of knowledge $pf k_{V}$ . (This proof is formally presented in Section 3, but a detailed description can be found in [23].) P also signs, on the behalf of the Voter, the ballot with $i d_{V}$ and sends it to the Ballot box. It then waits for a confirmation $s i_{R}$ coming from the latter, which is a hash of the initial encrypted ballot, signed by the Receipt generator. After checking this signature, the computer notifies the voter that his vote has been taken into account.

Ballot box (B). Upon receiving an encrypted and signed ballot $b$ from a computer, the Ballot box first checks the correctness of signatures and proofs before re-encrypting the original encrypted ballot with $a_{2}$ and blinding it with $s_{V}$ . B also generates a proof $pf k_{B}$ , showing that its computation is correct. B then sends the new modified ballot $b^{'}$ to the Receipt generator. Once the Ballot box receives a message $s i_{R}$ from R, it simply checks that the Receipt generator’s signature is valid, and sends it to the computer.

Receipt generator (R). Upon receiving an encrypted ballot $b^{'} = ⟨ b, \overset{ˇ}{x}, \overset{ˇ}{w}, \overset{ˇ}{p} ⟩$ from the Ballot box, the Receipt generator first checks signature and proofs (from the computer and the Ballot box). If the validity checks are successful, it generates:

a receipt code $\overset{ˇ}{r} = d_{V} (\overset{ˇ}{w} {\overset{ˇ}{x}}^{- a_{3}})$ sent by out-of-band channel directly to the Voter. Intuitively, the Receipt generator decrypts the (blinded) ballot, applying the function $d_{V}$ associated to the voter. This receipt code gives assurance to the voter that the correct vote was submitted to the Ballot box.

a signature on a hash of the original encrypted ballot for the Ballot box. Once transmitted by B, it is checked and passed on to the Voter’s Computer, which checks it once more and informs the Voter that his vote has been taken into account.

1.3. Counting phase

Once the voting phase is over, the counting phase begins (Fig. 2). The Ballot box selects the encrypted votes $x_{1}, \dots, x_{k}$ which need to be decrypted (if a voter has voted several times, all the submitted ballots remain in the memory of the Ballot box but only the last ballot should be sent) and sends them to the Decryption service. The whole content of the Ballot box $b_{1}, \dots, b_{n}$ ( $n ⩾ k$ ) is revealed to the Auditor, including previous votes from re-voting voters. The Receipt generator sends to the Auditor the list of hashes of ballots it has seen during the submission phase. The Decryption service decrypts the incoming ciphertexts $x_{1}, \dots, x_{k}$ received from the Ballot box and shuffles the decrypted votes before publishing them. It therefore outputs a message of the form $dec (x_{σ (1)}, a_{1}), \dots, dec (x_{σ (k)}, a_{1})$ where σ denotes the permutation obtained by shuffling the votes. It also provides the Auditor with a proof $pf k_{D}$ showing that the input ciphertexts and the outcoming decryption indeed match. Using the Ballot box content and the list of hashes from the Receipt generator, the Auditor verifies that no ballots have been inserted or lost and it computes its own list of encrypted ballots which should be counted. He compares this list with the one received from the Decryption service and checks the proof provided by the latter.

Fig. 2.

Counting phase.

1.4. Security analysis

The rest of the paper is devoted to the modeling and analysis of the protocol. We summarize here informally our main results and we list our main assumptions and simplifications. We formally prove ballot secrecy under two threat scenario:

All but two voters are dishonest and all the authorities (the Ballot box, the Receipt generator, the Decryption service and the Auditor) are honest.

All but two voters are dishonest and all the authorities but the Ballot box are honest.

These two results are obtained assuming authenticated but not necessarily secure communication channels between voters and the Ballot box and Receipt generator, meaning that an attacker may eavesdrop the communications. For this reason, ballot secrecy does not hold as soon as the Decryption device is corrupted. Note also that ballot privacy is also broken as soon as the voter’s computer (P) is corrupted since the voter sends her vote to her computer. We therefore had to assume P to be honest and we chose to model it together with the voter’s behavior. Authentication between the voter and the Ballot box is ensured through a login and password mechanism while authentication from the receipt generator to the voter relies on the out-of-band channel used between them (typically a SMS message).

When modeling the Norwegian protocol in a symbolic model, we had to proceed to some simplifications. First, and as discussed later in Section 3.1, the cryptographic primitives are abstracted by terms together with an equational theory, which potentially leaves out some flaws due to some crafty modifications of some messages. Second, we chose not to model revoting, for simplicity but also since it is explicitly and strongly discouraged in [23], as it may provide to an attacker that control the Ballot box the opportunity to swap the initial and the resubmitted votes. Third, for simplicity, we only consider one-option votes (that voters select one option), rather that a vector of options as in [23]. Finally, we also omit the proof of correct decryption provided by the decryption device since it should not affect ballot secrecy.

2. Applied pi-calculus

We describe here the applied pi-calculus [1], introduced by M. Abadi and C. Fournet. The applied pi-calculus is a process algebra that is often used to model protocols, and we briefly recall here the notations and definitions, providing some examples.

2.1. Terms

Messages are represented by terms built upon an infinite set of names $N$ (for communication channels or atomic data), a set of variables $X$ and a signature Σ consisting of a finite set of function symbols (to represent cryptographic primitives). A function symbol f is assumed to be given with its arity $ar (f)$ . Then, the set of terms $T (Σ, X, N)$ is formally defined by the following grammar:

We write ${^{M_{1}} /_{x_{1}}, \dots,^{M_{n}} /_{x_{n}}}$ for the substitution that replaces the variables $x_{i}$ with the terms $M_{i}$ . $N σ$ refers to the result of applying substitution σ to the free variables of the term N. A term is called ground when it does not contain variables.

In order to represent the properties of the primitives, the signature Σ is equipped with an equational theory E that is a set of equations which hold on terms built from the signature. We denote by $=_{E}$ the smallest equivalence relation induced by E, closed under application of function symbols, substitutions of terms for variables and bijective renaming of names. We write $M =_{E} N$ when the equation $M = N$ holds in the theory E.

Example 1.
A signature for symmetric, asymmetric encryption and signature is $\begin{matrix} Σ = {checksign, dec, pdec, enc, penc, sign, pk} \end{matrix}$ where $penc$ and $pdec$ represent resp. asymmetric (randomized) encryption and decryption, $enc$ and $dec$ stand resp. for symmetric (randomized) encryption and decryption, $sign$ models signature, $checksign$ represents a function that checks the validity of signature, and $pk$ represents the public key associated to a secret key. For example, the term $penc (m, r, pk (s k_{a}))$ represents the asymmetric encryption of the message m with the public key corresponding to the secret key $s k_{a}$ and random factor r. The properties of the cryptographic functions are represented by the equational theory $E_{enc}$ : $\begin{array}{l} dec (enc (m, r, k), k) = m \\ pdec (penc (m, r, pk (s k)), s k) = m \\ checksign (sign (m, s k), pk (s k), m) = ok . \end{array}$ The first equation models that symmetric decryption is only successful if the key used for decryption is the same as the one used for encryption. The second equation reflects that asymmetric decryption only succeeds when the corresponding secret key is used. Finally, the last equation checks that a signature corresponds to a given message and a given verification key.

For some cryptographic primitives, such as homomorphic encryption, it is necessary to introduce associative and commutative symbols. Equational theories including such symbols are called AC-theories. Therefore we define an equality modulo AC, noted $=_{A C}$ , which denotes that two terms are syntactically equal modulo the associative or commutative properties for each AC symbol +. $\begin{array}{l} x + (y + z) = (x + y) + z \\ x + y = y + x \end{array}$ Example 2.
To represent homomorphic encryption, we may use the signature $Σ = {+, , enc}$ with + and ∗ two associative and commutative (AC) symbols and the corresponding equational theory $E_{AC}$ , which includes the associative and commutative properties of + and ∗ symbols, and the equation: $\begin{array}{l} enc (m, k) enc (n, k) = enc (m + n, k) . \end{array}$ This equation models that two ciphertexts encrypted with the same key can be combined to create a ciphertext which corresponding plaintext is the sum of the two previous plaintexts.

2.2. Rewriting system

It might be difficult to work modulo an equational theory. Instead, it is often possible (and more convenient) to reason with a rewriting system. Formally, a rewriting system $R$ is a set of rewriting rules of the form $l \to r$ with l and r two terms. We say that a term s is rewritten in t for rule $l \to r$ , noted $s \to t$ , if there exists a position p in s and a substitution θ such that $s |_{p} = l θ$ and $t = s {[r θ]}_{p}$ .

Definition 1 (Convergence).

A rewriting system $R$ is said convergent if:

for every ground term U, there exists no infinite sequence $U \to U_{1} \to \dots \to U_{k} \to \dots$ . (In this case, we say that $R$ is terminating.)

for every ground terms U, $U_{1}$ , and $U_{2}$ such that $U \to^{*} U_{1}$ and $U \to^{*} U_{2}$ , there exists V such that $U_{1} \to^{*} V$ , and $U_{2} \to V$ . (In this case, we say that $R$ is confluent.)

For AC-theories, we consider rewriting systems modulo AC. Formally, a term s is rewritten modulo AC in t, noted $s \to_{A C} t$ , for a rule $l \to r$ if there exist $s^{'}$ and $t^{'}$ two terms such that $s =_{A C} s^{'}$ , $t =_{A C} t^{'}$ and $s^{'}$ is rewritten in $t^{'}$ for the rule $l \to r$ . Then, it is possible to define the notion of AC-convergence.

Definition 2 (AC-Convergence).

A rewriting system $R$ is said AC-convergent if:

for every ground term U, there is no infinite sequence $U \to_{A C} U_{1} \to_{A C} \dots \to_{A C} U_{k} \dots$ . (In this case, we say that $R$ is AC-terminating.)

for every ground terms U, $U_{1}$ , and $U_{2}$ such that $U \to_{A C}^{*} U_{1}$ and $U \to_{A C}^{*} U_{2}$ , there exists V such that $U_{1} \to_{A C}^{*} V$ , and $U_{2} \to_{A C}^{*} V$ . (In this case, we say that $R$ is AC-confluent.)

2.3. Processes

Processes and extended processes are defined in Fig. 3. The process 0 represents the null process that does nothing. $P ∣ Q$ denotes the parallel composition of P with Q while $! P$ denotes the unbounded replication of P (i.e. the unbounded parallel composition of P with itself). $ν n . P$ creates a fresh name n and then behaves like P. The process $if ϕ then P else Q$ behaves like P if ϕ holds and like Q otherwise. $u (x) . P$ inputs some message in the variable x on channel u and then behaves like P while $\overline{u} ⟨ M ⟩ . P$ outputs M on channel u and then behaves like P. We write $ν \tilde{u}$ for the (possibly empty) series of pairwise-distinct binders $ν u_{1} . \dots . ν u_{n}$ . The active substitution ${^{M} /_{x}}$ can replace the variable x for the term M in every process it comes into contact with and this behaviour can be controlled by restriction, in particular, the process $ν x ({^{M} /_{x}} ∣ P)$ corresponds exactly to $let x = M in P$ .

Fig. 3.

Syntax for processes.

As in [17], we slightly extend the applied pi-calculus by letting conditional branches now depend on formulae defined by the following grammar: $\begin{matrix} ϕ, ψ : : = M = N ∣ M \neq N ∣ ϕ \land ψ \end{matrix}$ If M and N are ground, we define $⟦ M = N ⟧$ to be $true$ if $M =_{E} N$ and $false$ otherwise. The semantics of $⟦ ⟧$ is then extended to formulae as expected.

The scope of names and variables is delimited by binders $u (x)$ and $ν u$ . Sets of bound names, bound variables, free names and free variables are respectively written $bn (A)$ , $bv (A)$ , $fn (A)$ and $fv (A)$ . Occasionally, we write $fn (M)$ (resp. $fv (M)$ ) for the set of names (resp. variables) which appear in term M. An extended process is closed if all its variables are either bound or defined by an active substitution.

An context $C [_]$ is an extended process with a hole instead of an extended process. We obtain $C [A]$ as the result of filling $C [_]$ ’s hole with the extended process A. An evaluation context is a context whose hole is not in the scope of a replication, a conditional, an input or an output. A context $C [_]$ closes A when $C [A]$ is closed.

A frame is an extended process built up from the null process 0 and active substitutions composed by parallel composition and restriction. The domain of a frame φ, denoted $dom (φ)$ is the set of variables for which φ contains an active substitution ${^{M} /_{x}}$ such that x is not under restriction. Every extended process A can be mapped to a frame $φ (A)$ by replacing every plain process in A with 0.

We refer the reader to Section 2.6 for a full example.

2.4. Operational semantics

The operational semantics of processes in the applied pi-calculus is defined by three relations: structural equivalence (≡), internal reduction (→) and labelled reduction ( $\overset{α}{\to}$ ).

Fig. 4.

Structural equivalence.

Structural equivalence is defined in Fig. 4. It is closed by α-conversion of both bound names and bound variables, and closed under application of evaluation contexts. Structural equivalence corresponds to some structural rewriting that does not change the semantics of a process. The internal reductions and labelled reductions are defined in Fig. 5. They are closed under structural equivalence and application of evaluation contexts. Internal reductions represent evaluation of condition and internal communication between processes. Labelled reductions represent communications with the environment.

2.5. Equivalences

Privacy properties are often stated as equivalence relations [21]. Intuitively, if a protocol preserves ballot secrecy, an attacker should not be able to distinguish between a scenario where a voter votes 0 from a scenario where the voter votes 1. Static equivalence formally expresses the indistinguishability of two sequences of terms.

Definition 3 (Static equivalence).

Two closed frames φ and ψ are statically equivalent, denoted $φ \approx_{s} ψ$ , if $dom (φ) = dom (ψ)$ and there exists a set of names $\tilde{n}$ and substitutions $σ, τ$ such that $φ \equiv ν \tilde{n} . σ$ and $ψ \equiv ν \tilde{n} . τ$ and for all terms $M, N$ such that $\tilde{n} \cap (fn (M) \cup fn (N)) = \emptyset$ , we have $M σ =_{E} N σ$ holds if and only if $M τ =_{E} N τ$ holds.

Two closed extended processes $A, B$ are statically equivalent, written $A \approx_{s} B$ , if their frames are statically equivalent; that is, $φ (A) \approx_{s} φ (B)$ .

Intuitively, two sequences of messages φ and ψ are distinguishable to an attacker (i.e. they are not statically equivalent) if the attacker can build a public test $M = N$ that holds for φ but not for ψ (or the converse).

Example 3.
Consider the signature and equational theory $E_{enc}$ defined in Example 1. Let $φ_{1} = ν k . σ_{1}$ and $φ_{2} = ν k . σ_{2}$ where $σ_{1} = {^{penc (s_{1}, r_{1}, pk (k))} /_{x_{1}},^{pk (k)} /_{x_{2}}}$ , $σ_{2} = {^{penc (s_{2}, r_{2}, pk (k))} /_{x_{1}},^{pk (k)} /_{x_{2}}}$ and $s_{1}$ , $s_{2}$ , k are names. We have that $φ_{1} ≉_{s} φ_{2}$ . Indeed, we have $penc (s_{1}, r_{1}, x_{2}) σ_{1} =_{E} x_{1} σ_{1}$ but $penc (s_{1}, r_{1}, x_{2}) σ_{2} \neq_{E} x_{1} σ_{2}$ .

Intuitively, since the randomness of the encryption is public, an attacker may reconstruct the ciphertexts and compare. The two messages become indistinguishable as soon as the randomness remain private. That is, we have that $ν (k, r_{1}) . σ_{1} \approx_{s} ν (k, r_{2}) . σ_{2}$ .

Fig. 5.
Semantics for processes.

Observational equivalence is the active counterpart of static equivalence, where the attacker can actively interact with the processes. The definition of observational equivalence requires to reason about all contexts (i.e. all adversaries), which renders the proofs difficult. Since observational equivalence has been shown to coincide [1,31] with labelled bisimilarity, we adopt the latter in the remaining of the paper.
Definition 4 (Labelled bisimilarity).

Labelled bisimilarity ( $\approx_{l}$ ) is the largest symmetric relation $R$ on closed extended processes such that $A R B$ implies:

$A \approx_{s} B$ ;

if $A \overset{}{\to} A^{'}$ , then $B {\overset{}{\to}}^{*} B^{'}$ and $A^{'} R B^{'}$ for some $B^{'}$ ;

if $A \overset{α}{\to} A^{'}$ such that $fv (α) \subseteq dom (A)$ and $bn (α) \cap fn (B) = \emptyset$ , then $B {\overset{}{\to}}^{*} \overset{α}{\to} {\overset{}{\to}}^{*} B^{'}$ and $A^{'} R B^{'}$ for some $B^{'}$ .

Intuitively, two processes A and B are labelled bisimilar if, anyhow the process A (resp. B) behaves, the process B (resp. A) may behave with the same visible actions and such that their resulting frames are statically equivalent, that is, an attacker cannot distinguish between them.

2.6. A detailed example

We provide a detailed example to illustrate the syntax and semantics of the applied pi-calculus. Readers already familiar with this formalism may skip this section. Let us consider a simple protocol proposed (for illustration purposes) by B. Blanchet [11].

In this protocol, Alice sends a newly generated and signed key k to Bob, the whole message encrypted using his public key $p k_{B}$ . Then, the receiver (Bob) checks that the signature belongs to the intended sender (Alice). He then encrypts a fresh secret s with k using symmetric encryption and sends it to Alice.

To model this protocol in applied-pi calculus, we use the equational theory $E_{enc}$ described in Example 1 that models the properties of the different primitives used in the protocol. The behavior of the sender and receiver are modeled in the applied pi-calculus as follows. $\begin{array}{l} A : = ν k . ν r_{a} . \overline{c} ⟨ penc (sign (k, s k_{a}), r_{a}, p k_{B}) ⟩ . c (x_{1}) \\ B (s) : = c (x_{2}) . B^{'} (s) \\ B^{'} (s) : = let y = pdec (x_{2}, s k_{b}) in \\ if checksign (y, p k_{A}) = ok then B^{″} (s) \\ B^{″} (s) : = ν r_{b} . \overline{c} ⟨ enc (s, r_{b}, k) ⟩ \end{array}$ In these processes, a and b are secret values that correspond to the private key pairs of Alice and Bob, respectively. Since Alice should not have a direct access to b, the secret key of Bob, A is given access to Bob’s public key through a variable $p k_{B}$ and similarly for B. The whole protocol can be easily expressed using Alice and Bob processes: $\begin{matrix} P (s) : = ν (a, b) . [A ∣ B (s) ∣ Γ] \end{matrix}$ where $Γ = {^{pk (s k_{a})} /_{p k_{B}},^{pk (s k_{b})} /_{p k_{B}}}$ . As mentioned above, $s k_{a}$ and $s k_{b}$ are protected but since $pk (s k_{a})$ and $pk (s k_{b})$ are public keys, we published them in a frame implying that they are available to anyone (including the attacker). We first illustrate the semantics of the internal reductions by simulating the normal execution of the protocol, without any interference. $\begin{array}{l} P (s) & \overset{(COMM)}{\to} ν (s k_{a}, s k_{b}, k, r_{a}) . [c (x_{1}) ∣ B^{'} (s) ∣ {^{penc (sign (k, s k_{a}), r_{a}, p k_{B})} /_{x_{2}}} ∣ Γ] \\ \overset{(THEN)}{\to} ν (s k_{a}, s k_{b}, k, r_{a}) . [c (x_{1}) ∣ B^{″} (s) ∣ {^{penc (sign (k, s k_{a}), r_{a}, p k_{B})} /_{x_{2}}} ∣ Γ] \\ \overset{(COMM)}{\to} ν \tilde{n} . [{^{enc (s, r_{b}, k)} /_{x_{1}},^{penc (sign (k, s k_{a}), r_{a}, p k_{B})} /_{x_{2}}} ∣ Γ], with \tilde{n} = (s k_{a}, s k_{b}, k, r_{a}, r_{b}) . \end{array}$ Alice sends her signed and encrypted message, which is received by Bob.

Actually, this simple protocol is flawed. Indeed, an intruder may impersonate Alice’s identity from Bob’s point of view. This attack only requires that Alice had, once in the past, spoken to the intruder using this protocol. This can be showed using our applied-pi calculus model by adding $penc (sign (k_{c}, s k_{a}), r_{c}, p k_{C})$ to the initial frame, which is a message that Alice would have sent to Charlie according to the protocol. Let us define this slightly new process: $\begin{matrix} P_{c} (s) : = ν (s k_{a}, s k_{b}, s k_{c}, r_{c}, k_{c}) . [A ∣ B (s) ∣ Γ_{c}], \end{matrix}$ where $Γ_{c} = {^{penc (sign (k_{c}, s k_{a}), r_{c}, p k_{C})} /_{x},^{pk (a)} /_{p k_{A}},^{pk (b)} /_{p k_{B}},^{pk (s k_{c})} /_{p k_{C}}}$ . Let us consider now the following execution: Charlie can send a message $M = penc (pdec (x, s k_{C}), r^{'}, p k_{B})$ to Bob, where x is the message previously received from Alice.

Let us define the substitution $σ = {^{enc (s, r_{b}, k_{c})} /_{x_{c}},^{M} /_{x_{2}}} ∣ Γ_{c}$ . In this execution, the test performed by B succeeds since, according to the equation theory, we have: $\begin{array}{l} M σ & = penc (pdec (x, sk (c)), r^{'}, p k_{B}) σ \\ = penc (pdec (penc (sign (k_{c}, sk (a)), r_{c}, pk (c)), sk (c)), r^{'}, pk (b)) \\ =_{E_{enc}} penc (sign (k_{c}, sk (a)), r^{'}, pk (b)), \end{array}$ thus, $\begin{array}{l} checksign (pdec (x_{2}, sk (b)), p k_{A}) σ \\ =_{E_{enc}} checksign (pdec (penc (sign (k_{c}, sk (a)), r^{'}, pk (b)), sk (b)), pk (a)) \\ =_{E_{enc}} checksign (sign (k_{c}, sk (a)), pk (a)) \\ =_{E_{enc}} ok \end{array}$ which implies that the message is accepted by B, who therefore believes that Alice just sent him the key $k_{c}$ she had, in fact, sent to Charlie in a former session. At the end of this execution, one can see that s is not secret anymore since Charlie knows $k_{c}$ from his previous exchange and can perform a decryption of $x_{c}$ to get s.

We can also illustrate Definition 4 using this example. Indeed, we have that for any $s_{1}$ and $s_{2}$ , $P (s_{1}) ≉_{l} P (s_{2})$ . This is due to the fact that the two processes may evolve in two states that are not statically equivalent ( $\approx_{s}$ ): $\begin{matrix} P (s_{1}) {\overset{α}{\to}}^{*} P_{1} = ν (a, b, r_{b}) . [A ∣ σ_{1}] and P (s_{2}) {\overset{α}{\to}}^{*} P_{2} = ν (a, b, r_{b}) . [A ∣ σ_{2}] \end{matrix}$ where $α = c (M) . ν x_{c} . \overline{c} ⟨ x_{c} ⟩$ . and $σ_{i}$ is defined as σ where s is simply replaced by $s_{i}$ . We can show that $P_{1} ≉_{s} P_{2}$ , due to the fact that the intruder can observe, using $N_{1} = dec (x_{c}, k_{c})$ and $N_{2} = s_{1}$ , that $(N_{1} =_{E} N_{2}) σ_{1}$ but $(N_{1} \neq_{E} N_{2}) σ_{2}$ .

3. Modeling the Norwegian protocol

We provide a formal specification of the Norwegian protocol, using the framework of the applied pi-calculus, defined in the previous section. We first model the cryptographic primitives used in the protocol (Section 3.1) and then the Norwegian protocol itself (Section 3.2).

3.1. Equational theory

We adopt the following signature to capture the cryptographic primitives used by the protocol. $\begin{array}{l} Σ_{sign} = & {ok, fst, hash, p, pk, s, snd, vk, blind, d, dec, +, *, \circ, ◇, pair, \\ renc, sign, unblind, checkpf k_{1}, checkpf k_{2}, checksign, penc, pf k_{1}, pf k_{2}} \end{array}$ The function $ok$ is a constant; $fst$ , $hash$ , $p$ , $pk$ , $s$ , $snd$ , $vk$ are unary functions; $blind$ , $d$ , $dec$ , +, ∗, ∘, ◇, $pair$ , $renc$ , $sign$ , $unblind$ are binary functions; $checkpf k_{1}$ , $checksign$ , $penc$ are ternary functions; $pf k_{1}$ , $checkpf k_{2}$ are quaternary functions and $pf k_{2}$ is a quinary function.

The term $pk (K)$ denotes the public key corresponding to the secret key K in asymmetric encryption. Terms $s (I)$ , $p (I)$ , and $vk (I)$ are respectively the blinding factor, the parameter and the verification key associated to a secret id I. The specific coding function used by the receipt generator for a voter with secret id I, applied to a message M is represented by $d (p (I), M)$ . It corresponds to the function $d_{V} (M)$ explained in Section 1.2. The term $blind (M, N)$ represents the message M blinded by N. Unblinding such a blinded term P, using the same blinding factor N is denoted by $unblind (P, N)$ . The term $penc (M, N, P)$ refers to the encryption of plaintext M using randomness N and public key P. The term $M \circ N$ denotes the homomorphic combination of ciphertexts and the corresponding operation is written $P ◇ Q$ on plaintexts and $R * S$ on random factors. The decryption of the ciphertext C using secret key K is denoted $dec (C, K)$ . The term $renc (M, K)$ is the re-encryption of the ciphertext M using a secret key K. The addition of secret keys is denoted by $K + L$ . The term $sign (M, N)$ refers to the signature of the message M using secret id N. The term ${pfk}_{1} (M, N, P, Q)$ models a proof of knowledge, linked to the public identity M, that proves that Q is a ciphertext of the plaintext P using randomness N. It models what is provided to convince a prover, and its arguments represents the material needed to construct the proof itself. The term ${pfk}_{2} (M, N, P, Q, R)$ represents a proof of knowledge linked to the public identity M, that R is a blinding of a re-encryption of a term Q using the secret key N and the blinding factor P. $pair (M, N)$ represents the tuple $(M, N)$ . For simplicity, $pair (M_{1}, pair (\dots, pair (M_{n - 1}, M_{n})))$ may be abbreviated as $⟨ M_{1}, \dots, M_{n} ⟩$ and $fst (snd {(M)}^{i - 1})$ as $Π_{i} (M)$ with $i \in N$ .

Fig. 6.

Equations for encryption, blinding, signature and proofs of knowledge.

The properties of the primitives are then modeled by equipping the signature with an equational theory E that asserts that functions +, ∗, ∘ and ◇ are commutative and associative, and includes the equations defined in Fig. 6. The first two equations are quite standard and models left and right projections of a pair of elements. The third equation simply represents usual decryption of a ciphertext using the corresponding secret key, while Eq. (E-4) reflects that a blinded ciphertext can be decrypted, yielding the corresponding blinded plaintext. Equation (E-5) models the homomorphic combination of ciphertexts. Equation (E-6) represents the re-encryption of a ciphertext. The operation of unblinding is described with Eq. (E-7). Equations (E-8), (E-9), and (E-10) correspond to the verification of respectively signature and proofs of knowledge $pf k_{1}$ and $pf k_{2}$ .

The rewriting system corresponding to this equational theory is AC-convergent. This can be proved showing that the system is both AC-confluent and AC-terminating. The first property is true since there is no critical pairs. AC-termination can be shown through a special measure for length of terms $| \cdot |$ defined as follows: $\begin{matrix} | M | = \{\begin{matrix} 1 & if M is a name or a variable, \\ 2 + | M_{1} | + | M_{2} | + | M_{3} | & if M = penc (M_{1}, M_{2}, M_{3}), \\ 2 + | M_{1} | + | M_{2} | & if M = renc (M_{1}, M_{2}), \\ 1 + \sum_{i = 1}^{k} | M_{i} | & otherwise, i.e. M = f (M_{1}, \dots, M_{k}) . \end{matrix} \end{matrix}$ Using this measure, it is easy to check that the length of terms is strictly decreasing at each step of the rewriting, which ensures AC-termination of the rewriting system.

3.2. Norwegian protocol process specification

We present here our model of the Norwegian voting protocol. Each player is modeled as an independent subprocess, and will be instantiated as a part of the whole protocol.

3.2.1. Voting process

The process $V (c_{bal}, c_{rec}, c_{pub}, k_{pub}, {id}_{vot}, {pid}_{rec}, v)$ represents both the voter and his computer.

with $\begin{array}{l} ϕ_{V} ({id}_{vot}, {pid}_{rec}, v, e, p, s i, x_{b}, x_{r}) = & (d (p ({id}_{vot}), blind (v, s ({id}_{vot}))) = x_{r}) \\ \land (checksign (hash (⟨ vk ({id}_{vot}), e, p, s i ⟩), {pid}_{rec}, x_{b}) = ok) . \end{array}$

Parameter v represents voter’s vote and $c_{bal}$ , $c_{rec}$ denote the authenticated channels shared with, respectively, the ballot box and the receipt generator. $k_{pub}$ represents the public key of the election used to encrypt votes; ${id}_{vot}$ is the secret id of the voter and ${pid}_{rec}$ is the verification key of the receipt generator. Note that messages sent over $c_{bal}$ and $c_{rec}$ are also sent on the public channel $c_{pub}$ . This simulates the fact that $c_{bal}$ and $c_{rec}$ are authenticated but not confidential channels. The synchronization step is only here to simplify the study in the case where B is corrupted. The formula $ϕ_{V} ({id}_{vot}, {pid}_{rec}, v, e, p, s i, x_{b}, x_{r})$ models all the checks performed by the voters: the message received from the ballot box should be properly signed and the message from the out-of-band channel should correspond to the right receipt code.

3.2.2. Ballot box

We represent the Ballot box, ready to listen to n voters, by the process $B_{n}$ defined as follows.

with:

and $\begin{array}{l} ϕ_{S} (M, N, U) = (checksign (hash (N), M, U) = ok), \\ \begin{matrix} ϕ_{B} (V, W) = & (W = ⟨ W_{1}, W_{2}, W_{3}, W_{4} ⟩) \land (checkpf k_{1} (W_{1}, W_{2}, W_{3}) = ok) \\ \land (W_{1} = V) \land (checksign (⟨ W_{2}, W_{3} ⟩, W_{1}, W_{4}) = ok) \end{matrix} \end{array}$ where $(X = ⟨ X_{1}, \dots, X_{n} ⟩)$ denotes the formula that holds only when X is a n-tuple. For example, $(X = ⟨ X_{1}, X_{2} ⟩)$ denotes the formula $X = pair (fst (X), snd (X))$ .

Intuitively, we assume the ballots to be received from the authenticated channels $c_{vot}^{1}, \dots, c_{vot}^{n}$ . The Ballot box processes each ballot one after another, exchanging with the Receipt generator through the secure channel $c_{rec}$ , before sending back a confirmation to the Voter. Once all votes have been casted, the Ballot box outputs the encrypted votes to the Decryption device using the secure channel $c_{dec}$ , and its content to the Auditor through the secure channel $c_{aud}$ . $k_{\sec}$ is the secret key known by B, while ${pid}_{vot}^{1}, \dots, {pid}_{vot}^{n}$ are the public identities of the voters (i.e. their verification keys) and $s_{vot}^{1}, \dots, s_{vot}^{n}$ the corresponding blinding factors.

3.2.3. Receipt generator

$R_{n} (c_{bal}, c_{aud}, c_{dec}, c_{pub}, k_{\sec}, {id}_{rec}, c_{vot}^{1}, {pid}_{vot}^{1}, p_{vot}^{1}, \dots, c_{vot}^{n}, {pid}_{vot}^{n}, p_{vot}^{n})$ is the Receipt generator’s process. It exchanges messages with the Ballot box, the Decryption service (only for an ad-hoc synchronization, used to simplify the proof) and the Auditor through secure channels $c_{bal}$ , $c_{dec}$ , and $c_{aud}$ respectively. It also talks directly to voters through out-of-band channels $c_{vot}^{1}, \dots, c_{vot}^{n}$ , which are modeled as authenticated channels here. $k_{\sec}$ is the secret key received by R during the setup phase, ${pid}_{vot}^{1}, \dots, {pid}_{vot}^{n}$ are the public identities of the voters and the corresponding receipt coding functions are $p_{vot}^{1}, \dots, p_{vot}^{n}$ .

with:

and $\begin{array}{l} ϕ_{R} (X, Y) = & (Y = ⟨ Y_{1}, Y_{2}, Y_{3} ⟩) \land (Y_{1} = ⟨ W_{1}, W_{2}, W_{3}, W_{4} ⟩) \land (W_{1} = X) \\ \land (checksign (⟨ W_{2}, W_{3} ⟩, W_{1}, W_{4}) = ok) \land (checkpf k_{1} (W_{1}, W_{2}, W_{3}) = ok) \\ \land (checkpf k_{2} (W_{1}, W_{2}, Y_{2}, Y_{3}) = ok) . \end{array}$

Note that instructions $c_{vot}^{i} ({sync}_{r}^{i})$ and $c_{vot}^{i} ({sync}_{v}^{i})$ are used to force the Receipt Generator to fully process each receipt before accepting a new entry from the Ballot box, which eases the security analysis. Note also that we slightly simplify the behavior of the Receipt Generator. [23] indicates that the Receipt Generator not only computes ${hbr}_{i}$ as defined above but also the hash of the voter’s ballot (obtained when computing $Π_{1} (x_{i})$ ) from which the signature is dropped. We ignore the second hash as it contains less information.

3.2.4. Decryption service

The Decryption service is represented by the process $D_{n} (c_{bal}, c_{rec}, c_{aud}, c_{pub}, k_{\sec})$ . It communicates securely with the Ballot box, the Receipt generator (waiting for synchronization), and the Auditor through respectively channels $c_{bal}$ , $c_{rec}$ , and $c_{aud}$ . The result is published on the public channel $c_{pub}$ . In order to decrypt ballots, it needs to know the secret key $k_{\sec}$ . The parallelism at the end of the process models that the votes are shuffled. For simplicity, we omit the proof of correct decryption provided by the Decryption device as it should not affect privacy.

3.2.5. Auditor

Finally, the Auditor is modeled by the process $A_{n} (c_{bal}, c_{rec}, c_{dec})$ which communicates with the other infrastructure players (Ballot box, Receipt generator, and Decryption device) using secure channels $c_{bal}$ , $c_{rec}$ , and $c_{dec}$ .

with: $\begin{array}{l} ϕ_{A} (H, X_{1}, \dots, X_{n}, Y_{1}, \dots, Y_{n}) = & (hash (⟨ Π_{2} (Y_{1}), \dots, Π_{2} (Y_{n}) ⟩) = H) \\ ⋀_{i = 1}^{n} [(Y_{i} = ⟨ W_{1}, W_{2}, W_{3}, W_{4} ⟩) \land (X_{i} = ⟨ Z_{1}, Z_{2} ⟩) \land (W_{1} = Z_{1}) \\ \land (hash (Y_{i}) = Z_{2}) \land (checksign (⟨ W_{2}, W_{3} ⟩, W_{1}, W_{4}) = ok)] . \end{array}$

3.2.6. Norwegian protocol and corruption scenarios

The interaction of all the players is simply modeled by considering all the processes in parallel, with the correct instantiation and restriction of the parameters. In what follows, the restricted names $a_{1}$ , $a_{2}$ , $a_{3}$ model the private keys used in the protocol and the corresponding public keys $pk (a_{1})$ , $pk (a_{2})$ and $pk (a_{3})$ are added in the process frame. The restricted names $c_{1}$ , $c_{2}$ (resp. $c_{R V_{1}}$ and $c_{R V_{2}}$ ) model authentic channels between the two honest voters and the Ballot box (resp. the Receipt generator). The restricted names $i d_{1}$ , $i d_{2}$ , $i d_{R}$ represent the secret ids of honest voters and of the Receipt generator. The corresponding public id’s are added to the process frame.

The process corresponding to the situation where all the authorities are honest is $P_{n} [_]$ where n is the number of voters and the hole is the voter’s place and is defined as follows: $\begin{matrix} \begin{matrix} P_{n} [_] = & ν \tilde{n} . (let a_{3} = a_{1} + a_{2} in) . [_ \\ ∣ B_{n} (c_{B R}, c_{B D}, c_{B A}, c_{out}, a_{2}, id p_{R}, c_{1}, id p_{1}, s (i d_{1}), \dots, c_{n}, id p_{n}, s (i d_{n})) \\ ∣ R_{n} (c_{B R}, c_{R A}, c_{R D}, c_{out}, a_{3}, i d_{R}, c_{R V_{1}}, id p_{1}, p (i d_{1}), \dots, c_{R V_{n}}, id p_{n}, p (i d_{n})) \\ ∣ D_{n} (c_{B D}, c_{R D}, c_{D A}, c_{out}, a_{1}) ∣ A_{n} (c_{B A}, c_{R A}, c_{D A}) ∣ Γ] \end{matrix} \end{matrix}$ with $\tilde{n} = a_{1}, a_{2}, a_{3}, i d_{1}, i d_{2}, r_{1}, r_{2}, i d_{R}, c_{1}, c_{2}, c_{R V_{1}}, c_{R V_{2}}, c_{B A}, c_{R A}, c_{D A}, c_{B R}, c_{B D}, c_{R D}$ the set of restricted names and the frame $Γ = {^{pk (a_{i})} /_{g_{i}} ∣ i = 1, \dots, 3} ∣ {^{vk (i d_{i})} /_{id p_{i}} ∣ i = 1, 2} ∣ {^{vk (i d_{R})} /_{id p_{R}}}$ . This frame represents the initial knowledge of the attacker: it has access to the public keys of the authorities and the verification keys of the voters. Moreover, since only the two first voters are assumed to be honest, only their two secret ids are restricted (in $\tilde{n}$ ). The attacker has therefore access to the secret ids of all the other voters.

The process $P_{n}$ corresponds therefore to a scenario where all the election authorities are honest. To model the case where the Ballot box is corrupted, we simply provide the attacker with the Ballot box’s secrets. Formally, we define the process $P_{n}^{b}$ defined as follows. $\begin{array}{l} P_{n}^{b} [_] = & ν {\tilde{n}}_{b} . (let a_{3} = a_{1} + a_{2} in) . [_ \\ ∣ R_{n} (c_{B R}, c_{R A}, c_{R D}, c_{out}, a_{3}, i d_{R}, c_{R V_{1}}, id p_{1}, p (i d_{1}), \dots, c_{R V_{n}}, id p_{n}, p (i d_{n})) \\ ∣ D_{n} (c_{B D}, c_{R D}, c_{D A}, c_{out}, a_{1}) ∣ A_{n} (c_{B A}, c_{R A}, c_{D A}) ∣ Γ_{b}] \end{array}$ with ${\tilde{n}}_{b} = a_{1}, a_{3}, i d_{1}, i d_{2}, r_{1}, r_{2}, i d_{R}, c_{R V_{1}}, c_{R V_{2}}, c_{R A}, c_{D A}, c_{R D}$ the set of restricted names and $Γ_{b} = {^{pk (a_{i})} /_{g_{i}} ∣ i = 1, \dots, 3} ∣ {^{vk (i d_{i})} /_{id p_{i}},^{s (i d_{i})} /_{s_{i}} ∣ i = 1, 2} ∣ {^{vk (i d_{R})} /_{id p_{R}}}$ . Compared to $P_{n}$ , we have simply removed $B_{n}$ from the process (since the Ballot box is now under the control of the attacker) and the secret key $a_{2}$ and the authenticated channels $c_{1}, c_{2}, c_{B A}, c_{B R}, c_{B D}$ are now public (they are not part of the set of restricted names anymore). Finally, we have added $s (i d_{1}), s (i d_{2})$ to the frame representing the initial knowledge. This models the fact that now, all the secrets of $B_{n}$ are known to the attacker.

4. Formal analysis of ballot secrecy

Our analysis shows that the Norwegian e-voting protocol preserves ballot secrecy, even when the Ballot box and all but two voters are corrupted, provided that the other components are honest. This of course implies ballot secrecy if all the authorities are honest and some voters are corrupted. Conversely, we identified several cases of corruption that are subject to attacks. Though not surprising, these cases were not explicitly mentioned in the literature.

In this section, we state our main security results, studying the privacy of the Norwegian protocol under two main corruptions scenarios. Moreover, we summarize existing attack scenarios. The formal proof of privacy is then detailed in the next three sections.

Ballot secrecy has been formally defined in terms of equivalence by Delaune, Kremer, and Ryan in [21]. A protocol with process $V (v, i d)$ and authority process A preserves ballot secrecy if an attacker cannot distinguish when votes are swapped, i.e. it cannot distinguish when a voter $a_{1}$ votes $v_{1}$ and $a_{2}$ votes $v_{2}$ from the case where $a_{1}$ votes $v_{2}$ and $a_{2}$ votes $v_{1}$ . This is formally specified by: $\begin{matrix} ν \tilde{n} . (A ∣ V (v_{1}, a_{1}) ∣ V (v_{2}, a_{2})) \approx_{l} ν \tilde{n} . (A ∣ V (v_{2}, a_{1}) ∣ V (v_{1}, a_{2})) \end{matrix}$ Proving ballot secrecy of the Norwegian protocol therefore amounts in proving equivalence of the corresponding processes we detailed in Section 3.

4.1. Corrupted ballot box and corrupted voters

Our main result states that the Norwegian protocol specification satisfies ballot secrecy even if the Ballot box and $n - 2$ voters are corrupted, provided that the other components are honest.

Theorem 1.
Let n be an integer representing the number of voters. Let $P_{n}^{b}$ be the process defined in Section 3.2.6 , that corresponds to the voting process where all the authorities but the Ballot box are honest. Then, $\begin{matrix} P_{n}^{b} [V_{1} (a) ∣ V_{2} (b)] \approx_{l} P_{n}^{b} [V_{1} (b) ∣ V_{2} (a)] \end{matrix}$ with $V_{i} (v_{j}) = V (c_{i}, c_{R V_{i}}, c_{out}, g_{1}, i d_{i}, id p_{R}, v_{j})$ which corresponds to the i-th voter voting $v_{j}$ .

In order to prove Theorem 1, we need to “guess” a symmetric relation $R$ on closed processes satisfying the properties of a labelled bisimilarity. This amounts into describing symbolically all the possible (co-)evolutions of the two processes, depending on the actions of the adversary. The description of this relation is given in Section F. The first step of the proof consists in showing $R$ satisfies property $(1)$ of a bisimilarity relation, that is, we need to show that all pairs of frames obtained in the relation $R$ are in static equivalence. In fact, all these frames are included in the final frames (modulo a “cleaning” step performed using Lemma 12 presented in appendix) corresponding to the complete execution of the two processes. It is therefore sufficient to prove static equivalence of the two final frames.

We consider the following frames: $\begin{array}{l} θ_{init} = {^{vk (i d_{k})} /_{id p_{k}},^{s (i d_{k})} /_{s_{k}} ∣ k = 1, \dots, n} ∣ {^{vk (i d_{R})} /_{id p_{R}}} ∣ {^{pk (a_{k})} /_{g_{k}} ∣ k = 1, \dots, 3}, \\ θ_{0} = θ_{init} ∣ {^{penc (v_{k}, r_{k}, g_{1})} /_{e_{k}},^{{pfk}_{1} (i d_{k}, t_{k}, v_{k}, e_{k})} /_{p_{k}},^{sign (⟨ e_{k}, p_{k} ⟩, i d_{k})} /_{s i_{k}} ∣ k = 1, 2}, \\ θ_{k} = θ_{k - 1} ∣ {^{sign (hash (Π_{1} (M_{k})), i d_{R})} /_{{sr}_{k}},^{d (p (i d_{k}), dec (Π_{2} (M_{k}), a_{3}))} /_{{rec}_{k}}}, \\ θ_{δ} = θ_{n} ∣ {^{dec (U_{δ (k)}, a_{1})} /_{{res}_{k}} ∣ k = 1, \dots, n}, \end{array}$ where $M_{i}$ and $U_{k}$ are free terms such that $fv (M_{i + 1}) \subseteq dom (θ_{i})$ and $fv (U_{k + 1}) \subseteq dom (θ_{n})$ . Intuitively, the $M_{i}$ and $U_{k}$ are the recipes sent by the adversary. The restriction on the variables makes sure the adversary only use terms he has access to, at this step. δ is a substitution of $⟦ 1, n ⟧$ intuitively corresponding to the shuffling of the votes at the end of the election. Then each frame can be interpreted as follows:

$θ_{init}$ corresponds to the initial knowledge of the attacker. It contains the public data of the honest voters and the public keys of the election.

$θ_{0}$ corresponds to the submission of ballots from the two honest voters. Note that our synchronization phase ensures that honest voters vote first. And we can show that the adversary cannot interfere with these two ballots.

$θ_{k}$ corresponds to the knowledge of the adversary once the k-th voter has voted. Intuitively, the adversary will submit any ballot he wishes ( $M_{k}$ ) based on his prior knowledge and in return, he receives the receipt and the signature from the Receipt generator, that is, he receives $d (p (i d_{k}), dec (Π_{2} (M_{k}), a_{3}))$ and $sign (hash (Π_{1} (M_{k})), i d_{R})$ .

Then $θ_{δ}$ corresponds to the frame with the final decryption of the votes, after shuffling, that is, the adversary can see the votes in clear after some permutation δ.
Proposition 1.
Let δ is a substitution of $⟦ 1, n ⟧$ and $^{t} δ = δ \circ [1 \mapsto 2, 2 \mapsto 1]$ . Let $θ_{δ}$ be the frame as defined above. Then we have: $\begin{matrix} ν \tilde{ω} . θ_{δ} σ_{L} \approx_{s} ν \tilde{ω} . θ_{^{t} δ} σ_{R}, with σ_{L} = {^{a} /_{v_{1}},^{b} /_{v_{2}}} and σ_{R} = {^{b} /_{v_{1}},^{a} /_{v_{2}}} . \end{matrix}$

This proposition is the main core result to establish Theorem 1.
Proof sketch.
The proof is done step by step. First, we show that $ν \tilde{ω} . θ_{0} σ_{L} \approx_{s} ν \tilde{ω} . θ_{0} σ_{R}$ , that is, the frames are in static equivalence once the two honest voters have voted (Lemma 13 detailed in appendix). We then show that the receipt sent by the receipt generator does not break static equivalence. This requires to prove in particular that adding the signature of a known term does preserve static equivalence (Lemma 8, one of our core lemma). Finally, we conclude by showing that the decryption of the (shuffled) vote only yields already known terms, built using the same recipes, in both frames.

The full proof of Proposition 1 can be found in Section 6. □

It then remains to show that we did not miss any possible execution, that is, show that $R$ is a bisimilarity relation, which is ensured by the following proposition.
Proposition 2.
Let $R$ be the relation defined in Definition 15 (Section F). Then, $R$ is verifying properties $(2)$ and $(3)$ of Definition 4 .
Proof sketch.
Given $(P, Q) \in R$ , we consider all possible evolutions of P in $P^{'}$ and show that there exists $Q^{'}$ such that $(P^{'}, Q^{'})$ remains in $R$ . In other words, we check that we did not forget any case when defining $R$ . The detailed proof is not really technical but is rather tedious and is therefore deferred to Section F. □

Theorem 1 then easily follows from Proposition 1 and Proposition 2.
4.2. Honest authorities and corrupted voters

The Norwegian e-Voting Protocol specification a fortiori satisfies ballot secrecy even if $n - 2$ voters are corrupted, provided that the other components are honest.

Theorem 2.
Let n be an integer, that corresponds to the number of voters. Let $P_{n}$ be the process defined in Section 3.2.6 , that corresponds to the voting process when all authorities are honest. Then, $\begin{matrix} P_{n} [V_{1} (a) ∣ V_{2} (b)] \approx_{l} P_{n} [V_{1} (b) ∣ V_{2} (a)] \end{matrix}$ with $V_{i} (v_{j}) = V (c_{i}, c_{R V_{i}}, c_{out}, g_{1}, i d_{i}, id p_{R}, v_{j})$ which corresponds to the i-th voter voting $v_{j}$ .

Theorem 2 is a corollary of Theorem 1. While this is intuitively obvious, the use of equivalence adds some technicalities to the proof. The key proposition is that extending the initial knowledge of the attacker can only help finding attacks.
Lemma 1.
Let $\tilde{n}$ be a set of names, P, Q, two processes. Then, we have: $\begin{matrix} ν \tilde{n} . (P ∣ {^{M} /_{x}}) \approx_{l} ν \tilde{n} . (Q ∣ {^{M} /_{x}}) ⟹ ν \tilde{n} . P \approx_{l} ν \tilde{n} . Q . \end{matrix}$
Proof.
We define a symmetric relation $R$ on closed extended processes as follows: $\begin{matrix} ν \tilde{n} . A R ν \tilde{n} . B \overset{def}{⟺} ν \tilde{n} . (A ∣ {^{M} /_{x}}) \approx_{l} ν \tilde{n} . (B ∣ {^{M} /_{x}}) . \end{matrix}$ Let us show that $R$ verifies the three properties of a bisimilarity relation (cf Definition 4).
This is straightforward since $ϕ (ν \tilde{n} . A) \subseteq ϕ (ν \tilde{n} . (A ∣ {^{M} /_{x}}))$ .

Let $A \to A^{'}$ . Then $ν \tilde{n} . (A ∣ {^{M} /_{x}}) \to ν \tilde{n} . (A^{'} ∣ {^{M} /_{x}})$ . Now, since $A R B$ , we have that $ν \tilde{n} . (A ∣ {^{M} /_{x}}) \approx_{l} ν \tilde{n} . (B ∣ {^{M} /_{x}})$ thus there exists $\overline{B}$ such that $ν \tilde{n} . (B ∣ {^{M} /_{x}}) \to^{} \overline{B}$ and $\overline{B} \approx_{l} ν \tilde{n} . (A^{'} ∣ {^{M} /_{x}})$ . Since B is a closed process, it can not make use of x thus it must be the case that there exists $B^{'}$ such that $B \to^{} B^{'}$ and $\overline{B} \equiv ν \tilde{n} . (B^{'} ∣ {^{M} /_{x}})$ . Moreover since $ν \tilde{n} . (A^{'} ∣ {^{M} /_{x}}) \approx_{l} \overline{B} \equiv ν \tilde{n} . (B^{'} ∣ {^{M} /_{x}})$ , we conclude that $A^{'} R B^{'}$ .

Let $A \overset{α}{⟶} A^{'}$ . Then $ν \tilde{n} . (A ∣ {^{M} /_{x}}) \overset{α}{⟶} ν \tilde{n} . (A^{'} ∣ {^{M} /_{x}})$ . Now, since $A R B$ , we have that $ν \tilde{n} . (A ∣ {^{M} /_{x}}) \approx_{l} ν \tilde{n} . (B ∣ {^{M} /_{x}})$ thus there exists $\overline{B}$ such that $ν \tilde{n} . (B ∣ {^{M} /_{x}}) \to^{} \overset{α}{⟶} \to^{} \overline{B}$ and $\overline{B} \approx_{l} ν \tilde{n} . (A^{'} ∣ {^{M} /_{x}})$ . Since A is a closed process, it does not contain x, thus we must have that the label α does not contain x either. Thus, if $ν \tilde{n} . (B ∣ {^{M} /_{x}}) \to^{} \overset{α}{⟶} \to^{} \overline{B}$ , we must have that there exists $B^{'}$ such that $B \to^{} \overset{α}{⟶} \to^{} B^{'}$ and $\overline{B} \equiv ν \tilde{n} . (B^{'} ∣ {^{M} /_{x}})$ . Moreover since $ν \tilde{n} . (A^{'} ∣ {^{M} /_{x}}) \approx_{l} \overline{B} \equiv ν \tilde{n} . (B^{'} ∣ {^{M} /_{x}})$ , we conclude that $A^{'} R B^{'}$ .
Now, since $\approx_{l}$ is the largest relation satisfying these three properties, we conclude. □

We are now ready to prove Theorem 2. Proof of Theorem 2.
Let us define $A = P_{n}^{b} [V_{1} (a) ∣ V_{2} (b)]$ and $B = P_{n}^{b} [V_{1} (b) ∣ V_{2} (a)]$ . According to Theorem 1, we have that: $A \approx_{l} B$ . Thus, for all closing evaluation context $C [_]$ , we also have: $C [A] \approx_{l} C [B]$ . Let us consider the following closing evaluation context: $\begin{matrix} C [_] = ν \tilde{m} . [_∣ B_{n} (c_{B R}, c_{B D}, c_{B A}, c_{out}, a_{2}, id p_{R}, c_{1}, id p_{1}, s_{1}, \dots, c_{n}, id p_{n}, s_{n})], \end{matrix}$ with $\tilde{m} = a_{2}, c_{1}, c_{2}, c_{B R}, c_{B D}$ and $B_{n}$ is defined as the honest one except that we replace arguments $s (i d_{1})$ and $s (i d_{2})$ by variables $s_{1}$ and $s_{2}$ . Then: $\begin{matrix} C [A] = ν \tilde{m} . [ν {\tilde{n}}_{b} . (let a_{3} = a_{1} + a_{2} in) . (V_{1} (a) ∣ V_{2} (b) ∣ R_{n} ∣ D_{n} ∣ Γ_{b}) σ_{L} ∣ B_{n}] \end{matrix}$ where $B_{n}$ , $R_{n}$ and $D_{n}$ are just short notations of the different processes with their attributes. Since $B_{n}$ is such that $(fv (B_{n}) \cup fn (B_{n})) \cap {\tilde{n}}_{b} = \emptyset$ , we have that: $\begin{array}{l} C [A] & = ν \tilde{m} . [ν {\tilde{n}}_{b} . (let a_{3} = a_{1} + a_{2} in) . (V_{1} (a) ∣ V_{2} (b) ∣ B_{n} ∣ R_{n} ∣ D_{n} ∣ Γ_{b})] \\ = ν (\tilde{m}, {\tilde{n}}_{b}) . (let a_{3} = a_{1} + a_{2} in) . [V_{1} (a) ∣ V_{2} (b) ∣ B_{n} ∣ R_{n} ∣ D_{n} ∣ Γ_{b}] . \end{array}$ But $(\tilde{m}, {\tilde{n}}_{b}) = \tilde{n}$ and: $\begin{array}{l} B_{n} (c_{B R}, c_{B D}, c_{B A}, c_{out}, a_{2}, id p_{R}, c_{1}, id p_{1}, s_{1}, \dots, c_{n}, id p_{n}, s_{n}) Γ_{b} \\ = B_{n} (c_{B R}, c_{B D}, c_{B A}, c_{out}, a_{2}, id p_{R}, c_{1}, id p_{1}, s (i d_{1}), \dots, c_{n}, id p_{n}, s (i d_{n})) Γ_{b} . \end{array}$ So, we get that $C [A] = {\overline{P}}_{n} [V_{1} (a) ∣ V_{2} (b)]$ , where ${\overline{P}}_{n}^{a}$ is exactly the same as $P_{n}$ except that Γ is replaced by $Γ_{b}$ . Doing the same for $C [B]$ , we deduce that $C [B] = {\overline{P}}_{n} [V_{1} (b) ∣ V_{2} (a)]$ and thus ${\overline{P}}_{n} [V_{1} (a) ∣ V_{2} (b)] \approx_{l} {\overline{P}}_{n} [V_{1} (b) ∣ V_{2} (a)]$ . According to Lemma 1, this equivalence implies that: $\begin{matrix} P_{n} [V_{1} (a) ∣ V_{2} (b)] \approx_{l} P_{n} [V_{1} (b) ∣ V_{2} (a)] . \end{matrix}$ □

4.3. Attacks

We have shown that the Norwegian protocol guarantees ballot privacy provided that the Receipt generator, the Decryption service, and the Auditor are honest. We review further cases of corruption where ballot secrecy is no longer guaranteed.

Dishonest decryption service. The Decryption service is a very sensitive component since it has access to the decryption key $a_{1}$ of the public key used for the election. Therefore, a corrupted Decryption service can very easily decrypt all encrypted ballots and thus learns the votes as soon as he has access to the communication between the voters and the Ballot box. Such an attack is not possible in [23,24] since communications are assumed to be secure (e.g. using TLS channels). It is interesting to note that the combination of both studies indicates that in case the Decryption service is corrupted then ballot secrecy solely relies on the security of the communication channels between the voters and the Ballot box.

Dishonest ballot box and receipt generator. Clearly, if the Ballot box and the Receipt generator collude, they can compute $a_{1} = a_{3} - a_{2}$ and they can then decrypt all incoming encrypted ballots. More interestingly, a corrupted Receipt generator does not need the full cooperation of the ballot box for breaking ballot secrecy. Indeed, assume that the Receipt generator has access, for some voter V, to the blinding factor $s_{V}$ used by the Ballot box to blind the ballot. Recall that the Receipt generator retrieves $f {(o)}^{s_{V}}$ when generating the receipt codes (by computing $\overset{ˇ}{w} {\overset{ˇ}{x}}^{- a_{3}}$ ). Therefore, the Receipt generator can compute $f {(o^{'})}^{s_{V}}$ for any possible voting option $o^{'}$ . Comparing with the obtained values with $f {(o)}^{s_{V}}$ it would easily deduce the chosen option $o$ . Of course, the more blinding factors the Receipt generator can get, the more voters it can attack. Therefore, the security of the protocol strongly relies on the security of the blinding factors which generation and distribution are left unspecified in the documentation (who has access to the data during the generation? How the data are distributed and how secure the distribution is?). The Ballot box can also perform a similar attack provided that it has access to the SMS sent by the Receipt generator and provided it can learn the coding function $d_{V}$ for some voters V (which probably requires partial corruption of the Receipt generator as well). Note that if the Ballot box and the Receipt generator collude, verifiability is broken as well, as pointed in [23,24], since votes can be changed without voters noticing.

Dishonest ballot box and auditor. Even if the Auditor does not hold any secret (besides the access to the output of both the Ballot box and the Receipt generator), it is still a key component in the voting process. Indeed, it ensures that the ballots sent to the Decryption service indeed correspond to the ballots sent by the voters (unless both the Ballot box and the Receipt generator are corrupted). Assume now that the Ballot box and the Auditor corrupted. Then the Ballot box can send any ballots it wants to the Decryption service (the – corrupted – Auditor would not complain). This is a clear breach of security in terms of the correctness of the result: indeed, the results would not correspond to the votes as casted by the voters (as also pointed in [23,24]). As a consequence, this is also a breach of ballot privacy. Indeed, the Ballot box may send the same ballot several times (possibly re-randomized) therefore obtaining a bias of information about the vote casted by the voter under attack.

5. Lemmas for static equivalence

The proof of our main result requires several intermediate lemmas. We believe that some of them are of independent of interest. We first state lemmas that are independent of the equational theory (Section 5.1) and then one of them that relies on it but is still quite general and could be reused for other formal studies of protocols (Section 5.2).

5.1. Generic lemmas

We use some arguments repetitively on our proofs and we found useful to state them separately. First, we notice that splitting pairs preserves static equivalence.

Lemma 2.
Let $\tilde{n}, \tilde{m}$ be names, $θ_{1}, θ_{2}$ substitutions and let us define $ϕ = ν \tilde{n} . (θ_{1} ∣ {^{⟨ U_{1}, U_{2} ⟩} /_{x}})$ and $ψ = ν \tilde{m} . (θ_{2} ∣ {^{⟨ V_{1}, V_{2} ⟩} /_{x}})$ two frames with $U_{1}$ , $U_{2}$ , $V_{1}$ , $V_{2}$ some terms. We have: $\begin{matrix} ϕ \approx_{s} ψ ⟺ ν \tilde{n} . (θ_{1} ∣ {^{U_{1}} /_{x_{1}},^{U_{2}} /_{x_{2}}}) \approx_{s} ν \tilde{m} . (θ_{2} \cup {^{V_{1}} /_{x_{1}},^{V_{2}} /_{x_{2}}}) . \end{matrix}$
Proof.
Let $ϕ^{'} = ν \tilde{n} . (θ_{1} ∣ {^{U_{1}} /_{x_{1}},^{U_{2}} /_{x_{2}}})$ and $ψ^{'} = ν \tilde{m} . (θ_{2} \cup {^{V_{1}} /_{x_{1}},^{V_{2}} /_{x_{2}}})$ .

Let M, N be terms s.t. $(M =_{E} N) ϕ^{'}$ . We consider $δ = [x_{1} \mapsto Π_{1} (x), x_{2} \mapsto Π_{2} (x)]$ and we have, for all term P: $(P δ) ϕ =_{E} P ϕ^{'}$ and $(P δ) ψ =_{E} P ψ^{'}$ . Thus $M ϕ^{'} =_{E} N ϕ^{'}$ implies $(M δ) ϕ =_{E} (N δ) ϕ$ . Since $ϕ \approx_{s} ψ$ we deduce $(M δ) ψ =_{E} (N δ) ψ$ , that is $M ψ^{'} =_{E} N ψ^{'}$ . Since ϕ and ψ play a symmetric role, we deduce that $M ψ^{'} =_{E} N ψ^{'}$ implies $M ϕ^{'} =_{E} N ϕ^{'}$ as well. □

Adding a deducible term to the frames preserves static equivalence, provided the condition that the same recipe is used in the two frames.
Lemma 3.
Let $\tilde{n}, \tilde{m}$ be names, $θ_{1}, θ_{2}$ substitutions, and $ϕ = ν \tilde{n} . θ_{1}$ and $ψ = ν \tilde{m} . θ_{2}$ frames. Let U be a free term, we have: $\begin{matrix} ϕ \approx_{s} ψ ⟺ ν \tilde{n} . (θ_{1} ∣ {^{U θ_{1}} /_{x}}) \approx_{s} ν \tilde{m} . (θ_{2} \cup {^{U θ_{2}} /_{x}}) . \end{matrix}$
Proof.
Let $ϕ^{'} = ν \tilde{n} . (θ_{1} ∣ {^{U θ_{1}} /_{x}})$ and $ψ^{'} = ν \tilde{m} . (θ_{2} \cup {^{U θ_{2}} /_{x}})$ .

$⟸ ∣$ Straightforward.

$⟹ ∣$ Let M, N be terms such that $(M =_{E} N) ψ^{'}$ . We consider $δ : x \mapsto U$ and we have, for all term P: $(P δ) ϕ =_{E} P ϕ^{'}$ and $(P δ) ψ =_{E} P ψ^{'}$ . Thus $M ϕ^{'} =_{E} N ϕ^{'}$ implies $(M δ) ϕ =_{E} (N δ) ϕ$ . Since $ϕ \approx_{s} ψ$ , we deduce $(M δ) ψ =_{E} (N δ) ψ$ , that is $M ψ^{'} =_{E} N ψ^{'}$ . □

The next lemmas hold for equational theories for which destructors can be identified.
Definition 5.
Let E be an equational theory induced by an AC convergent rewriting system $R$ and Σ a signature. We say that $f \in Σ$ is a destructor in E if for any rewrite rule $l \to r$ of $R$ $\begin{matrix} f \notin r and (f \notin l or l = f (l_{1}, \dots, l_{n}) and \forall i \in ⟦ 1, n ⟧, f \notin l_{i}), \end{matrix}$ i.e. f can only appear in head in l and does not appear in r. Terms of the form $f (t_{1}, \dots, t_{n})$ with f destructor in E are called destructor terms.

The next lemma states that destructor terms cannot be introduced by rewriting rules.
Lemma 4.
Let E be an equational theory induced by an AC-convergent rewriting system $R$ , Σ a signature and $f \in Σ$ a destructor in E. Let $C [_]$ be a context such that $f \notin C$ and let $T_{1}, \dots, T_{n}$ be terms in normal form. Then there exists a context $C^{'} [_]$ such that $f \notin C^{'}$ and $C [T_{1}, \dots, T_{n}] \to C^{'} [M_{1}, \dots, M_{p}]$ where $M_{1}, \dots, M_{p}$ are subterms of $T_{1}$ , …, $T_{n}$ .
Proof.
Let us consider such context $C [_]$ and such terms $T_{1}, \dots, T_{n}$ . For this proof, we also consider that we flatten AC symbols, i.e. a term $\oplus (x, \oplus (y, z))$ will be considered as $\oplus (x, y, z)$ for any AC symbol ⊕. Moreover, we can consider w.l.o.g. that each $T_{i}$ does not start with an AC-symbol. If $T_{i} = \oplus (N_{1}, \dots, N_{q})$ for one $i \in ⟦ 1, n ⟧$ , then we can consider $\overline{C} [_]$ a new context deduced from $C [_]$ by adding a ⊕ symbol at each position $T_{i}$ should be inserted in $C [_]$ . Then, we have: $\begin{matrix} C [T_{1}, \dots, T_{n}] =_{A C} \overline{C} [T_{1}, \dots, T_{i - 1}, N_{1}, \dots, N_{q}, T_{i + 1}, \dots, T_{n}] . \end{matrix}$ Now, if $C [T_{1}, \dots, T_{n}]$ is in normal form, the result is straightforward. If it is not, then we know that there exists a position s, a rule $l \to r$ from $R$ and a substitution θ such that $C [T_{1}, \dots, T_{n}] |_{s} =_{A C} l θ$ . Let x be a variable of l and $p_{x}$ be a position such that $l |_{p_{x}} = x$ . We know that $p_{x}$ can’t be the root, otherwise $l = x$ and $R$ would contain a rule $x \to r$ . Such a rule would allow infinite chains of reduction which is in contradiction with hypothesis on $R$ . Thus, we can move one step up and call $p_{s}$ the position such that $p_{x} = p_{s} * j$ with $j \in N^{}$ and $l |_{p_{s}} = g \in Σ$ . We consider two cases:
g is not an AC-symbol. We consider two subcases:

$p_{x}$ is a position of $C [_]$ . Then $x θ =_{A C} C_{x} [T_{1}, \dots, T_{n}]$ with $C_{x} [_]$ a sub context of $C [_]$ and we can replace the substitution of x in θ by ${^{C_{x} [T_{1}, \dots, T_{n}]} /_{x}}$ .

$p_{x}$ is not a position of $C [_]$ , i.e. there exists $p_{i}$ and $p_{2}$ two positions such that $p_{x} = p_{i} p_{2}$ with $C [T_{1}, \dots, T_{n}] |_{p_{i}} =_{A C} T_{i}$ and $T_{i} |_{p_{2}} =_{A C} x θ =_{A C} W$ with $W \in St (T_{i})$ . In that case, we can just replace the substitution of x in θ by ${^{W} /_{x}}$ .

$g = \oplus$ , an AC-symbol. Then, we have $l |_{p_{s}} =_{A C} x \oplus l^{'}$ . We consider again two subcases:

Either $p_{s}$ is a position of $C [_]$ . Then, $l |_{p_{s}} θ =_{A C} (x \oplus l^{'}) θ =_{A C} C_{x} [T_{1}, \dots, T_{n}]$ . Thus, $head (C_{x} [T_{1}, \dots, T_{n})) = \oplus$ and we can expand it as follows: $\begin{matrix} C_{x} [T_{1}, \dots, T_{n}] =_{A C} ⨁_{i = 1}^{m_{1}} C_{x}^{i} [T_{1}, \dots, T_{n}] ⨁_{j = 1}^{m_{2}} W_{j} \end{matrix}$ with $C_{x}^{i} [_]$ subcontexts of $C_{x} [_]$ and $W_{j}$ being one of $T_{1}, \dots, T_{n}$ . Then, each $x θ$ is linked to a subset of this sum and we can replace the substitution of x in θ by ${^{⨁_{i = 1}^{w_{1}} C_{x}^{i} [T_{1}, \dots, T_{n}] ⨁_{j = 1}^{w_{2}} W_{j}} /_{x}}$ with $w_{1} ⩽ m_{1}$ and $w_{2} ⩽ m_{2}$ .

Or $l |_{p_{s}} θ =_{A C} W$ with $W \in St (T_{i})$ for one $i \in ⟦ 1, n ⟧$ . Then, $x θ$ is subterm of W and we conclude.
Finally, for each case, we have that $l θ =_{A C} l θ^{'}$ where $θ^{'}$ contain only substitutions of variables of l by sub contexts of $C [_]$ and subterms of $T_{1}, \dots, T_{n}$ . Thus, we have: $\begin{matrix} C [T_{1}, \dots, T_{n}] |_{s} =_{A C} l θ \to r θ^{'} =_{A C} C_{r} [R_{1}, \dots, R_{q_{r}}] \end{matrix}$ where $C_{r} [_]$ contains r and all subcontexts $C_{x} [_]$ , $C_{x}^{k} [_]$ . Since $f \notin C$ and $C_{x} [_]$ , $C_{x}^{k} [_]$ are subcontexts of $C [_]$ , we know that $f \notin C_{x}$ and $f \notin C_{x}^{k}$ . Moreover, since f is a destructor in E, $f \notin r$ . Thus, $f \notin C_{r}$ . Finally, $R_{1}, \dots, R_{q_{r}}$ are subterms of $T_{1}, \dots, T_{n}$ , then: $\begin{matrix} C [T_{1}, \dots, T_{n}] \to C [T_{1}, \dots, T_{n}] {[C_{r} [R_{1}, \dots, R_{q_{r}}]]}_{p} = C^{'} [M_{1}, \dots, M_{q}] . \end{matrix}$ □

If a destructor term t is non deducible and does not appear as subterm of a frame then t cannot appear as subterm of any deducible term.
Lemma 5.
Let E be an equational theory induced by an AC convergent rewriting system $R$ , Σ a signature and $f \in Σ$ is a destructor in E. Let φ be a frame and $U = f (U_{1}, \dots, U_{n})$ a term in normal form such that $U \notin St (φ)$ and $φ ⊬ U$ . Then: $\begin{matrix} for all term T in normal form such that φ ⊢ T, U \notin St (T) . \end{matrix}$
Proof.
Let us prove this by induction on the number of steps used to deduce T.

Base case: $T \in φ$ . Then, since $U \notin St (φ)$ , we have that $U \notin St (T)$ .

Induction case: Now suppose that for any T in normal form such that $φ ⊢ T$ in n steps, then $U \notin St (T)$ . Let T in normal form such that $φ ⊢ T$ in $n + 1$ steps. We have $φ ⊢ T =_{A C} g (T_{1}, \dots, T_{n}) ↓$ where $g \in Σ$ and $φ ⊢ T_{i}$ in n steps with $T_{i}$ in normal form for $i \in ⟦ 1, n ⟧$ .
If $g (T_{1}, \dots, T_{n})$ is already in normal form, then we have two subcases:

If $g \neq f$ , then according to the induction hypothesis and since $U \notin St (T_{i})$ , we have $U \notin St (T)$ .

If $g = f$ , then, if $U \in St (T)$ and since $U \notin St (T_{i})$ according to the induction hypothesis, we must have $T = U$ , which yields to a contradiction since $φ ⊢ T$ and $φ ⊬ U$ .

If $g (T_{1}, \dots, T_{n})$ is not in normal form. If $g = f$ then, we have that $f (T_{1}, \dots, T_{n}) \to r [{\tilde{T}}_{i}]$ for some rule $l \to r$ . Since f is a destructor in E, we know that $f \notin r$ . Thus, according to Lemma 4, we know that $r [{\tilde{T}}_{i}] \to^{} C [{\tilde{T}}_{i}]$ such that $f \notin C$ . In that case, if $U \in St (C [{\tilde{T}}_{i}])$ , then, we must have $U \in St ({\tilde{T}}_{i})$ which is a contradiction. If $g \neq f$ , then, using Lemma 4 with $C [T_{1}, \dots, T_{n}] =_{A C} g (T_{1}, \dots, T_{n})$ , we have that $\exists C^{'}$ such that $f \notin C^{'}$ and $g (T_{1}, \dots, T_{n}) \to^{} C^{'} [{\tilde{T}}_{i}]$ with ${\tilde{T}}_{i}$ subterms of $T_{1}, \dots, T_{n}$ . Then $T =_{A C} C^{'} [{\tilde{T}}_{i}]$ but we know that $U \notin St ({\tilde{T}}_{i})$ according to induction hypothesis, thus $U \notin St (T)$ .
This concludes the induction. □

A context in normal form applied to a destructor term remains in normal form.
Lemma 6.
Let E be an equational theory induced by an AC convergent rewriting system $R$ , Σ a signature and $f \in Σ$ is a destructor in E. Let $U = f (U_{1}, \dots, U_{n})$ a term in normal form and $P {[X]}_{p}$ another term in normal form. Then $P {[U]}_{p}$ is also in normal form.
Proof.
Assume that $P [U]$ is not in normal form. Since $P [X]$ and U are in normal form, it implies that $\exists p$ a position of $P [_]$ such that $P [U] |_{p} =_{A C} l θ$ with some rule $l \to r$ and some substitution θ. But f is a destructor in E, thus, f must appear at the head of l, which is a contradiction with the position p. □

As a consequence of the previous lemmas, we can state that adding non deducible destructor terms to the frames preserve static equivalence. Lemma 7.
Let E be an equational theory, Σ a signature and $f, g \in Σ$ destructors in E. Let $φ_{1} = ν {\tilde{ω}}_{1} . θ_{1}$ and $φ_{2} = ν {\tilde{ω}}_{2} . θ_{2}$ be frames. Let $U_{1} = f (U_{1}^{1}, \dots, U_{p}^{1})$ and $U_{2} = g (U_{1}^{2}, \dots, U_{q}^{2})$ be terms in normal form such that, $\forall i \in {1, 2}$ , $φ_{i} ⊬ U_{i}$ and $U_{i} \notin St (φ_{i})$ . Then: $\begin{matrix} φ_{1} \approx_{s} φ_{2} ⟺ ν {\tilde{ω}}_{1} . (θ_{1} ∣ {^{U_{1}} /_{x}}) \approx_{s} ν {\tilde{ω}}_{2} . (θ_{2} ∣ {^{U_{2}} /_{x}}) . \end{matrix}$
Proof.
Let $φ_{i}^{'} = ν {\tilde{ω}}_{i} . (θ_{i} ∣ {^{U_{i}} /_{x}}) = ν {\tilde{ω}}_{i} . θ_{i}^{'}$ for $i \in {1, 2}$ .

$⟸ ∣$ Straightforward.

$⟹ ∣$ Let M and N be terms s.t. $fv (M, N) \subseteq dom (φ_{1}^{'})$ and $bn (M, N) \cap bn (φ_{1}^{'}) = \emptyset$ with $(M =_{E} N) φ_{1}^{'}$ . Then: $\begin{matrix} \begin{matrix} M φ_{1}^{'} & =_{E} & N φ_{1}^{'} \\ (M φ_{1}^{'}) ↓ & =_{A C} & (N φ_{1}^{'}) ↓ \\ (M φ_{1} δ_{1}) ↓ & =_{A C} & (N φ_{1} δ) ↓ \end{matrix} \end{matrix}$ with $δ_{1} : x \mapsto U_{1}$ , according to $φ_{1}^{'}$ definition. Since $U_{1}$ is in normal form, we apply Lemma 6: $\begin{matrix} \begin{matrix} (M φ_{1}) ↓ δ_{1} & =_{A C} & (N φ_{1}) ↓ δ_{1} \\ ((M φ_{1}) ↓ δ_{1}) δ_{1}^{- 1} & =_{A C} & ((N φ_{1}) ↓ δ_{1}) δ_{1}^{- 1} \end{matrix} \end{matrix}$ with $δ_{1}^{- 1} : U_{1} \mapsto x$ . We know that $U_{1} = f (U_{1}^{1}, \dots, U_{p}^{1})$ with f destructor in E and $U_{1}$ in normal form and not subterm of $φ_{1}$ . Thus, using Lemma 5, for any T in normal form s.t. $φ_{1} ⊢ T$ , then $U_{1} \notin St (T)$ . And, since $φ_{1} ⊢ (M φ_{1}) ↓$ (resp. $(N φ_{1}) ↓$ ) we have that $(M φ_{1}) ↓ δ_{1}^{- 1} = (M φ_{1}) ↓$ (resp. $(N φ_{1}) ↓ δ_{1}^{- 1} = (N φ_{1}) ↓$ ). Thus: $\begin{matrix} \begin{matrix} (M φ_{1}) ↓ δ_{1} δ_{1}^{- 1} & =_{A C} & (N φ_{1}) ↓ δ_{1} δ_{1}^{- 1} \\ (M φ_{1}) ↓ & =_{A C} & (N φ_{1}) ↓ \end{matrix} \end{matrix}$ Since $φ_{1} \approx_{s} φ_{2}$ , we have (with $δ_{2} : x \mapsto U_{2}$ ): $\begin{matrix} \begin{matrix} (M φ_{2}) ↓ & =_{A C} & (N φ_{2}) ↓ \\ (M φ_{2}) ↓ δ_{2} & =_{A C} & (N φ_{2}) ↓ δ_{2} \end{matrix} \end{matrix}$ Using Lemma 6, we deduce $(M φ_{2}) ↓ δ_{2} =_{A C} (N φ_{2}) ↓$ , implying that $(M =_{E} N) φ_{1}^{'} \to (M =_{E} N) φ_{2}^{'}$ . Repeating the same reasoning, we can also prove that $(M =_{E} N) φ_{2}^{'} \to (M =_{E} N) φ_{1}^{'}$ , and we conclude. □

5.2. A more specific lemma

We show that adding the signature of a deducible term preserves static equivalence, when the same recipe is used in both frames. We believe that this lemma holds for other primitives provided the equations are similar to those for the “ $sign$ symbol like the case of zero-knowledge proofs.

Lemma 8.
Let $φ_{1} = ν ω_{1} . θ_{1}$ and $φ_{2} = ν ω_{2} . θ_{2}$ be two frames, x a fresh variable and a, a name such that $a \in ω_{1} \cap ω_{2}$ , ${^{vk (a)} /_{id p_{a}}} \in θ_{1} \cap θ_{2}$ and $φ_{1}, φ_{2} ⊬ a$ . Let $U = sign (U^{'}, a)$ in normal form with $U^{'}$ a free term and such that $(U φ_{i}) ↓ \notin St (φ_{i})$ . Then: $\begin{matrix} φ_{1} \approx_{s} φ_{2} ⟺ ν ω_{1} . (θ_{1} ∣ {^{(U φ_{1}) ↓} /_{x}}) \approx_{s} ν ω_{2} . (θ_{2} ∣ {^{(U φ_{2}) ↓} /_{x}}) . \end{matrix}$

Before proving this lemma, we introduce the notion of down-to-top strategy, where a rewrite rule is applied first as deep as possible. Note that since we consider convergent rewrite systems, we may chose any rewrite strategy. Definition 6.
Let us consider $M_{0} \overset{l_{1} \to r_{1}}{\to} M_{1} ⟶ \dots \overset{l_{i} \to r_{i}}{\to} M_{i} \dots ⟶ M_{n} = M_{0} ↓$ a reduction strategy. This strategy is called down-to-top, noted $⟶_{d t}$ , if, for all $i \in ⟦ 1, n ⟧$ , $M_{i - 1} |_{p_{i}} =_{A C} l_{i} θ_{i} \to r_{i} θ_{i}$ and for all position $q < p_{i}$ , $M_{i - 1} |_{q}$ is in normal form.
Proof.
Let ${\overline{φ}}_{i} = ν ω_{1} . {\overline{θ}}_{i}$ with ${\overline{θ}}_{i} = θ_{i} ∣ {^{(U φ_{i}) ↓} /_{x}}$ for $i \in {1, 2}$ .

$⟸ ∣$ Straightforward.

$⟹ ∣$ We first assume the two following claims that we prove next. Claim 1.
Let M be a term s.t. $fn (M) \cap ω_{i} = \emptyset$ . Then, for any term T s.t. $M φ_{i} ⟶_{d t}^{} T$ , we have* $(U φ_{i}) ↓ \notin St (T)$ .
Claim 2.
Let M be a term s.t. $(U φ_{i}) ↓ \notin St (M)$ and for all term T s.t. $M ⟶_{d t}^{} T$ , then* $(U φ_{i}) ↓ \notin St (T)$ . Let $σ = {^{(U φ_{i}) ↓} /_{x}}$ a substitution. If $M σ ⟶_{d t}^{} T$ with no rule (8) involved in the reduction path, then there exists some term* $T^{'}$ such that $M ⟶_{d t}^{} T^{'}$ and* $T^{'} σ =_{A C} T$ .

We now suppose that $φ_{1} \approx_{s} φ_{2}$ and we consider M and N two terms s.t. $fv (M, N) \subseteq dom ({\overline{φ}}_{1})$ and $fn (M, N) \cap ω_{1} = \emptyset$ . (Since $φ_{1} \approx_{s} φ_{2}$ , we have $ω_{1} = ω_{2}$ and $dom ({\overline{φ}}_{1}) = dom ({\overline{φ}}_{2})$ .) We are going to prove that $(M =_{E} N) {\overline{φ}}_{1}$ iff $(M =_{E} N) {\overline{φ}}_{2}$ by induction on the number of positions p in M and N s.t. $M |_{p} = checksign (M_{1}, M_{2}, M_{3})$ and $(M |_{p} {\overline{φ}}_{i}) ↓ =_{E} ok$ for $i = 1$ or $i = 2$ . We also assume down-to-top reduction strategies only (noted $⟶_{d t}$ ).

Base case: There is no such position in M and N. Then, we can apply Claim 2 on $M {\overline{φ}}_{i}$ and $N {\overline{φ}}_{i}$ . Indeed, let $σ_{i} = {^{(U φ_{i}) ↓} /_{x}}$ . For $P \in {M, N}$ , then $P {\overline{φ}}_{i} = (P φ_{i}) σ_{i} ⟶_{d t}^{} (P {\overline{φ}}_{i}) ↓$ . If there exists a position p such that $(P φ_{i}) |_{p} =_{A C} (U φ_{i}) ↓$ then, according to the hypothesis on $φ_{i}$ , p must be a position of P (and not at a leaf). This implies that $P |_{p 2} = a$ which would be a contradiction with the fact that a is restricted. Thus, we have $(U φ_{i}) ↓ \notin St (P φ_{i})$ . We also have $P φ_{i} ⟶_{d t}^{} (P φ_{i}) ↓$ and s.t. $fn (P) \cap ω_{i} = \emptyset$ . Using Claim 1, we deduce that $(U φ_{i}) ↓$ does not occur in any of the terms in the reduction $P φ_{i} ⟶_{d t}^{} (P φ_{i}) ↓$ . Applying Claim 2 leads to $(P {\overline{φ}}_{i}) ↓ =_{A C} (P φ_{i}) ↓ σ_{i}$ . Then: $\begin{matrix} \begin{matrix} (M {\overline{φ}}_{i}) ↓ & =_{A C} & (N {\overline{φ}}_{i}) ↓ \\ (M φ_{1}) ↓ σ_{1} & =_{A C} & (N φ_{1}) ↓ σ_{1} (Claim 2) \\ (M φ_{1}) ↓ & =_{A C} & (N φ_{1}) ↓ (Claim 1) \end{matrix} \begin{matrix} (M φ_{2}) ↓ & =_{A C} & (N φ_{2}) ↓ (φ_{1} \approx_{s} φ_{2}) \\ (M φ_{2}) ↓ σ_{2} & =_{A C} & (N φ_{2}) ↓ σ_{2} \\ (M {\overline{φ}}_{2}) ↓ & =_{A C} & (N {\overline{φ}}_{2}) ↓ . (Claim 2) \end{matrix} \end{matrix}$

Induction step: We suppose that there exists at least one position p in M or N s.t. $M |_{p} = checksign (M_{1}, M_{2}, M_{3})$ (or $N |_{p}$ ) and $(M |_{p} {\overline{φ}}_{i}) ↓ =_{E} ok$ (resp. $N |_{p}$ ) for $i = 1$ or $i = 2$ . Let us consider w.l.o.g. that this position is in M and that it reduces when ${\overline{φ}}_{1}$ is applied. (We note that if $(M |_{p} {\overline{φ}}_{2}) ↓ =_{E} ok$ too then we have $(M {[ok]}_{p} =_{E} M) {\overline{φ}}_{i}$ for $i \in {1, 2}$ and we can conclude using the induction hypothesis on $M {[ok]}_{p}$ and N.) We consider the deepest position satisfying this in M. Thus, we know that $M_{1}$ , $M_{2}$ and $M_{3}$ do not contain such a position.

Since $(M |_{p} {\overline{φ}}_{1}) ↓ =_{E} ok$ , then, according to E, we have that $(M_{3} {\overline{φ}}_{1}) ↓ =_{A C} sign ((M_{1} {\overline{φ}}_{1}) ↓, Q)$ and $(M_{2} {\overline{φ}}_{1}) ↓ =_{A C} vk (Q)$ for some term Q. According to the hypothesis on position p, we can apply the same reasoning as used in the base case on $M_{1}$ , $M_{2}$ and $M_{3}$ separately and therefore we can apply Claim 2 on them, which leads to $(M_{i} {\overline{φ}}_{1}) ↓ =_{A C} (M_{i} φ_{1}) ↓ σ_{1}$ for $i \in {1, 2, 3}$ . We have then the following equalities:
$(M_{1} φ_{1}) ↓ =_{A C} T_{1}$ and $T_{1} σ_{1} =_{A C} (M_{1} {\overline{φ}}_{1}) ↓$ .

$(M_{2} φ_{1}) ↓ =_{A C} T_{2}$ and $T_{2} σ_{1} =_{A C} vk (Q)$ . According to definition of $σ_{1}$ , which does not contain a term of this form, we must have $T_{2} =_{A C} vk (T_{2}^{'})$ and $T_{2}^{'} σ_{2} =_{A C} Q$ .

$(M_{3} φ_{1}) ↓ =_{A C} T_{3}$ and $T_{3} σ_{1} =_{A C} sign ((M_{1} {\overline{φ}}_{1}) ↓, Q)$ . Using the two previous equalities, we have $T_{3} σ_{1} =_{A C} sign (T_{1} σ_{1}, T_{2}^{'} σ_{1})$ . Then, according to the definition of $σ_{1}$ , we consider two subcases:

$T_{3} =_{A C} sign (T_{1}, T_{2}^{'},)$ and then, we have: $\begin{array}{l} (M |_{p} φ_{1}) ↓ & =_{E} checksign ((M_{1} φ_{1}) ↓, (M_{2} φ_{1}) ↓, (M_{3} φ_{1}) ↓) ↓ \\ =_{E} checksign (T_{1}, vk (T_{2}^{'}), sign (T_{1}, T_{2}^{'})) ↓ \\ =_{E} ok . \end{array}$ Thus, $(M |_{p} =_{E} ok) φ_{1}$ and using $φ_{1} \approx_{s} φ_{2}$ , we have $(M |_{p} =_{E} ok) φ_{2}$ which also implies by extension $(M |_{p} =_{E} ok) {\overline{φ}}_{2}$ and we conclude.

$T_{3} = x$ . Then, we have $T_{2} σ_{1} =_{A C} vk (a)$ , i.e. $T_{2} =_{A C} vk (a)$ , which is $(M_{2} φ_{1}) ↓ =_{A C} vk (a)$ . Thus, we have $(M_{2} =_{E} id p_{a}) φ_{1}$ and, using $φ_{1} \approx_{s} φ_{2}$ that leads us to $(M_{2} =_{E} id p_{a}) {\overline{φ}}_{2}$ . Moreover, $(M_{1} {\overline{φ}}_{1}) ↓ =_{A C} T_{1} σ_{1} =_{A C} (U^{'} φ_{1}) ↓$ , i.e. $T_{1} =_{A C} (U^{'} φ_{1}) ↓$ according to the definition of $σ_{1}$ , which implies $(M_{1} φ_{1}) ↓ =_{A C} (U^{'} φ_{1}) ↓$ . Using $φ_{1} \approx_{s} φ_{2}$ again, we have $(M_{1} =_{E} U^{'}) {\overline{φ}}_{2}$ . Then: $\begin{array}{l} (M |_{p} {\overline{φ}}_{2}) ↓ & =_{E} checksign ((M_{1} {\overline{φ}}_{2}) ↓, (M_{2} {\overline{φ}}_{2}) ↓, (x {\overline{φ}}_{2}) ↓) ↓ \\ =_{E} checksign ((U^{'} φ_{2}) ↓, (id p_{a} φ_{2}) ↓, (U φ_{2}) ↓) ↓ \\ =_{E} ok . \end{array}$ And we conclude.

We now prove that the two claims hold.

Proof of Claim 1 We prove this Claim by induction on the size of M. We suppose w.l.o.g. that M is in normal form.

Base case: $M = y$ is a variable (or a name). Since $φ_{i}$ is in normal form, we have that for all T s.t. $M φ_{i} ⟶_{d t}^{} T$ then $M φ_{i} =_{A C} T$ . If M is a name, result is straightforward. If M is a variable, then $(U φ_{i}) ↓ \in St (T)$ implies that $(U φ_{i}) ↓ \in St (φ_{i})$ which is a contradiction.

Induction Step: We assume that for any term M of size m s.t. $fn (M) \cap ω_{i} = \emptyset$ we have, for all term T s.t. $M φ_{i} ⟶_{d t}^{} T$ , $(U φ_{i}) ↓ \notin St (T)$ . We now consider a term M of size $(m + 1)$ , i.e. $M = f (M_{1}, \dots, M_{n})$ with $M_{i}$ of size at most equal to m. Moreover, following a down-to-top reduction strategy, we have $M φ_{i} = f (M_{1} φ_{i}, \dots, M_{n} φ_{i}) ⟶_{d t}^{} f (T_{1}, \dots, T_{n})$ with $T_{j} = (M_{j} φ_{i}) ↓$ . According to the induction hypothesis, we now that for all term T s.t. $M_{j} φ_{i} ⟶_{d t}^{} T$ , then $(U φ_{i}) ↓ \notin St (T)$ . Let us consider now the down-to-top reduction strategy $M φ_{i} ⟶_{d t}^{} T = f (T_{1}^{'}, \dots, T_{n}^{'}) ⟶_{d t}^{} f (T_{1}, \dots, T_{n})$ . If $(U φ_{i}) ↓ \in St (T)$ , then we have two possibilities. Either $(U φ_{i}) ↓ \in St (T_{k}^{'})$ for some $k \in ⟦ 1, n ⟧$ and we have a contradiction with the induction hypothesis; or $f (T_{1}^{'}, \dots, T_{n}^{'}) =_{A C} (U φ_{i}) ↓$ and $f = sign$ , $n = 2$ and $T_{2}^{'} = a$ which implies that $a$ is deducible by $φ_{i}$ , contradiction. Thus, $(U φ_{i}) ↓$ does not occur in any of the terms in the reduction $(M φ_{i}) ↓ ⟶_{d t}^{} f (T_{1}, \dots, T_{n})$ . We now consider the reduction of $f (T_{1}, \dots, T_{n})$ :
It is in normal form, then, we have two subcases:

$f \neq sign$ . Then, since $(U φ_{i}) ↓ \notin St (T_{j})$ for $j \in ⟦ 1, n ⟧$ by the induction hypothesis, we conclude.

$f = sign$ . Using the induction hypothesis, if $(U φ_{i}) ↓ \in St (sign (T_{1}, T_{2}))$ , we must have $sign (T_{1}, T_{2}) =_{A C} (U φ_{i}) ↓$ and $a$ would be deducible by $φ_{i}$ which is a contradiction.

$f (T_{1}, \dots, T_{n})$ is not in normal form. Then, we have $f \neq sign$ since there are no rule in E s.t. $sign$ is in head. We have $f (T_{1}, \dots, T_{n}) ⟶_{d t} T$ and we consider two subcases:

$T \in St (T_{1}, \dots, T_{n})$ , then T is in normal form and, using the induction hypothesis, we know that $(U φ_{i}) ↓ \notin St (T)$ and we conclude.

$T \notin St (T_{1}, \dots, T_{n})$ , then, according to E, we have used rule (4), (5), (6) or (8), (9), (10). The three last rules lead to $T = ok$ which concludes straightforwardly and the three first rules lead to T in normal form with the property that if $(U φ_{i}) ↓ \in St (T)$ , then $(U φ_{i}) ↓ \in \cup St (T_{k})$ , which would be a contradiction.

Proof of Claim* 2 Let us prove this by induction on the number of reduction steps in $M σ ⟶_{d t}^{} T$ .

Base case: If $M σ =_{A C} T$ , the result is straightforward. If $M σ ⟶_{d t} T$ in one step, then, there is a position p, a substitution θ and a rule $l ⟶ r$ (different from (8)) s.t. $(M σ) |_{p} =_{A C} l θ ⟶_{d t} r θ$ . Since σ is in normal form, p must be a position of M. In particular, if we consider $M^{'} = M {[z]}_{p}$ , we have: $\begin{matrix} M σ =_{A C} (M {[z]}_{p} σ) {[l θ]}_{p} =_{A C} (M^{'} σ) {[l θ]}_{p} and M σ ⟶_{d t} (M^{'} σ) {[r θ]}_{p} . \end{matrix}$ We note $δ : (U φ_{i}) ↓ \mapsto x$ . Then, we have $(M σ) δ =_{A C} ((M^{'} σ) {[l θ]}_{p}) δ$ . Hypothesis on M states that there is no position q such that $M |_{q} =_{A C} (U φ_{i}) ↓$ . Therefore, there is no position q such that $M^{'} |_{q} =_{A C} (U φ_{i}) ↓$ and the following equalities hold: $(M σ) δ =_{A C} M (σ δ) =_{A C} M$ and $(M^{'} σ) δ =_{A C} M^{'} (σ δ) =_{A C} M^{'}$ . Moreover, we know that $(l θ) \notin St ((U φ_{i}) ↓)$ otherwise $(U φ_{i}) ↓$ would not be in normal form. Thus, $M =_{A C} M^{'} {[(l θ) δ]}_{p}$ . Since $l ⟶ r$ is different from rule (8), we have $(l θ) δ = l (θ δ) = l θ^{'} ⟶ r θ^{'}$ , for $θ^{'} = θ δ$ , and this implies $M ⟶_{d t} M^{'} {[r θ^{'}]}_{p}$ following a down-to-top reduction strategy since if there was a lower reduction in M it would also exists in $M σ$ . Now, we can conclude since: $\begin{array}{l} (M^{'} {[r θ^{'}]}_{p}) σ & =_{A C} (M^{'} σ) {[(r θ^{'}) σ]}_{p} \\ =_{A C} (M^{'} σ) {[r (θ^{'} σ)]}_{p} \\ =_{A C} (M^{'} σ) {[r θ]}_{p} . \end{array}$

Induction Step: We suppose that, for any term M s.t. for all term T s.t. $M ⟶_{d t}^{} T$ , then $(U φ_{i}) ↓ \notin St (T)$ , we have: if $M σ ⟶_{d t}^{m} T$ in m steps involving no (8) rule, then $M ⟶_{d t}^{m} T^{'}$ with $T^{'} σ =_{A C} T$ . We consider now M s.t. $M σ ⟶_{d t}^{m + 1} T$ in $(m + 1)$ steps with no rules (8) in the reduction path. Then $M σ ⟶_{d t}^{m} M_{1} ⟶_{d t} T$ . Using the induction hypothesis, we have that $M ⟶_{d t}^{m} M_{1}^{'}$ with $M_{1}^{'} σ =_{A C} M_{1}$ , thus $M_{1}^{'} σ ⟶_{d t} T$ . But $M^{'}$ is verifying hypothesis of Claim 2, otherwise we would have a contradiction with the fact that M is satisfying them. Then, using Base Case, we have $M_{1}^{'} ⟶_{d t} T^{'}$ with $T^{'} σ =_{A C} T$ . Thus, $M ⟶_{d t}^{m} M_{1}^{'} ⟶_{d t} T^{'}$ and $T^{'} σ =_{A C} T$ , which allows us to conclude. □

6. Static equivalence of the final frame

This section is devoted to the proof of Proposition 1, that states static equivalence of the final frame obtained in the relation $R$ . This proof relies on several lemmas. Some of them have been presented in the previous section, other are stated here and proved in appendix.

6.1. Definitions and useful lemmas

We first start by introducing some notations that will be useful for the following lemmas. Some of these definitions may seem artificial but mainly come from the establishment of the relation $R$ , which is described in the Appendix Section F.

Definition 7.
We introduce (or remind) the following definitions: $\begin{array}{l} \tilde{ω} = a_{1}, a_{3}, i d_{1}, i d_{2}, t_{1}, t_{2}, i d_{R}, \\ θ_{init} = {^{vk (i d_{k})} /_{id p_{k}},^{s (i d_{k})} /_{s_{k}} ∣ k = 1, \dots, n} ∣ {^{vk (i d_{R})} /_{id p_{R}}} ∣ {^{pk (a_{k})} /_{g_{k}} ∣ k = 1 \dots, 3}, \\ θ_{0} = θ_{init} ∣ {^{penc (v_{k}, r_{k}, g_{1})} /_{e_{k}},^{{pfk}_{1} (i d_{k}, t_{k}, v_{k}, e_{k})} /_{p_{k}},^{sign (⟨ e_{k}, p_{k} ⟩, i d_{k})} /_{s i_{k}} ∣ k = 1, 2}, \\ θ_{k} = θ_{k - 1} ∣ {^{sign (hash (Π_{1} (M_{k})), i d_{R})} /_{{sr}_{k}},^{d (p (i d_{k}), dec (Π_{2} (M_{k}), a_{3}))} /_{{rec}_{k}}}, \\ θ_{δ} = θ_{n} ∣ {^{dec (U_{δ (k)}, a_{1})} /_{{res}_{k}} ∣ k = 1, \dots, n}, \\ σ_{L} = {^{a} /_{v_{1}},^{b} /_{v_{2}}}, σ_{R} = {^{b} /_{v_{1}},^{a} /_{v_{2}}}, \\ \hat{σ} = {^{M_{k} α} /_{x_{k}},^{U_{k} α} /_{d_{k}},^{W_{k} α} /_{{hb}_{k}} ∣ k = 1, \dots, n} ∣ {^{N_{k} α} /_{x_{b}^{k}} ∣ k = 1, \dots, 2}, \\ {\hat{σ}}_{i}^{j} = {^{M_{k} α} /_{x_{k}} ∣ k = 1, \dots, i} ∣ {^{N_{k} α} /_{x_{b}^{k}} ∣ k = 1, \dots, \min (i, 2)} ∣ {^{U_{k} α} /_{d_{k}},^{W_{k} α} /_{{hb}_{k}} ∣ k = 1, \dots, j} . \end{array}$ where α is a substitution representing the intermediate outputs visible by an adversary controlling the corrupted Ballot Box (full definition given in Section A), and $M_{k}$ , $N_{k}$ , $U_{k}$ , $W_{k}$ are free terms satisfying some conditions defined in Section F. They represent the inputs submitted by the adversary during the different steps of the protocol.

The first lemma ensures that several secret datas (like encryption/decryption keys, voters’ secret IDs, etc.) remain secret during the execution of the protocol.
Lemma 9.
For $i \in {1, 2}$ , $j \in {1, 2, 3}$ and any free term U, if M is of one of the following forms: $a_{j} + U$ , $t_{i} * U$ , $i d_{i}$ or $p (i d_{i})$ , then $ν \tilde{ω} . θ_{δ} ⊬ M$ , i.e. M is not deducible from the frame $ν \tilde{ω} . θ_{δ}$ .

We then prove that the different outputs of the (honest) Receipt Generator, that is, a signature and a receipt for each submitted ballot, do not bring any relevant information to the adversary that could help him to make a difference between two different executions of the protocol. This property is expressed by the fact that we can add these terms to the frame without breaking the static equivalence.
Lemma 10.
For $i \in ⟦ 0, n ⟧$ , we have: $ν \tilde{ω} . θ_{i} {\hat{σ}}_{i}^{0} σ_{L} \approx_{s} ν \tilde{ω} . θ_{i} {\hat{σ}}_{i}^{0} σ_{R}$ .

Finally, we show that we can control the form of what is sent to the Decryption Device, assuming it is approved by the Auditor. Lemma 11.
Let us consider $M_{1}, \dots, M_{n}$ free terms s.t. $\forall i \in ⟦ 1, n ⟧$ , $ϕ_{R} (id p_{i + 1}, M_{i + 1}) θ_{i} {\hat{σ}}_{i}^{0} σ_{L} = ok$ with $fv (M_{i + 1}) \subseteq dom (θ_{i}) \cup dom ({\hat{σ}}_{i}^{0}) ∖ {x_{b}^{i}}$ . We suppose that $\forall i \in ⟦ 1, n ⟧$ , $ν \tilde{ω} . θ_{i} {\hat{σ}}_{i}^{0} σ_{L} \approx_{s} ν \tilde{ω} . θ_{i} {\hat{σ}}_{i}^{0} σ_{R}$ . We also consider $U_{1}, \dots, U_{n}$ and $W_{1}, \dots, W_{n}$ be free terms such that:
$fv (U_{k + 1}) \subseteq dom (θ_{n}) \cup {dom ({\hat{σ}}_{n}^{0})} \cup {d_{1}, \dots, d_{k}}$ and $fv (W_{k + 1}) \subseteq dom (θ_{n}) \cup {dom ({\hat{σ}}_{n}^{k})}$ ,

$ϕ_{A} (hash (⟨ U_{1}, \dots, U_{n} ⟩), {hb}_{r}^{1}, \dots, {hb}_{r}^{n}, W_{1}, \dots, W_{n}) θ_{n} \hat{σ} σ_{L} = ok$ , with the corresponding notation ${hb}_{r}^{i} = ⟨ id p_{i}, hash (Π_{1} (M_{i})) ⟩$ .
Then, we have, for $σ \in {σ_{L}, σ_{R}}$ , $\forall 1 ⩽ i ⩽ n$ : $\begin{matrix} U_{i} θ_{n} \hat{σ} σ =_{E} e_{i} θ_{n} \hat{σ} σ, for i = 1, 2 . \end{matrix}$ Moreover, there exist free terms $U_{1}^{'}$ , $U_{2}^{'}$ and free term $U_{3}^{'}$ or $U_{3}^{'} = pk (a_{k} + U)$ with free term U: $\begin{matrix} U_{i} θ_{n} \hat{σ} σ =_{E} penc (U_{1}^{'}, U_{2}^{'}, U_{3}^{'}) θ_{n} \hat{σ} σ, for i \in ⟦ 3, n ⟧ . \end{matrix}$

6.2. Proving Proposition 1

With all these lemmas, we can now prove the final static equivalence, which is stated in Proposition 1.

Proof.
We introduce the notation ${\hat{θ}}_{i}^{δ} = θ_{n} ∣ {^{{dec}_{δ (k)}} /_{{res}_{k}} ∣ k \in ⟦ 1, i ⟧}$ with ${dec}_{δ (i + 1)} = dec (d_{δ (i + 1)}, a_{1})$ . We show by induction that: $\begin{matrix} ν \tilde{ω} . {\hat{θ}}_{i}^{δ} \hat{σ} σ_{L} \approx_{s} ν \tilde{ω} . {\hat{θ}}_{i}^{^{t} δ} \hat{σ} σ_{R} . \end{matrix}$

Base case. The base case is ensured by Lemma 10 which guarantees that $ν \tilde{ω} . θ_{n} {\hat{σ}}_{n}^{0} σ_{L} \approx_{s} ν \tilde{ω} . θ_{n} {\hat{σ}}_{n}^{0} σ_{R}$ thus, by rewriting, we have $ν \tilde{ω} . {\hat{θ}}_{0}^{δ} \hat{σ} σ_{L} \approx_{s} ν \tilde{ω} . {\hat{θ}}_{0}^{^{t} δ} \hat{σ} σ_{R}$ .

Induction step. Suppose that $ν \tilde{ω} . {\hat{θ}}_{i}^{δ} \hat{σ} σ_{L} \approx_{s} ν \tilde{ω} . {\hat{θ}}_{i}^{^{t} δ} \hat{σ} σ_{R}$ for some $i ⩾ 0$ . Let us show that: $\begin{matrix} ν \tilde{ω} . {\hat{θ}}_{i + 1}^{δ} \hat{σ} σ_{L} \approx_{s} ν \tilde{ω} . {\hat{θ}}_{i + 1}^{^{t} δ} \hat{σ} σ_{R} . \end{matrix}$ We have that ${dec}_{δ (i + 1)} = dec (U_{δ (i + 1)}, a_{1})$ in the frame ${\hat{θ}}_{i + 1}^{δ} \hat{σ}$ . We distinguish cases according to the value of $δ (i + 1)$ :
If $δ (i + 1) = 1$ , then, using Lemma 11 (since we are considering the decryption step of the protocol, $ϕ_{A}$ must have been successful), we know that $U_{k} θ_{n} \hat{σ} σ = e_{k} θ_{n} \hat{σ} σ$ for $k \in {1, 2}$ and any $σ \in {σ_{L}, σ_{R}}$ . Thus, we have that ${res}_{i + 1} {\hat{θ}}_{i + 1}^{δ} \hat{σ} σ_{L} =_{E} dec (U_{1}, a_{1}) {\hat{θ}}_{i + 1}^{δ} \hat{σ} σ_{L} =_{E} v_{1} σ_{L}$ . But, we also have the following equalities ${res}_{i + 1} {\hat{θ}}_{i + 1}^{^{t} δ} \hat{σ} σ_{R} =_{E} dec (U_{2}, a_{1}) {\hat{θ}}_{i + 1}^{^{t} δ} \hat{σ} σ_{R} =_{E} v_{2} σ_{R}$ . According to the definition of $σ_{L}$ and $σ_{R}$ , we have $v_{1} σ_{L} =_{E} v_{2} σ_{R} =_{E} a$ . Then, using the induction hypothesis and Lemma 3 with the free term $U = a$ and we conclude.

If $δ (i + 1) = 2$ , we adopt the same argument used in the previous case (replacing 1 by 2 and 2 by 1) and conclude using the induction hypothesis and Lemma 3 with the free term $U = b$ .

If $δ (i + 1) = j \in ⟦ 3, n ⟧$ , then $^{t} δ (i + 1) = δ (i + 1)$ and we have ${res}_{i + 1} = dec (U_{j}, a_{1})$ . According to Lemma 11, we have that $U_{j} θ_{n} \hat{σ} σ = penc (N, P, Q) θ_{n} \hat{σ} σ$ for free terms N, P, Q and any $σ \in {σ_{L}, σ_{R}}$ . Thus, ${res}_{i + 1} {\hat{θ}}_{i + 1}^{δ} \hat{σ} σ_{L} =_{E} dec (penc (N, P, Q), a_{1}) θ_{n} \hat{σ} σ_{L}$ . We consider two subcases:

$Q θ_{n} \hat{σ} σ_{L} =_{E} pk (a_{1})$ . Then, ${res}_{i + 1} {\hat{θ}}_{i + 1}^{δ} \hat{σ} σ_{L} =_{E} N {\hat{θ}}_{i + 1}^{δ} \hat{σ} σ_{L}$ with free N. And, in that case, we also have $Q θ_{n} \hat{σ} σ_{R} =_{E} pk (a_{1})$ (using the induction hypothesis and the fact that $g_{1} = pk (a_{1})$ ) and ${res}_{i + 1} {\hat{θ}}_{i + 1}^{^{t} δ} \hat{σ} σ_{R} =_{E} N {\hat{θ}}_{i + 1}^{^{t} δ} \hat{σ} σ_{R}$ too. Thus, we conclude using Lemma 3.

Fig. 7.
Equational theory $E^{'}$ used in ProVerif.

$Q θ_{n} \hat{σ} σ_{L} \neq_{E} pk (a_{1})$ . Then, there is no reduction of ${res}_{i + 1}$ (in both frames) and we have two possibilities. If there exists $j \in ⟦ 1, i ⟧$ such that ${res}_{j} {\hat{θ}}_{j}^{δ} \hat{σ} σ_{L} = {res}_{i + 1} {\hat{θ}}_{i + 1}^{δ} \hat{σ} σ_{L}$ , then we conclude using Lemma 3. If there is not, then since $a_{1}$ is restricted and not deducible (Lemma 9), we have that ${res}_{i + 1}$ is neither deducible itself, nor a subterm of ${\hat{θ}}_{i}^{δ} \hat{σ} σ_{L}$ and ${\hat{θ}}_{i}^{^{t} δ} \hat{σ} σ_{R}$ . Now since $dec$ is a destructor in E, we use Lemma 7 to conclude.
Finally, we have that $ν \tilde{ω} . {\hat{θ}}_{n}^{δ} \hat{σ} σ_{L} \approx_{s} ν \tilde{ω} . {\hat{θ}}_{n}^{^{t} δ} \hat{σ} σ_{R}$ , that is, changing the notations: $\begin{matrix} ν \tilde{ω} . θ_{δ} \hat{σ} σ_{L} \approx_{s} ν \tilde{ω} . θ_{^{t} δ} \hat{σ} σ_{R} . \end{matrix}$ □

7. Further corruption cases using ProVerif

In order to study further corruption cases, we have used ProVerif, one of the only tools that can analyse equivalence properties in the context of security protocols. Since ProVerif does not handle associative and commutative (AC) symbols, we had to simplify the equational theory, yielding theory $E^{'}$ defined by the equations of Fig. 7. The main idea behind $E^{'}$ is to remove associative and commutative symbols from E. All equations besides the AC equations are left unchanged except Eqs (E-5) and (E-6). Equation (E-5) states that two encryptions can be combined, This can no longer be reflected in our ProVerif model. Equation (E-6) models re-encryption. To get rid of AC symbols, we instantiate it with the keys of the protocol ( $a_{1}$ , $a_{2}$ and $a_{3}$ ), preserving the behavior of the protocol, yielding Eq. (E’-5). The fact that we can consider a simplified equational theory weakens the attacker model: some attacks relying on crafty combinations of the messages may be missed. But as shown by our study, this allows to analyse (automatically) more corruption scenario.

Since ProVerif is designed to prove equivalences between processes that differ only by terms, we also needed to use another tool, ProSwapper [28], to cope with the (non deterministic) shuffle done by the Decryption service. More precisely, we actually used their algorithm to compute directly a slightly modified process in our ProVerif specification.

Table 1
Results and performances for proving ballot secrecy using ProVerif

The results1

Tests made on a MacBook Pro (OSX El Capitan 10.11.6) i5 2,3 GHz with 4Go RAM, using the ProVerif 1.94p11 version.

are displayed in Table 1 and the ProVerif files corresponding to our experimentation can be found at [35]. Our case study with ProVerif indicates that ballot secrecy is still preserved even when the Receipt generator is corrupted (as well as several voters), at least in the simplified theory

E^{'}

8. Conclusion

We have proposed the first formal proof in a symbolic model that the e-voting protocol used in Norway indeed satisfies ballot secrecy, even when all but two voters are corrupted and even when the voters communications channels can be eavesdropped and when the Auditor and either the Ballot box or the Receipt generator are corrupted. As expected, ballot secrecy is no longer guaranteed if both the Ballot box and the Receipt generator are corrupted. Slightly more surprisingly, the protocol is not secure either if the Decryption service is corrupted or if the Ballot box and the Auditor are corrupted, as discussed in Section 4.3. Our results in Table 2. In this table, ✓ indicates that ballot secrecy is satisfied and Õ shows that there is an attack. In particular, all the attacks described in Section 4.3 are displayed in the table.

Table 2

Results for ballot secrecy

Instead of doing additional (long and technical) proofs, a further step consists in developing a procedure for automatically checking for equivalences. Of course, this is a difficult problem. A first decision procedure has been proposed in [16] but is limited to subterm convergent theories. An implementation has recently been proposed [15] but it does not support such a complex equational theory. An alternative step would be to develop a sound procedure that over-approximate the relation, losing completeness in the spirit of ProVerif [10] but tailored to privacy properties.

It is also important to note that the security of the protocol strongly relies on the way initial secrets are pre-distributed. For example, three private decryption keys $a_{1}, a_{2}$ , $a_{3}$ (such that $a_{1} + a_{2} = a_{3}$ ) need to be securely distributed among (respectively) the Ballot box, the Receipt generator and the Decryption service. Also, a table $(V, s_{V})$ containing the blinding factor for each voter needs to be securely distributed to Ballot box and a table $(V, d_{V})$ containing a permutation for each voter needs to be securely distributed to the Receipt generator. Moreover, anyone with access with both the codes mailed to the voters and to the SMS emitted by the Receipt generator would immediately learn the values of all the votes. We did not find in the documentation how and by who all these secret values were distributed. It should certainly be clarified as it could be a weak point of the system.

It also remains to study other security properties such as receipt-freeness, coercion-resistance, and verifiability. Receipt-freeness seems to strongly rely on whether the voter may forge a fake table of receipts or fake the message received from the receipt generator. One important feature of the Norwegian protocol is to ensure verifiability even when the voter’s computer is not trusted. Our formal model could serve as a basis, splitting further the voter’s behavior from its computer.

Footnotes

Acknowledgment

The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Program (FP7/2007-2013)/ERC grant agreement $n^{\circ} 258865$ , project ProSecure.

References

Abadi and

Fournet, Mobile values, new names, and secure communication, in: 28th ACM Symposium on Principles of Programming Languages (POPL), 2001.

Arapinis,

Bursuc and

Ryan, Reduction of equational theories for verification of trace equivalence: Re-encryption and AC, in: First International Conference on Principles of Security and Trust (POST’12), Springer, 2012.

Arapinis,

Cortier and

Kremer, When are three voters enough for privacy properties? in: Proceedings of the 21st European Symposium on Research in Computer Security (ESORICS’16), 2016.

Armando,

Basin,

Boichut,

Chevalier,

Compagna,

Cuellar,

Hankes Drielsma,

P.-C.

Héam,

Kouchnarenko,

Mantovani,

Mödersheim,

von Oheimb,

Rusinowitch,

Santiago,

Turuani,

Viganò and

Vigneron, The AVISPA tool for the automated validation of Internet security protocols and applications, in: 17th International Conference on Computer Aided Verification (CAV), 2005.

Basin,

Dreier and

Sasse, Automated symbolic proofs of observational equivalence, in: ACM Conference on Computer and Communications Security (CCS’15), 2015.

Benaloh,

M.D.

Byrne,

Eakin,

P.T.

Kortum,

McBurnett,

Pereira,

P.B.

Stark,

D.S.

Wallach,

Fisher,

Montoya,

Parker and

Winn, STAR-Vote: A secure, transparent, auditable, and reliable voting system, in: 2013 Electronic Voting Technology Workshop/Workshop on Trustworthy Elections (EVT/WOTE’13), 2013.

Bernhard,

Cortier,

Pereira,

Smyth and

Warinschi, Adapting helios for provable ballot secrecy, in: 16th European Symposium on Research in Computer Security (ESORICS), 2011.

Bernhard,

Pereira and

Warinschi, How not to prove yourself: Pitfalls of the fiat-shamir heuristic and applications to helios, in: International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT), 2012.

Bhargavan,

Corin,

Fournet and

Zalinescu, Cryptographically verified implementations for TLS, in: 15th ACM Conference on Computer and Communications Security (CCS), 2008.

10.

Blanchet, An automatic security protocol verifier based on resolution theorem proving (invited tutorial), in: 20th International Conference on Automated Deduction (CADE), 2005.

11.

Blanchet, Vérification Automatique de Protocoles Cryptographiques: Modèle Formel et Modèle Calculatoire. Mémoire d’habilitation à diriger des recherches, Université Paris-Dauphine, 2008.

12.

Blanchet,

Abadi and

Fournet, Automated verification of selected equivalences for security protocols, Journal of Logical and Algebraic Methods in Programming (2008).

13.

Chadha,

Ş.

Ciobâcă and

Kremer, Automated verification of equivalence properties of cryptographic protocols, in: 21th European Symposium on Programming (ESOP), 2012.

14.

Chaum,

Carback,

Clark,

Essex,

Popoveniuc,

R.L.

Rivest,

P.Y.A.

Ryan,

Shen,

A.T.

Sherman and

P.L.

Vora, Corrections to scantegrity II: End-to-end verifiability by voters of optical scan elections through confirmation codes, IEEE Trans. Information Forensics and Security 5(1) (2010), 194. doi:10.1109/TIFS.2010.2040672.

15.

Cheval,

Comon-Lundh and

Delaune, Trace equivalence decision: Negative tests and non-determinism, in: 18th ACM Conference on Computer and Communications Security (CCS), 2011.

16.

Cortier and

Delaune, A method for proving observational equivalence, in: 22nd Computer Security Foundations Symposium (CSF), 2009.

17.

Cortier and

Smyth, Attacking and fixing helios: An analysis of ballot secrecy, Journal of Computer Security (2013).

18.

Cortier and

Wiedling, A formal analysis of the Norwegian E-voting protocol, in: First International Conference on Principles of Security and Trust (POST), 2012.

19.

Cramer,

Gennaro and

Schoenmakers, A secure and optimally efficient multi-authority election scheme, in: International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt), 1997.

20.

Cremers, The scyther tool: Verification, falsification, and analysis of security protocols, in: 20th International Conference of Computer Aided Verification (CAV), 2008.

21.

Delaune,

Kremer and

Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security (2009).

22.

Fujioka,

Okamoto and

Ohta, A practical secret voting scheme for large scale elections, in: Workshop on the Theory and Application of Cryptographic Techniques: Advances in Cryptology, 1992.

23.

Gjøsteen, Analysis of an internet voting protocol. Cryptology ePrint Archive, Report 2010/380, 2010.

24.

Gjøsteen, The Norwegian internet voting protocol. Cryptology ePrint Archive, Report 2013/473, 2013.

25.

Government, Article of the Norwegian government on the deployment of E-voting (last seen: 08-26-16), https://www.regjeringen.no/en/aktuelt/Internet-voting-pilot-to-be-discontinued/id764300/.

26.

Halderman and

Teague, The new South Wales iVote system: Security failures and verification flaws in a live online election, in: 5th International Conference on E-voting and Identity (VoteID’15), 2015.

27.

Khader and

P.Y.A.

Ryan, Receipt freeness of Prêt à voter provably secure. IACR Cryptology ePrint Archive, 2011:594, 2011.

28.

Klus,

Smyth and

M.D.

Ryan, ProSwapper: Improved equivalence verifier for ProVerif (last seen: 08-26-16), 2010, http://www.bensmyth.com/proswapper.php.

29.

Küsters and

Truderung, An epistemic approach to coercion-resistance for electronic voting protocols, in: IEEE Symposium on Security and Privacy (S&P), 2009.

30.

Lee,

Boyd,

Dawson,

Kim,

Yang and

Yoo, Providing receipt-freeness in mixnet-based voting protocols, in: 6th International Conference on Information Security and Cryptology (ICISC), 2004.

31.

Liu, A proof of coincidence of labeled bisimilarity and observational equivalence in applied pi calculus, 2011, http://lcs.ios.ac.cn/~jliu/papers/LiuJia0608.pdf.

32.

Ohkubo,

Miura,

Abe,

Fujioka and

Okamoto, An improvement on a practical secret voting scheme, in: 2nd International Information Security Workshop (ISW), 1999.

33.

A.T.

Sherman,

Carback,

Chaum,

Clark,

Essex,

P.S.

Herrnson,

Mayberry,

Popoveniuc,

R.L.

Rivest,

Shen,

Sinha and

P.L.

Vora, Scantegrity mock election at Takoma Park, in: 4th International Conference on Electronic Voting 2010 (EVOTE’10), 2010, pp. 45–61.

34.

Tiu and

J.E.

Dawson, Automating open bisimulation checking for the spi calculus, in: 3rd IEEE Computer Security Foundations Symposium (CSF), 2010.

35.

Wiedling, Source files for ProVerif code, http://people.rennes.inria.fr/Cyrille.Wiedling/Resources/resources.html.

A formal analysis of the Norwegian E-voting protocol

Abstract

Keywords

1. The Norwegian e-voting protocol

1.1. Setting phase

1.2. Submission phase

2. Applied pi-calculus

2.1. Terms

Definition 1 (Convergence).

Definition 2 (AC-Convergence).

2.3. Processes

Definition 3 (Static equivalence).

2.6. A detailed example

3. Modeling the Norwegian protocol

3.1. Equational theory

3.2.1. Voting process

3.2.2. Ballot box

3.2.3. Receipt generator

3.2.4. Decryption service

3.2.5. Auditor

3.2.6. Norwegian protocol and corruption scenarios

4. Formal analysis of ballot secrecy

4.1. Corrupted ballot box and corrupted voters

5. Lemmas for static equivalence

5.1. Generic lemmas

6.1. Definitions and useful lemmas

Table 1 Results and performances for proving ballot secrecy using ProVerif

Footnotes

Acknowledgment

References

Table 1
Results and performances for proving ballot secrecy using ProVerif