Behnoosh Namdarzadeh

Nicolas Ballier

The neural machine translation of dislocations

Keywords: dislocation, language pairs French English, neural machine translation

. We analysed 436 translations of French dislocated segments in the novel Voyage au bout de la nuit (Céline 1932) and a contemporary corpus for spoken data from Corpus de Français Parlé Parisien (CFPP) (Branca-Rosoff & Lefeuvre 2016) by DeepL and Google. Beyond prototypical X, c'est dislocations, translation toolkits continue to misfire, and this might be due to the lack of spoken data in training sets of NMT.

Introduction

This paper replicates the challenge set approach proposed by Pierre Isabelle and colleagues for English into French [START_REF] Isabelle | A Challenge Set Approach to Evaluating Machine Translation[END_REF]). The idea is to target the difficult linguistic features and observe the output of machine translation systems like Google Translate and DeepL. Our focus for our challenge set is dislocations; structures where double constituents are licit in the source text (like two grammatical subjects in French) but not in English.

Dislocations are universal [START_REF] Lambrecht | Information structure and sentence form: Topic, focus, and the mental representations of discourse referents[END_REF]) and all languages seem to have identical forms of topic-marking. Syntactically, two positions can be considered. One is called theme or Left Dislocation (LD), a clause and a constituent to its left. In the example "[Peter] I've known him for a long time" [START_REF] Westbury | Left dislocation: A typological overview[END_REF], Peter is a dislocated segment which occurs before the clause. The other is right dislocation (RD). In the example "He lived in Africa, [the wizard] (Lambrecht 1994) right dislocation has the wizard at the right edge of the sentence. Pragmatically, a linear arrangement of linguistic elements in a sentence affects information packaging. Our dislocation challenge set of French examples encompasses a pragmatic need (usually expressed by thematization) and a syntactic constraint (only one subject) for the translations into English.

Methodology

Our corpus includes Voyage au bout de la nuit from the INTERSECT parallel corpus [START_REF] Salkie | INTERSECT[END_REF]. The reference translation in English of the French sentences in which dislocation occurs was obtained using AntPConc software.

In addition to this classic subcorpus, a contemporary corpus for spoken data from the Corpus de Français Parlé Parisien (CFPP) des années 2000 (Branca-Rosoff & Lefeuvre 2016) was also searched using the Universal Dependency (UD) annotation to retrieve the possible dislocations with the dependency relation. Annotation was performed with the {UDpipe} package in R. The corpora yielded 2,546 occurrences, out of which we analysed 436 translations by DeepL and Google translate. We briefly report the discrepancies in the translations of dislocations observed in our corpus.

Results

While we do not report recall for the automatic detection of dislocations with UD, the precision of our retrieval method was pretty accurate for the 218 analysed dislocations (91% and 98 %). Few false positives were detected but more frequently for the written data (appositions and parentheticals mistaken as dislocations) than for the spoken data (repairs and repetitions). The detailed typology of dislocations observed in the data is beyond the remit of this paper. We describe the complexity of the dislocations in Table 1 by reporting multiple cases of dislocations within sentences, much more frequent in our spoken data. We focus on the dominant type of dislocations (<left dislocated item>, c'est dislocations) and compare the two toolkits on their ability to produce translations that avoid the repetition of the subject (we call it "subject copy"). C'est constructions often have ça as a left dislocated constituent like ça c'est vrai [START_REF] Céline | Voyage au bout de la nuit[END_REF], which is translated as that is true. Despite the high number of occurrences of c'est construction in both of our corpora (62 occurrences out of 109 sentences for the novel and 73 occurrences out of 109 sentences for CFPP), there is still a deficiency in translating this construction by the toolkits. Google tends to produce more "subject copies" in typical examples. The picture is more blurred for more complex cases like l'amour c'est elle la misère … [START_REF] Céline | Voyage au bout de la nuit[END_REF], Google outperforms DeepL and translates it as love is misery … with the suppression of the extra subject which is not required in English, whereas DeepL output is closer to the ST translation suggesting the love it is it the misery… .

Left dislocated items can also be stacked as instances with more than two constituents for topic-marking function [START_REF] Raquel | Establishing topic in conversation: A contrastive study of leftdislocation in English and Spanish[END_REF]. For example, in Lui, le père, je l'apercevais… [START_REF] Céline | Voyage au bout de la nuit[END_REF], which includes double topicalization, all the initial subjects are translated by the two translation toolkits as him, the father, I …. . In the other example, moi ça m'a toujours semblé… normal… (Branca-Rosoff, Lefeuvre 2016), Google keeps the structure of double topicalization as in the French source text and translates it into me it always seemed to me… normal, whereas, DeepL omits the extra subject and translates it into I always thought it was… normal.

Many dislocations have a tonic pronoun as the left dislocated item, prototypically the moi, je construction in French sentences. It can be tricky for the MT systems. In translating the source text mais autrement non moi je trouve j'aime bien (Branca-Rosoff, Lefeuvre 2016), Google follows word-by-word strategy translating it into but otherwise not me I find I like. DeepL omits this part of the source text and suggests but otherwise I like it.

Table 1 .

 1 Distribution of main dislocation types and success rate for the c'est

	dislocation in our data.
	corpora	multiple c'est	"subject copy" in the translation
	Voyage (n=109)	15	62	Google = 17, DeepL = 11
	CFPP (n=109)	22	73	Google = 30, DeepL = 32

Acknowledgements

Part of this research was financed within the SPECTRANS project, funded under the 2020 émergence research project, under the ANR grant (ANR-18-IDEX-0001, Financement IdEx Université de Paris).

Discussion and conclusion

We retained the original absence of punctuation (commas) of the CFPP, which is even more distinct from the canonical training data of the toolkit. For instance, translating the French ST le parc Mabille[,] c'est parc des Beaumonts maintenant[,] ils l'ont bien aménagé (Branca-Rosoff & Lefeuvre 2016), DeepL suggests the park Mabille it is park of Beaumonts now they arranged it well. The zero article for Parc de Beaumonts may account for the absence of recognition of the pattern. We revised the transcription of CFPP and added commas where appropriate to check the ability of the MT toolkits. Re-punctuating the sentences (see our [,]) did not solve the it subject copy issue.

Analysing only 436 translations of dislocated constructions produced by Google and DeepL still outlines meaningful patterns for the toolkit translations of this tricky structure. The partial success with c'est dislocation suggests training data is crucial for the results. Les frequent structures tend to be mistranslated, especially for spoken data. Overall, the challenging dislocated segments mainly originate from spoken language and this might suggest that more spoken data should be included in the training sets of neural machine translation.

While parentheticals seem to ease the translation of dislocations, more complex structures with stacking remain an issue for NMT toolkits. The topicmarking function and some tropicalized object constructions can also be challenging.

The overall patterns differ in the two toolkits. On the one hand, Google seems to keep the paratactic structure of the French source sentence, i.e., to produce a word-by-word translation of the structure and to reiterate the words. If anything, Google tends to be more source-based for the translation of dislocations and more systematically preserves the original punctuation. On the other hand, DeepL outputs are hypotactic in a sense that even for double constituents, the toolkit suppresses reiterations or links the constituents using subordinating conjunctions.


Vincent Cheval
email: vincent.cheval@inria.fr

Véronique Cortier
email: veronique.cortier@loria.fr

Alexandre Debant
email: alexandre.debant@inria.fr

Election Verifiability with ProVerif

Electronic voting systems should guarantee (at least) vote privacy and verifiability. Formally proving these two properties is challenging. Indeed, vote privacy is typically expressed as an equivalence property, hard to analyze for automatic tools, while verifiability requires to count the number of votes, to guarantee that all honest votes are properly tallied.

We provide a full characterization of E2E-verifiability in terms of two simple properties, that are shown to be both sufficient and necessary. In contrast, previous approaches proposed sufficient conditions only. These two properties can easily be expressed in a formal tool like ProVerif but remain hard to prove automatically. Therefore, we provide a generic election framework, together with a library of lemmas, for the (automatic) proof of E2E-verifiability. We successfully apply our framework to several protocols of the literature that include two complex, industrial-scale voting protocols, namely Swiss Post and CHVote, designed for the Swiss context.

Introduction

It is now a standard practice to analyze security protocols with formal methods during their design for example with tools like ProVerif [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF] or Tamarin [START_REF] Meier | The Tamarin Prover for the Symbolic Analysis of Security Protocols[END_REF]. It is the case of major protocols like TLS1.3 [START_REF] Bhargavan | A symbolic analysis of privacy for TLS 1.3 with encrypted client hello[END_REF] or Signal [START_REF] Cohn-Gordon | A Formal Security Analysis of the Signal Messaging Protocol[END_REF]. Voting protocols form a particular class of protocols that combines several difficulties: complex cryptographic primitives that yield complex equational theories, a large number of actors (e.g. server, registrar, voting client, tally authorities) and therefore a large number of threat scenarios, and non standard security properties. Thus voting protocols push formal tools at their limits. Yet, it remains crucial to conduct a formal analysis to avoid undetected flaws and it is actually even a legal requirement in Switzerland [START_REF] Confederation | Technical and administrative requirements for electronic vote casting[END_REF].

Voting systems should guarantee two main security properties: vote secrecy (no one should know how I voted) and verifiability (my vote should be properly counted). Depending on the election context, other properties may be desired such as coercion-resistance or accountability. Vote secrecy is expressed as an equivalence property: an attacker should not distinguish between two scenarios where voters This work was partly supported by the following grants: ANR Chair AI ASAP (ANR-20-CHIA-0024) and ANR France 2030 project SVP (ANR-22-PECY-0006). switch votes. It often focuses much of the attention since equivalence properties are typically harder to analyze than trace properties. In that respect, verifiability seems easier to prove. However, looking at the literature, it can first be noticed that it is not easy to define. Several terminologies have been developed. One is the motto: cast-as-intended, recorded-as-cast, tally-as-recorded. This intuitively says that the ballot of a voter should contain their intended vote, their ballot should be recorded without modification, and finally, the tally should make sure that it counts all the ballots. This terminology however fails to capture eligibility: only legitimate ballots should be counted, otherwise the system could be subject to ballot stuffing. Another standard terminology covers this case. It splits verifiability into three sub-properties:

• individual verifiability: a voter should be able to check that their ballot is in the ballot box. This sometimes includes cast-as-intended, • universal verifiability: the result should correspond to the ballot box, • eligibility verifiability: ballots should come from legitimate voters However, these two sets of properties still miss some attacks! As pointed out by Ralf Küesters et al [START_REF] Küsters | Clash Attacks on the Verifiability of E-Voting Systems[END_REF], a voting system should also prevent clash attacks, where two honest voters are (maliciously) given the same ballot, yielding the loss of one honest vote.

Hence, it is safer to define verifiability as a global property, as done in [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF]. Intuitively, a voting system satisfies E2E-verifiability if the result of the election corresponds to:

• all the votes of honest voters that did verify their votes;

• a subset of the votes of honest voters that did not verify;

• k additional votes, where k is bounded by the number of dishonest voters. This approach does not need to assume any structure on the voting systems like the existence of a board or a clear tally phase (sometimes invalid ballots are discarded during the tally, sometimes at an earlier stage). However, such a property is much more difficult to analyze for tools like Tamarin or ProVerif since it requires to count the votes. Therefore, previous works have proposed sufficient conditions, that imply E2E-verifiability and are easier to prove, either for ProVerif [START_REF] Cortier | Beleniosvs: Secrecy and verifiability against a corrupted voting device[END_REF], or for Tamarin [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF], [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF]. Unsurpris-ingly, these sufficient conditions are close to the notion of individual, universal, eligibility verifiability, and no-clash. These approaches however suffer from several drawbacks:

• These sufficient conditions may be too strong. For example, in [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF], they found that Belenios does not satisfy one of their properties, with no corresponding attack against E2E-verifiability. • These conditions are specific to some architecture and assume e.g. a bulletin board, registrars, and voting credentials. [START_REF] Cortier | Beleniosvs: Secrecy and verifiability against a corrupted voting device[END_REF] even needs to define two sets of sufficient conditions, depending on whether the Registrar or the Voting Server is honest. • These conditions are stated on ballots "about to be counted". The tally part is typically excluded from the models and hence not verified.

Our contributions. Our first contribution is to characterize E2E-verifiability with two simple injective properties. The first one says that any honest verified vote should (injectively) be counted in the result of the election.

inj-verified(id, v) ⇒ inj-counted(v)
The other property controls the other direction and makes sure that any counted vote come from a legitimate voter (honest or dishonest). We show that these two properties not only suffice to prove E2E-verifiability but are also necessary, yielding a complete characterization of E2Everifiability. This result holds for arbitrary protocols and arbitrary cryptographic primitives. The only assumption is that the result of the election is the (multi)set of votes, which covers most elections. Interestingly, these two properties are directly expressible in ProVerif, hence we chose ProVerif to build our framework, although a similar approach could probably be developed for Tamarin, after some preliminary work like the one performed for handling global states [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF].

However, our properties only hold once the tally is over. Indeed, even if a voter successfully verifies during the voting phase, their vote is (obviously) not yet counted. Moreover, the model needs to reflect the fact that all valid ballots are eventually processed. Most existing models (e.g [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF], [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF], [START_REF] Cortier | A formal analysis of the neuchâtel e-voting protocol[END_REF], [START_REF] Cortier | A formal analysis of the norwegian e-voting protocol[END_REF]) are instead very permissive and let the tally stop at any time. This, in passing, show that they only check some partial properties w.r.t. verifiability. Instead, we need here to faithfully model the fact that ballots are typically stored in a stack and the tally is over when all ballots have been processed, yielding an empty stack. Combined with the verification of injective properties, this may cause all kind of issues to verification tools, as ProVerif experts may have already guessed.

To overcome these issues, we use the whole machinery recently introduced in ProVerif [10]: use of counters, lemmas, axioms, and restrictions. Our second contribution is a generic and re-usable framework for proving E2Everifiability. Namely, we propose a reference model for a mini-voting scheme, with a library of corresponding lemmas and axioms. This generic models needs then to be populated with the behavior of the considered protocol. For example, the setup process needs to define the public and private data generated for each voter, possibly introducing new actors. Similarly, the voting process defines the voter's behavior and returns in the end the ballot that should be cast. We applied our framework to Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] and Belenios [START_REF] Cortier | Belenios: a simple private and verifiable electronic voting system[END_REF], studied in previous approaches aiming at proving verifiability [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF], [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF], [START_REF] Cortier | Beleniosvs: Secrecy and verifiability against a corrupted voting device[END_REF]. We also cover two complex, industrial-scale protocols, namely CHVote [START_REF] Haenni | CHVote system specification[END_REF] and SwissPost [1]. These two protocols involve complex primitives (e.g. oblivious transfer for CHVote) with ad-hoc encoding as equational theories, and their architecture differs a lot from Helios and Belenios. In particular, the server is split into 4 independent components and there is no public bulletin board. Voters do not check the presence of their ballots but instead receive return codes from their voting device, checked against a code sheet. It is important to note that we did not write any of these ProVerif models. For our 4 case studies, we filled our framework (designed once and for all) with the existing models. We got them from public repositories presenting security analyses of these protocols and just fit them with a few adjustments. In particular, because our two properties cover E2E-verifiability, we needed to more faithfully model the registration and the tally phase. ProVerif was able to automatically prove our two injective properties, hence E2Everifiability, thanks to our main theorem. No manual work outside of the framework was required except for one variant of Belenios that involves a chain of hashes. Due to the intrinsic complexity of this protocol, a couple of customized lemma have been added. In all cases, the ProVerif verification was fast (around 1 minute or below).

ProVerif

We provide an informal introduction of the syntax and the semantics of the ProVerif tool. A comprehensive description is available in [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF]. An excerpt of the syntax of ProVerif is displayed in Figure 1.

Messages

ProVerif relies on a symbolic model in which messages are represented by terms, formed of symbolic functions and atomic data. Atomic data represent nonces, keys, or any constant. Function symbols model cryptographic primitives such as encryption, signature, or hash function. For example, the encryption of the message m with the public key pk(k) and the random r can be modeled with the term aenc(pk(k), r, m) where aenc(•, •, •) is a symbol of function modeling any encryption scheme. Relations between terms are modeled by rewriting rules. For instance, to model that a participant is able to decrypt a message as soon as he knows the corresponding private key, we define a destructor symbol adec(•, •) to represent the decryption algorithm and the rewriting rule: adec(k, aenc(pk(k), r, m)) → m. Similarly, destructor symbols and rewriting rules can be defined to model the verification algorithms of signatures or ZK proofs.

Protocols

Protocols are modeled through a process algebra similar to the applied pi-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Fresh names unknown to the attacker are generated with the command new n. Tests can be evaluated using conditional declarations of the form let x = v in P : the process P in which x is replaced by v is executed if v reduces to a term without destructor symbols when applying rewriting rules. Communications are modeled using the usual in(c, x) and out(c ′ , u) commands, modeling respectively, an input on channel c and the output of message u on channel c ′ . It is important to note that an input can be filled with any message known by the attacker when c is public. Agent states are defined with table in which processes can insert elements using the insert command and then test whether there exists a entry satisfying a formula ϕ using the get command. If so, the process P in which x 1 , . . . , x k are instantiated according to the considered table entry is executed, and Q otherwise. Finally, P | Q models that two processes are executed in parallel, and !P represents an arbitrary number of processes P executed in parallel. ProVerif also contains a command event(E(u 1 , . . . , u l )) where E(•) is an event function symbol and u 1 , . . . , u l are messages. These events are annotations whose semantics does not interfere with the execution of the protocol. The operational semantics is defined e.g. in [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF]. We note Traces(P ) the set of execution traces of the process P , i.e. a sequence P → P 1 → P 2 → . . . → P n where → denotes a step in the operational semantics. We note → * the transitive closure of →.

M, N, M 1 , . . . , M k ::= terms x | n | f (M 1 , . . . , M k ) D::= expressions M | h(D 1 , . . . , D k ) ϕ::= formula M = N | ϕ 1 ∧ ϕ 2 | ϕ 1 ∨ ϕ 2 | ¬ϕ
Example 1. We consider the voting protocol Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] as a running example. In this protocol, when a voter wishes to vote for v, they authenticate themselves to the server and submit an encrypted ballot pseudo, aenc(pk E , r, v) using the public key pk E of the election and a pseudonym pseudo. The pseudonym is optional in Helios but we consider here a version with pseudonym as it allows to distinguish between the id of the voter and their cryptographic data. Voters can check right before the tally that their ballot belongs to the (public) final bulletin board. The corresponding process, associated to a voter id is as follows. Helios assumes a secure authenticated channel between the voter and the server. We model this as a channel created during the registration phase and shared between voter and server using a table voting_data. Both can read in this data base to retrieve the corresponding channel. The attacker should be able to read data sent on the authenticated channel (since it is not assumed to be a private channel), and thus all the outputs on the private channel are preceded by an output of the same data on the public channel c pub .

The second part of the voter process models the fact that the voter may verify that their vote appears on the bulletin board. More precisely, we model that the voter verifies their last ballot only, that is, the one that should be counted. To do so, we use a private channel cell voter (id voter ) that is read at the beginning of the process (hence consuming the channel since communication are synchronous) and is only released if the voter does not verify, offering them the possibility to vote again. The content of this channel also records how many ballots the voter has cast so far relying on the variable nb vote which is incremented at the end of each session.

The voting process is annotated with events, whose role will be explained in the next sections.

Security properties

ProVerif allows to verify two kinds of properties: correspondence queries and observational equivalence. In the e-voting context, queries are used to express verifiability while observational equivalence is used to model privacy.

Correspondence queries. Given a trace tr = tr 1 . . . . .tr n , we say that tr executes event(E(u 1 , . . . , u l )) at time i ∈ {1, . . . , n} if tr i identifies a semantics step that executes event(E(u 1 , . . . , u l )). Correspondence queries are formulas of the form:

p k=1 F k (v 1 , . . . , v l k ) ⇒ m i=1 ni j=1 E i,j (u i,j 1 , . . . , u i,j li,j )
Such a query is satisfied by a process P if for all traces tr ∈ Traces(P ), whenever there exists a substitution σ such that for all k ∈ {1, . . . , p} the event event(F k (v 1 . . . , v l k ))σ is executed in tr, then for any i, there exist a substitution σ ′ and j such that for all k, F k (v 1 . . . , v l k )σ ′ = F k (v 1 . . . , v l k )σ and event(E i,j (u i,j 1 , . . . , u i,j li,j ))σ ′ is executed in tr. Queries are extended as expected with test equalities v = v ′ , dis-equalities v ̸ = v ′ and predicates pred(v 1 , . . . , v p ).

Injective correspondence queries. To model finer grained properties, ProVerif allows to define injective correspondence queries whose purpose is to capture one-to-one relationship between events. For sake of simplicity, we define here the semantics of the class of injective queries we need to establish our main result. A comprehensive semantics for injective queries is available in [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF]. Injective correspondence queries are formulas of the form:

inj-F 0 (v 1 , . . . , v l0 ) ∧ p k=1 F k (v 1 , . . . , v l k ) ⇒ m i=1 inj-E i,0 (u i,0 1 , . . . , u i,0 li,0 ) ∧ ni j=1 E i,j (u i,j 1 , . . . , u i,j li,j )
Given a trace tr = tr 1 . . . . .tr n , we note F(tr) the set of indices α such that tr executes F 0 (v 1 , . . . , v l0 )σ at time α for some σ. Similarly, we note E(tr) the set of indices β such that tr executes E i,0 (u i,0 1 , . . . , v i,0 li,0 )σ at time β for some σ and i. An injective correspondence query as defined above is satisfied by a process P if for all trace tr ∈ Traces(P ), whenever there exists a substitution σ such that for all k ∈ {0, . . . , p} the event event(F k (v 1 . . . , v l k ))σ is executed in tr, then there exists i and a substitution σ ′ such that for all

k, F k (v 1 . . . , v l k )σ ′ = F k (v 1 . . . , v l k )σ
and for all j, event(E i,j (u i,j 1 , . . . , u i,j li,j ))σ ′ is executed in tr. Moreover, there exists an injective function f :

F(tr) → E(tr) such that if F 0 (v 1 , . . . , v l0 )σ is executed in tr at time α then E i,0 (u i,0 1 , . . . , u i,j li,0 )σ ′ is executed in tr at time f (α).
Informally, a protocol P satisfies an injective query if it satisfies the non-injective counterpart, and if there is a oneto-one mapping between injective events used to satisfy the query.

Example 2. Let E 1 (•), E 2 (•)
and F (•) be three event function symbols of arity 1. Let tr 1 , tr 2 , and tr 3 be three traces such that tr

1 = event(E 1 (n)).event(F (n)).event(E 2 (m)).event(F (m)), tr 2 = event(E 1 (n)).event(E 2 (n)).event(F (n)) and tr 3 = event(E 1 (n)).event(F (n)).event(F (n)). If we consider the injective query ρ = inj-F (x) ⇒ inj-E 1 (x) ∨ inj-E 2 (x)
then we have:

• tr 1 satisfies ρ. We can define the injective function f such that f (2) = 1 and f (4) = 3;

• tr 2 satisfies ρ. We can define the injective function f 1 such that f 1 (3) = 2 or the injective function f 2 such that f 2 (3) = 1. We note that, contrary to item 1, the functions f 1 and f 2 are not surjective over E(tr 2 ) = {1, 2}. • tr 3 does not satisfy ρ. There is no injective function f : {2, 3} → {1}.

Temporal queries. Facts in queries may be annotated with temporal variables, yielding a temporal fact F @i. Given a trace tr = tr 1 . . . . .tr n , the temporal fact F @i is executed in tr w.r.t. a substitution σ if tr σ(i) = F σ. This allows e.g. to specify when an event should occur before another one.

Example 3. The following query states that the event verified should occur at most once per voter.

verified(id, x)@i ∧ verified(id, y)@j ⇒ i = j

Definition of E2E verifiability

E2E verifiability intuitively guarantees that the result of the election reflects the votes of the voters. We state this property using events that record when a voter votes or verifies and when a vote is counted.

Events

A voting process is a process that contains several special events:

• voted(id, v) represents the fact that voter id believe they have voted for v. In any voting protocol, the voter knows for who they have tried to vote for. • verified(id, v) represents the fact that voter id has voted for v and successfully performed the verification test, that is optional in many cases. The event should be executed at most once for each voter, typically for the final vote when revoting is allowed. • counted(v) tells that a vote has been counted for v.

We consider elections where the multiset of votes is displayed at the end of the election. • finish tells that the tally procedure is over, no more counted event will be emitted. Moreover, we assume that any voter id occurs exactly once in one of these three events:

• hv(id) means that the honest voter id will vote and verify their vote. • hnv(id) means that the honest voter id will vote but not necessarily verify their vote. • corrupt(id) records that voter id is corrupted and the attacker typically has access to their credential. Our characterization of E2E-verifiability will hold independently on how these events are placed but of course, E2E verifiability will only be meaningful when these events are properly placed (like in any model). We illustrate this on our running example.

Example 4.

Continuing Example 1, we first note that in the voter process, the events voted(id, v) and verified(id, v) occur as expected. The remaining processes representing Helios are displayed in Figure 2.

The process Voter_registration(id) creates an authenticated channel and a public pseudonym for any voter and assigns the voter to corrupt, hv, or hnv, at the attacker's will, with corresponding events. As expected, the channel is given to the adversary when the voter is corrupted. In order to model that voters in hv will verify, we restrict the analysis to traces satisfying the property:

finish ∧ hv(id) ⇒ verified(id, x).
This can easily be modeled in ProVerif, using a new feature, called restriction [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF], that allows to discard traces that do not satisfy the property stated in the restriction.

The public bulletin board is modelled by private channels cell BB (id). There is one per eligible voter. This allows each voter to easily find their vote on the board. But we make sure to let the adversary reads the board and also writes on it when the server is corrupted.

The Voting Server is modelled as expected. It receives ballots and publishes them on the public board, that is on the channel cell BB (id) corresponding to the voter.

The content of the channel cell BB (id) is initialized at empty at registration and may then change several times when the voter revotes. At some point, the voter stops and the last published ballot will be counted. This is modeled by the process Close_voting_booth() that transfers the content of cell BB (id) to a new channel cell tally (id). This process does not release cell BB (id) hence it can no longer be used.

Finally, the process Tally(skE) decrypts all received ballots, skiping voters that did not vote.

How to place the event finish? Placing the finish event is a challenging task. Indeed, this event must ensure that all the ballots have been counted. In this first example, we describe a solution when considering a bounded number of voters. A more general approach for an unbounded number is presented in Section 5. When the i-th ballot is processed by the tally process, the constant OK is sent on private channel c end (i). We then consider the process Finish that gathers all these confirmations (a finite predefined number) before executing finish. The process Finish is an example for two voters.

Definition

Given two multisets S 1 and S 2 we denote S 1 ⊆ m S 2 their inclusion and S 1 ∪ m S 2 their union. The subscript m may be omitted when it is clear from the context that the relation is applied to multisets.

Given a trace tr of a voting process P , we define the set of involved voters as Voters = HV ∪ HNV ∪ D where:

• D is the set of corrupted voters, i.e., D = {id | corrupt(id) ∈ tr} is the set of dishonest voters. • HV is the set of voters who verify, i.e., HV = {id | hv(id) ∈ tr and verified(id, v) ∈ tr}. We note V hv the corresponding multiset of vote intentions:

V hv = {v | verified(id, v) ∈ tr and id ∈ HV}

• HNV is the set of voters who do not necessarily verify, i.e., HNV = {id | hnv(id) ∈ tr}. We note V hnv the corresponding multiset of vote intentions:

V hnv = {v | voted(id, v) ∈ tr and id ∈ HNV}
We note that for honest voters who do not verify, we consider all the votes that the voter has submitted. We will say that a system is secure as soon as if a ballot is counted for these voters then it corresponds to one of the submitted vote (not necessarily the last one). This definition is consistent with [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF] and [START_REF] Cortier | Beleniosvs: Secrecy and verifiability against a corrupted voting device[END_REF], [START_REF] Cortier | Voting: You can't have privacy without individual verifiability[END_REF] when no revote is permitted. In order to consider at most one vote per voter, we consider all the voted events associated to a voter.

V id hnv = {(id, v) | voted(id, v) ∈ tr and id ∈ HNV} We say that V ⊆ id m V id hnv if V is a selection of at most one vote per voter, that is, if there exists a multiset V id such that V = {v | (id, v) ∈ V id } and V id ⊆ m V id hnv and two elements (id, v), (id ′ , v ′ ) of V id have different ids, i.e. id ̸ = id ′ .
The result of the election is the multiset of counted votes:

Result = {v | counted(v) ∈ tr}
Definition 1. A voting process P satisfies E2E-verifiability if, for any trace tr of P that contains the event finish, there exist

V ′ hnv ⊆ id m V id hnv and V d such that |V d | ≤ |D| and Result = V hv ∪ m V ′ hnv ∪ m V d
For sake of understandability, this definition deserves some comments:

1) As stated, E2E verifiability provides strong guarantees to honest voters who decide to abstain. Indeed, this definition guarantees that an attacker is not able to cast a ballot on behalf of such a voter. Any ballot recorded in the name of an honest voter must have been intentionnally cast by this voter; this is the purpose of the multiset V ′ hnv ⊆ id m V id hnv . 2) When no revote is allowed, we can equivalently write

V ′ hnv ⊆ id m V id hnv and V ′ hnv ⊆ m V hnv .
In this case, we retrieve the original definition of [START_REF] Cortier | Beleniosvs: Secrecy and verifiability against a corrupted voting device[END_REF], [START_REF] Cortier | Voting: You can't have privacy without individual verifiability[END_REF].

3) When revote is allowed and in case the voted event occurs each time a voter votes, the definition is rather weak: not only ballots may be dropped for voters who do not verify but the adversary can actually pick any of the ballots a voter has voted. This corresponds to the definition proposed in [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF] and the one actually satisfied in practice. Indeed, in most existing protocols, if Alice does not verify, the adversary may simply let her vote normally until the vote of his choice, and then drop all future ballots. 4) In case voted events occur only when a voter votes for the last time, then E2E-verifiability captures a stronger property where voters who do not verify are guaranteed that their last ballot is either counted or dropped, but no previous ballots can be counted. Interestingly, our results hold independently on how voted events are placed. Hence both properties can be considered using our simpler, equivalent queries.

Characterization of E2E verifiability

We can equivalently translate E2E verifiability into two simple injective properties, more amenable to verification.

Assumptions

The previously mentioned events can actually be placed arbitrarily, this will not impact our main theorem. Of course, E2E-verifiability may not hold when the events are not properly placed, for example if verified is placed before the voter is done checking their ballot. However, the equivalence between E2E-verifiability and the two properties will remain. We only need a few assumptions, that we list here.

• We assume the sets HV, HNV and D to be pairwise disjoint. This should hold in any reasonable model and can be easily checked in ProVerif. • We assume that whenever verified(id, v) ∈ tr then voted(id, v) ∈ tr. This is easy to ensure and check. • Finally, the verified event should be executed at most once per voter. Note that the E2E-verifiability property makes sense only in this case anyway. As seen in Example 3, this property can easily be written in ProVerif using a temporal query.

verified(id, x)@i ∧ verified(id, y)@j ⇒ i = j

A voting process is a process satisfying these 3 properties 1 .

ProVerif queries

We can characterize E2E-verifiability by two simple injective queries that intuitively check the double inclusion of the two sets Result and

V hv ∪ m V ′ hnv ∪ m V d . query 1 finish ∧ inj-counted(x) ⇒ inj-hv(z) ∧ verified(z, x) ∨ inj-hnv(z) ∧ voted(z, x) ∨ inj-corrupt(z)
1. Note that, as mentioned in Section 5.2.2, in our framework all these protocol assumptions are automatically checked by ProVerif before starting the security analysis.

query 2 finish ∧ inj-verified(z, x) ⇒ inj-counted(x)
Intuitively, query 1 ensures that any counted vote comes from a legitimate voter, honest or dishonest. Conversely, query 2 makes sure that any verified vote is counted.

Theorem 1. A voting process P is E2E-verifiable if and only if it satisfies query 1 and query 2.

We prove Theorem 1 by showing that a trace satisfies the E2E-verifiability property if and only if it satisfies query 1 and query 2. Not only this allows us to conclude but interestingly, this shows that our result is independent of the exact execution semantics of a process. In particular, our result is likely to apply in other contexts like the framework of Tamarin [START_REF] Meier | The Tamarin Prover for the Symbolic Analysis of Security Protocols[END_REF].

We prove separately the two implications in Lemma 1 and Lemma 2.

Lemma 1. If a voting process P is E2E-verifiable then it satisfies query 1 and query 2.

This direction is rather easy: the definition of E2Everifiability allows to construct injective functions that satisfy query 1 and query 2. The proof is given in appendix.

Interestingly, this direction was missing (and false) in previous approaches [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF], [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF], [START_REF] Cortier | Beleniosvs: Secrecy and verifiability against a corrupted voting device[END_REF] that provided only sufficient conditions for E2E-verifiability, that were too strict in general. As mentioned in introduction, the study of [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF] shows that the Belenios protocol does not satisfy one of their conditions, while no attack against verifiability is exhibited. We further comment this false negative in appendix B.

Lemma 2. If a voting process P satisfies query 1 and query 2 then it is E2E-verifiable.

Proof sketch. This direction requires more care. Instead of representing Result as a multiset of votes v, we represent it as a set of pairs x = (v, i) where v is a vote and i is its occurrence index, i.e. x is the i-th vote for v in the trace under study. Thus, from query 1, we deduce the existence of an injective function f : Result → Voters. More precisely, the image of f is Im(f ) = HV ′ ∪ HNV ′ ∪ D ′ with HV ′ ⊆ HV, HNV ′ ⊆ HNV, and D ′ ⊆ D. If f were surjective over HV, we could easily conclude but unfortunately, f is not necessarily surjective over HV. From query 2 and the assumption that finish ∧ hv(id) ⇒ verified(id, v), we deduce the existence of an injective function g : HV → Result. This is illustrated in Figure 3.

We use g to transform f into an injective function h : Result → Voters that is surjective over HV.

We define h by h

(x) =      g -1 (x) if x ∈ g(HV) (i) (f • g) n • f (x) if x / ∈ g(HV) and f (x) ∈ HV (ii) where n = min{i > 0 | (f • g) i • f (x) / ∈ HV} f (x) otherwise (iii)
Case (i) makes sure that h is surjective over HV. We need to show that h is well-defined. Intuitively, to associate a vote x to a voter, we can simply consider f (x). But in order to ensure that h is injective, this does not work when f (x) ∈ HV. Hence we try to escape from HV by composing f • g. We can prove that we eventually leave HV as HV is finite and f and g are injective, as illustrated in Figure 4.

We can then prove that h is injective and use h to prove E2E-verifiability. The full proof is given in appendix.

A generic ProVerif voting framework

Thanks to our two verifiability queries, we can check E2E-verifiability using ProVerif. However, it requires to overcome different difficulties.

First, the model of the protocol must be accurate enough. In particular, it requires to faithfully model the tally process, which was typically abstracted away in most previous analyses. It needs to enforce that the tally phase processes all the ballots collected in the ballot-box during the voting phase of the protocol. As an immediate consequence, the model must precisely describe the voter registration phase too. To ease the modeling of a protocol, we propose a common framework which abstracts most of the technical details. The framework is described in Section 5.1.

Second, because of the accuracy of the model, it appeared that ProVerif fails to automatically prove our two security properties. Therefore, we extended our initial framework to guide ProVerif proofs. This includes techniques à la GSVerif [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF] and generic lemmas that the framework should satisfy. These two elements make the ProVerif procedure precise enough to avoid over-approximations that would lead to false attacks. They also aim at improving termination. Details are given is Section 5.2.

Description of the framework

The framework defines two parts: specific processes and generic processes. The first one consists of the elements that describe the protocol under study. They must be defined for each protocol. The second one is fixed and defines how the specific elements are put together yielding the main model that is finally analyzed. For readability, we write in bold and blue the processes and macros specific to the protocol and in orange the generic processes. An overview of the framework is given in Figure 5.

Specific processes and macros

The framework builds upon 12 processes that describe the protocol under study. We distinguish standard processes and macros that do not contain input/output commands and return a term. These are processes defined with the keyword letfun in the ProVerif syntax.

Setup. In the model, each voter is assigned a natural number, called voter index, denoted v idx . Given an index, a process Gen_Voter_Ident describes how to generate a corresponding public identifier. Typically, it may correspond to the voter index itself for simple protocols or another public credential (e.g. a public signing key). A macro gen_voter_data returns the initial knowledge (prior to the registration) corresponding to a given voter index. Finally, a process Gen_Voting_Data describes how a voter receives their voting data. It takes as input, an election identifier, a voter index, and their corresponding initial knowledge and inserts in a table voting_data the voting data received by the voter in order to vote. Note that the set of candidates V is not part of this data and is instead defined by a macro is_valid(v) which returns true if and only if v ∈ V.

Voting Phase. A process Voting describes how a voter votes. In general, this process should contain the voted event. Similarly, a process Final_Check describes what the voter is expected to do after having cast their last ballot. It typically models what a voter should do to verify their vote, and thus contain the verified event. gbl(e id ) := update_gbl(B,gbl,. . . ) cell(e id , ident) := update_ballot(B, cell(e id , ident),gbl(e id ),. . . )

if is_valid_ballot(B, cell(e id , ident), gbl(e id ),. . . )

Process Tally(e id )

Process Decrypt_Ballot

output v emit counted(e id , v) vote v
For each ident, cell(e id , ident) given to Initialize Tally in blue: parts to be defined specifically for each voting protocol Bulletin board. Two macros update_gbl and update_ballot describe how the (public or private) bulletin board evolves. More precisely, the bulletin board maintains a global memory cell gbl(e id ) as well as one memory cell cell(ident) for each voter identifier ident generated by Gen_Voter_Ident. Additionally, we assume a table ballot_box(e id ) that contains data (e.g. ballots) cast for publication onto the bulletin board in election e id . Each time a valid entry (as defined by the Boolean macro is_valid_ballot) of this table is processed, the macro update_gbl is executed to update the value of the memory cell gbl(e id ). Moreover, after retrieving a voter identifier ident from the entry us-ing the macro get_ident_from_ballot, the macro update_ballot updates the memory cell cell(ident).

Tally. The process Decrypt_Ballot describes how ballots are decrypted during the tally phase. For the sake of simplicity, our framework allows to model protocols based on mixnets for tally only.

Main process. Finally, the main process FinalSystem defines the scenarios under study. This process builds upon the System(e id) process provided by the framework to model an election. For sake of generality, it is possible to define other protocol specific processes to faithfully model the peculiarities of each protocol.

Example 5. We illustrate our framework with the He-lios protocol described in Example 1 and Figure 2. Most of the macros and processes are very simple to define: Decrypt_Ballot simply decrypts the ballot as expected, is_valid_ballot(b) checks that b is not an empty ballot, update_ballot returns the accepted ballot and update_gbl returns a dummy constant since there is no global data to be updated in the protocol. The precise definitions are given in Appendix C.

The process Gen_Voter_Ident takes as input the election identifier and a voter index, and outputs the a freshly generated pseudonym on a framework specific channel res_GVI(e id, v idx), i.e.

1 let Gen_Voter_Ident(e_id,v_idx) = 2 new pseudo; out(res_GVI(e_id,v_idx),pseudo).

In our toy example, the voter registration is abstracted. We consider that the authenticated channel used by the voter to cast a ballot is part of their initial knowledge. Therefore, the macro gen_voter_data generates the authenticated channel c auth which is forwarded to the voter by the process Gen_Voting_Data through the table voting_data. The macro also retrieves the pseudonym that was generated by Gen_Voter_Ident from the table public_identifier. Moreover, an event Link_Idx_Ident(e id , v idx, pseudo) is executed to store the relationship between the voter index and its corresponding identifier. This event will be useful to help ProVerif proofs as explained in Section 5.2. Regarding the voting phase, the processes Voting and Final_Check roughly correspond to the process Voter described in Example 1. Voting models how the voter forges a ballot, i.e.: This process exactly corresponds to the first part of the process Voter up to the use of an election identifier and an output on the framework specific channel res_voting(e id, v idx, nb vote). We can note that nb vote is a natural integer used to count how many times the voter voted. This information is particularly relevant to model protocols allowing re-votes.

In our model, the voter verifies their last vote only. The check is thus modeled by the Final_Check process which defines actions that the voter is expected to do once their last vote has been cast. In the context of Helios, this corresponds to the verification step in which the voter reads onto the bulletin board and checks that their ballot appears as expected. This process takes as argument the same elements as the voting process plus the last cast ballot. Finally, we end the modeling of Helios by defining the scenarios under study. The process FinalSystem models multiple elections, each using an encryption key chosen by the attacker (decryption authorities are supposed compromised). It calls the generic process System(e_id) defined by our framework and may also consider additional processes. In Helios, the process Server inserts in the table ballot_box the ballots it received on the authenticated channels shared with the voters. For more complex protocols, the Server may also model how to establish such an authenticated channel from the initial data.

Generic processes

In order to put together the protocol specific macros and processes, the framework defines different generic processes. Because the understanding of them is not a requirement to use the framework, we just present an excerpt of these processes.

Voter process. The role of a voter is modeled by a Voter process which mainly builds upon the protocol specific processes Voting and Final_Check. The process is very similar to the one presented in Example 1: it receives from the attacker the name of the candidate the voter is going to vote for. Then it executes the Voting process to cast a ballot and, if it is the last vote, executes the Final_Check process too. However, the reader can note that these actions are guarded by a communication on the private channel cell voter(e id, v idx): an input is executed before executing the voting process and an output is executed right after if the vote is not the last. Based on the semantics of communications on private channels, this allows to prevent concurrent voter sessions executions. Hence, it allows to count (by increasing the variable nb vote) the number of (re)votes by voters. Concretely, the process is as follows: Tally process. In the framework, the tally is closely related to the generation of the voter identifiers. Indeed, in order to guarantee that the finish(e id) event is executed once all the ballots have been tallied, we proceed as follows: during the setup of the election, the framework counts the number of voter identifiers that are generated. Then, the tally executes the event finish(e id) once one (possibly empty) ballot is tallied for each of them. Technically, it relies on the use of a private channel cell ident(e id) that contains a counter which is incremented each time a new identifier is generated (process Pub_Voter_Ident_Generation).

1 let Voter(e_id) = 2 in(c_pub,v); 3 if is_valid(v)
At some point, this generation of identifiers is stopped (process Stop_Pub_Voter_Ident_Generation) and the current value on the channel is transferred to another private channel cell tally(e id) whose value will be decremented by 1 each time a ballot is tallied. Concretely, these two first processes are as follows: We can note that the voter identifier associated to each counter value is recorded with the event Public_identifier(e id, i + 1, ident). Finally, the number of generated public identifiers is stored in the event Nb_identifier(e id, i) (see Section 5.2 for usage).

1 let Pub_Voter_Ident_Generation(e_id) = 2
We can now model the tally through the two following processes: Init_Tally collects the last ballot for each voter identifier and stores them in specific private channels read by Tally to compute the tally. The Tally process is very similar to the process described in Figure 2. It relies on the cell cell tally(e id) to count the number of tallied ballots and execute the finish(e id) event at the right place. Note that the events T ally Read(e id, i) and CountedExtended(e id, v, i, ident) are new annotations that will be useful to help ProVerif proofs. Their usage is commented in the next section.

Improving ProVerif accuracy

Unsurprisingly, our first experiments have shown that ProVerif was not able to prove the security of even simple protocols when using this complex framework. To overcome this limitation of the tool, we extended our framework with well chosen axioms and lemmas. All of them are protocol independent and can thus be reused to analyze a new protocol without any modification.

GSVerif-like annotations

The first difficulty for ProVerif lies in the manipulation of cells and counters. Indeed, some of ProVerif proof strategies lead to dramatic over-approximations in this context. In 2018, Cheval et. al. proposed the tool GSVerif [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF] to overcome these limitations. Based on events, it adds formally proven correct axioms to improve ProVerif accuracy.

Unfortunately, our framework is too complex and GSVerif cannot be used to automatically annotate the processes and add the relevant axioms. Therefore, we decided to manually place those events and gather in the ProVerif library gsverif_library.pvl all the GSVerif-like axioms that are being used. Interestingly, because of the complexity of our framework, we needed to extend GSVerif approach by defining new events and related axioms, as described below.

Counter intervals: Let's consider a cell (i.e. a channel used as a cell) that manipulates an increasing counter, but where steps may be greater than 1, i.e. the counter may increase by n > 1. This may typically happen when manipulating cells containing global data and cells containing data specific to an identifier. In our generic framework, both rely on linked counters: if the counter associated to the global data always increases by 1, the one of the specific identifier may increase by greater steps (it is not updated for each accepted ballot). In this case, it is important to reflect that intermediate values cannot appear in the cell. To do so, we define a new event CounterInterval(c, i, j) executed each time the counter of the cell c, whose current value is i, is incremented to j (j > i). We also consider a new event CounterInterval(c, k) executed each time the value k is read on the cell c. We can then define the following axioms:

1 axiom c:channel, i,j,k:nat; We can easily convince ourselves of the validity of the axiom in two steps. First, we can check that we placed such events only when the underlying channel is a cell in the sense of GSVerif, hence we know from [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF] that the Its correctness follows directly from the fact that values inside an interval are skipped. Of course, these are excerpts of the axioms that can be defined following the same approach. A complete description of them is provided in the GSVerif library accompanying the framework.

Term freshness: An other source of inaccuracy lies in the fact that ProVerif is not able to detect that a message must be fresh enough to be input at some points of the protocol. Figure 6 presents a minimal process and a simple query that ProVerif cannot prove satisfied. To overcome this limitation, we define the following events and axiom: the event T ermF reshlyCreated(c, i, x) is executed when the message x is created (that contains a nonce) and the current value of the cell c is i, the event T ermReceived(c, j, y) is executed each time the message y is received and the current value of the cell c is j. The following axiom is defined:

1 axiom c:channel, i,j:nat, x,y:bitstring; 2 event(TermFreshlyCreated(c,i,x)) && is_subterm(x,y) 3

&& event(TermReceived(c,j,y)

) =⇒ i < j.
where is subterm(x, y) is a predicate evaluated to true when x is a subterm of y. These events and axiom are generic and can be used anywhere in the process to emphasize the need of freshness. The correctness of the axiom follows from the fact that the nonce used in x cannot appear in a term y before its creation. Our axioms are only informally justified. As future work, we plan to characterize more generally in the GSVerif setting where the corresponding events can be placed and then prove the axioms to be correct (which typically follows easily from the characterization). Our axioms could thus be added in a future version of the tool.

Prove intermediate lemmas

In addition to axioms, ProVerif supports the definition of lemmas, i.e. queries that will be proved before the analysis of the main query and then internally used to guide the analysis. In our framework, we provide several generic lemmas that should be satisfied by our generic processes or the protocol under study. These are gathered in a unique ProVerif library, properties.pvl. We provide here an overview of these lemmas.

Simple lemmas: First, lemmas are used to emphasize simple properties such as: the value of the counter in the cell cell pub id(e id ) is a natural number and smaller than the value recorded in the event N umber V oter Id(e id , i). This is formally defined by the following lemma:

1 lemma e_id:election_id, x:bitstring, i,j:nat; 2 mess(cell_ident(e_id),i) =⇒ is_nat(i); 3 event Nb_identifier(e_id,i))

4
&& mess(cell_ident(e_id),j) =⇒ j <= i.

In our framework, different simple events like this one are defined. For instance, this lemma holds for the cell cell tally(e id) too.

Assumption lemmas: As presented in Section 4.1, a few assumptions on the protocol under study must be verified to apply Theorem 1. They are thus defined as lemmas in our framework and automatically proved satisfied by ProVerif before starting the analysis of the main queries.

Moreover, even if our framework has been designed to be as generic as possible, we found that an extra protocol assumption was needed to make ProVerif prove: all the verified events are executed by legitimate voters. Hopefully, this assumption should be satisfied by any reasonable protocol. Concretely, the following lemma is defined and proved by ProVerif before starting the security analysis:

1 lemma e_id:election_id, ident:voter_ident, v_idx:nat; 2 event(verified(e_id,v_idx,v)) 3

=⇒ event(Link_Idx_Ident(e_id,v_idx,ident)).

Induction lemma: Finally, our framework contains lemmas which specify useful induction invariants to make the proof. For instance, regarding the Tally process presented in Section 5.1, we can explicit the following invariant: given an index i 1 and its corresponding identifier ident, if ident has been associated to a voter, v idx, who is expected to verify, then either the tally process has not reached the ballot corresponding to ident yet (i.e. i 1 ≥ i 2), or there is a Counted event which corresponds to the intended vote of the voter. One can note that the event CountedExtended is used to strengthen the property. Moreover, the events Link_Idx_Ident and Public_identifier link the voter index to an index manipulated by the tally process. Indeed, even if both are associated to the same public voter identifier ident these associations are defined at two different steps of the protocol: Link_Idx_Ident should be executed during the registration the voter, while Public_identifier is executed in the process Pub Voter Ident Generation, i.e. during the initialization of the bulletin board. The framework does not guarantee that a public voter identifier is bound to the same (voter) index in both cases.

Case studies

We apply our framework to prove verifiability of several voting protocols. The first one is our running example, Helios, in a simple form. We then study the security of Belenios, a protocol that inherits a lot of structure from Helios. To show the applicability of our framework, we consider two complex protocols, namely the Swiss-Post voting protocol [1] and the CHVote protocol [START_REF] Haenni | CHVote system specification[END_REF], developed to comply with the demanding Swiss regulations. We started from existing ProVerif models, as written by their respective authors, and showed that they can be directly imported into our framework in order to prove E2E-verifiability.

In these previous models, only individual verifiability was proven, with external justifications (on paper). Since we now prove E2E-verifiability, we had to model the tally process for each of these protocols (with some abstraction regarding the cryptographic primitives), yielding a more complete model. All these protocols could be automatically proved with ProVerif using our framework, without any modification. Only one variant of Belenios required to manually write specific lemmas, due to the recursive nature of this protocol that makes use of chains of hashes.

Helios

We first studied the Helios protocol as presented in running example. As a proof of concept, we decided to propose a simple model. As a consequence, we do not model the audit mechanism and assume an honest voting device instead. Thanks to our framework, we prove the security of Helios as expected: Helios ensures E2E-verifiability as soon as the server is honest. Otherwise, a malicious server could impersonate any voter and vote on their behalf which defeats E2E-verifiability.

Belenios

Belenios is an improvement of Helios in which voters are provided with a private signing key used to authenticate the senders of the ballots and created by a registrar. This new feature allows to obtain E2E-verifiability when either the registrar or the server is honest; the trust is shared between those two agents.

An implicit assumption in this analysis (same for Helios) is that the voter verifies the presence of their ballot onto the bulletin board after the election is over. This is what we call Belenios tally. As suggested in [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF], we also explore a more realistic assumption: voters verify their last ballot during the voting phase, i.e. just after they cast their vote. We call this Belenios last. In this context, Belenios (as Helios) fails to ensure E2E-verifiability. Indeed, if a voter first casts a ballot b 1 , then a ballot b 2 , and checks that b 2 is in the ballot box, a malicious server may re-cast the first ballot b 1 . We thus consider a variant of Belenios, called Belenios-hash last, where ballots are chained: each ballot contains the hash of a preceding ballot. This solution was suggested in [START_REF] Baloglu | Provably Improving Election Verifiability in Belenios[END_REF] and has been further simplified by Belenios authors [START_REF] Cortier | [END_REF] for efficiency reasons. Interestingly, the first simplification by Belenios authors was a version with counters, called Belenios-counter last, that our approach proved to be flawed.

We applied our framework to prove the E2E-verifiability of the different versions of Belenios. We confirmed the expected security guarantees and the applicability of our framework. Only Belenios-hash required to write manually three main lemmas. The most technical one intuitively says that whenever two ballots from the same voter appear on the bulletin board then the hash of the first submitted ballot must be contained in the second ballot. The need of this lemma is due to the intrinsic difficulty of the analysis by ProVerif of a chain of hashes and is orthogonal to our framework.

Swiss Post protocol

The Swiss Post protocol [1] is developed for more than 5 years and was initially designed by Scytl. It is planned to be deployed in several cantons in 2023. The protocol relies on a setup component, whose purpose is to generate and broadcast the voting material to voters. Its role can be compared with the role of the registrar in the Belenios protocol. It assumes four control components (CCR and CCM) to process ballots during the voting phase. One of them is honest to ensure verifiability (and vote secrecy). Their role is similar to the role of the server in Helios or Belenios protocols2 . One challenge of the voting protocols designed for the Swiss context is that they need to offer a cast-as-intended mechanism based on return codes. Before the voting phase, each voter receives a voting sheet with some authentication material as well as return codes, one for each voting choice. During the voting phase, a voter selects their choice(s) for each question, using their voting device. They then receive a code for each selection and check that it matches the code on their voting sheet. Only once they agree with all the received codes, they send their final confirmation code. This protects against a malicious voting device that may try to modify their vote. Formally, E2E-verifiability has to hold even if the voting device is compromised. Of course, the voting server should not learn how a voter voted. Hence the return codes are computed by the four control components so that the vote remains hidden, involving non trivial cryptographic primitives.

In order to comply with the demanding Swiss regulation [START_REF] Confederation | Technical and administrative requirements for electronic vote casting[END_REF], ProVerif models have been developed over the years to prove both verifiability and privacy. These are complex models (about 500 lines of code), with ad-hoc equational theories. We imported the last available model [START_REF]Symbolic analysis of the swiss post voting system[END_REF] in our framework and proved E2E-verifiability immediately 3 .

CHVote

Another protocol, CHVote [START_REF] Haenni | CHVote system specification[END_REF], is designed since 2017 to also comply with the Swiss voting requirements. Therefore, it also includes a cast-as-intended mechanism with return codes. In CHVote, the control components jointly compute the return codes during the voting phase using oblivious transfer. CHVote has been supported by the Canton of Geneva during several years but is currently not considered for deployment for budget reasons. However, in order to comply with the obligation to provide computational and symbolic proofs, ProVerif models have been developed [START_REF] Bernhard | Verifiability analysis of chvote[END_REF]. We imported these models in our framework and we again proved E2E-verifiability immediately.

Our findings are summarized in Table 1. All models are available as supplementary material in [START_REF] Cheval | Election Verifiability with ProVerif[END_REF]. They could easily be proved in ProVerif using the latest development branch improved_scope_lemma 4 that is about to be merged in the branch master 5 . For all the voting protocols, our two queries could automatically be proved by ProVerif, thanks to our library of lemmas and axioms, with the exception of Belenios-hash last that required a couple of manual lemmas, as explained above. assumptions for our characterization of E2E-verifiability have been written once for all in our library of lemmas and are easily proved by ProVerif, as expected. The benchmark have been obtained on a laptop Intel quad-core i7, 2.3 GHz, 32Go RAM.

Voter

Registrar Server E2E (setup) (1 CCR/M) Verifiability Helios (toy ex.) -16s

Belenios tally 24s

Belenios last 5s

Belenios-counter last 8s

Belenios-hash last 62s

Swiss Post 58s

CHVote 17s

= honest = dishonest TABLE 1: Results of the security analyses.

3. In this model, the voting device is dishonest, hence not modeled. 4. https://gitlab.inria.fr/bblanche/proverif/-/tree/improved scope lemma 5. According to personal communications with the developers.

Conclusion

We designed a ProVerif framework to analyze the E2E verifiability of voting protocols based on our characterization of verifiability with two simple injective queries. This framework embeds lemmas to let ProVerif automatically check that the protocol satisfies the main assumption of the characterization. Two libraries of generic lemmas and axioms, designed in the spirit of the GSVerif tool, are included in the framework to improve ProVerif accuracy. Finally, this framework has been successfully applied to several protocols of the literature. It has been filled using existing ProVerif models of these protocols.

Our characterization holds for counting functions that are equivalent to the multiset of votes, which already covers most of the elections. Interestingly, for alternative counting functions (e.g. Condorcet, Single Transferable Vote, d'Hondt method), our two queries still imply E2E-verifiability, hence they can be use to prove E2E-verifiability with ProVerif. However, the converse implication does not hold: these two queries may be too strong in general. Writing tight queries in the general case is left as future work.

We have written our generic framework with the goal of being as general as possible, hoping that other voting systems will be cast in our framework in the future, in order to prove verifiability. It would be interesting to also be able to prove vote secrecy with the same framework. The tally phase needs to be reworked to model the fact that ballots are mixed before been decrypted. Moreover, since vote secrecy is modeled as an equivalence property, this will certainly create new challenges for ProVerif proofs.

Figure 1 :

 1 Figure 1: Syntax of ProVerif (excerpt).

Figure 2 :

 2 Figure 2: ProVerif processes of Example 4

  Subset ofResult mapped to HV by f Subset of Result mapped to HNV by f Subset of Result mapped to D by f

Figure 3 :Figure 4 :

 34 Figure 3: Two injective functions f and g.

Figure 5 :

 5 Figure 5: Overview of the framework.

1

  let Voting(e_id,v_idx,nb_vote,v,voting_data) = 2 get election_key(=e_id,_,pkE) in 3 let (pseudo,c_auth) = voting_data in 4 new r_ctxt; 5 let ctxt = aenc(pkE,v,r_ctxt) in 6 event voted(e_id,v_idx,v); 7 let b = (pseudo,ctxt) in 8 out(c_pub, b); out(c_auth, b); 9 10 out(res_voting(e_id,v_idx,nb_vote),b).

1

  let Final_Check(e_id,v_idx,v,voting_data,b,...) = 2 let (pseudo,_) = v_data in 3 in(cell_tally(e_id,pseudo), =b); 4 event verified(e_id,v_idx,v); 5 out(cell_tally(e_id,pseudo), b).

3

 3 && event(CounterValue(c,k)) && i < k =⇒ j <= k; 4 event(CounterInterval(c,i,j)) 5&& event(CounterValue(c,k)) && k < j =⇒ k <= i.

1 let Voter(id,pkE) =

	2	in(c_pub,v);
	3	get voting_data(=id,(pseudo,c_auth)) in
	4	in(cell_voter(id), nb_vote); // Read on cell voter(id)
	5	new r_ctxt;
	6	let ctxt = aenc(pkE,v,r_ctxt) in
	7	event voted(id,v);
	8	let b =(pseudo,ctxt) in // Create the ballot
	9	out(c_pub, b); out(c_auth, b);
	10
	11	in(c_pub, is_verif);
	12	if is_verif then
	13	in(cell_tally(pseudo), =b); // Read and test equality
	14	event verified(

id,v); 15 out(cell_tally(pseudo), b) 16 else out(cell_voter(id),nb_vote+1). /

/ Increment cell voter(id)

  e id , v idx , gen_voter_data(v idx ). . .

	table registered_voters	Setup Phase	Process Gen_Voter_Ident
						insert in
	given to					table public_identifier
	Process Gen_Voting_Data				ident . . .
	insert in					for each ident initializes cell(e id , ident)
	table voting_data				Bulletin Board
	e id , v idx , v data . . .					1 memory cell gbl(e id ) 1 memory cell cell(e id , ident) per identifier ident
			Voting Phase	updated in
	Process Voter		table ballot_box	Process Cleansing
	input v	given to	B 1 B 2	for each	ident = get_ident_from_ballot(B)
	if is_valid(v) then v parameter for		. . .		B
	Process Voting		b given to	insert B
	emit voted(e result b given to	Server processing b into B
	Process Final_Check
			Voting Phase

id , v idx , v)

emit verified(e id , v idx , v)

  Figure 6: Toy example to illustrate ProVerif inaccuracy value of the counter increases strictly. Then, since eventsCounterInterval(c, i, j) are placed in case the values of the counter is skipped from i to j, if the value k of the counter is such that i < k then we must have j ≤ k. The same argument holds for the second axiom. Similarly, we can define the following axiom which states that the intervals cannot overlap:

	1 query x:bitstring, i,j:nat;
	2	event(E(x,i)) && event(F(x,j)) =⇒ i > j.
	3
	4 process
	5	out(cell, 0) | (
	6	! in(cell, x); new n; event F(n,x);
	7	out(cell,x+1) | out(c,n)
	8	) | (
	9	! in(cell, x:nat); in(c, x_n:bitstring);
	10	event E(x_n,x); out(cell, x+1))
	1 axiom c:channel, i,j,k,l:nat;
	2	event(CounterInterval(c,i,j))
	3	&& event(CounterInterval(c,k,l))
	4	&& j <= l	=⇒ (j = l && i = k) || j <= k.

The Swiss framework also considers a server. However, because it is considered untrustworthy, it is omitted in the security analysis.

Appendix A. Proof of the main theorem

We provide the detailed proofs of Lemma 1 and Lemma 2.

Lemma 1. If a voting process P is E2E-verifiable then it satisfies query 1 and query 2.

Proof. Because P is E2E verifiable, we know that for all traces tr of P that contains the event finish, there exist V ′ hnv ⊆ id m V id hnv and V d such that |V d | ≤ |D| and Result = V hv ∪ V ′ hnv ∪ V d P satisfies query 1: Let tr a trace of P that contains the event finish. We are going to define an injective function f : Result → Voters that satisfies query 1.

First, we define

x → id where verified(id, x) ∈ tr is the event corresponding to x in the definition of V hv

Because the events verified(id, •) are executed at most once for each voter id, we know that f | V hv is a bijective function.

Then, because V ′ hnv ⊆ id m V hnv we know that there exists a multiset

hnv and for all (id, v), (id ′ , v ′ ) elements in V id , we have id ̸ = id ′ . We define

We are now able to conclude that the trace tr satisfies query 1 using the function

Indeed, the multisets HV, HNV, D are disjoint by definition and thus f is injective by construction.

P satisfies query 2:

Let tr be a trace of P such that tr contains the event finish. Because P is E2E verifiable, we have that V hv ⊆ m Result. We thus we immediate deduce that we can define an injective function g : HV → Result such that for all verified(id, v) ∈ tr, g(id) = v and counted(v) ∈ tr. Therefore, tr satisfies query 2. Lemma 2. If a voting process P satisfies query 1 and query 2 then it is E2E-verifiable.

Proof. Recall that we see Result as a set of pairs x = (v, i) where v is the value of the vote and i is its index of occurrence in Result. We will note value(x) the vote value v of x.

Recall that we have defined h by h

Case (i) makes sure that h is surjective over HV. Justification of (ii). We need to show that

∈ HV} is well-defined. Assume by contradiction that for all i, (f

Applying once more that f is injective, we have x = (g • f ) j-i (x). Thus x ∈ g(HV) and has already been considered in case (i), contradiction. We conclude that n is well-defined.

h is injective. Let now show that h is injective. Assume by contradiction that this is not the case. Then there exist x, y ∈ Result, x ̸ = y such that h(x) = h(y).

• either x is considered in (i) and y is considered in (ii).

We have

Again, h(x) = g -1 (x) ∈ HV and h(y) = f (y) / ∈ HV, contradiction.

• or x is considered in (ii) and y is considered in (iii).

We have

∈ g(HV). • x and y cannot be both considered in (i) nor in (iii) since g and f are injective. • the last case is when x and y are considered in

and x, y / ∈ g(HV). We can assume i < j.

We can therefore conclude that h is injective.

E2E-verifiability.

Let dom 1 be the (multi)set of x considered in case (i) and dom 2 be the (multi)set of x considered in cases (ii) and (iii). By construction, Im(h| dom1 ) = HV. Moreover, Im(h| dom2 ) ⊆ Im(f )\HV. Hence Im(h| dom2 ) = HNV ′′ ∪ D ′′ with HNV ′′ ⊆ HNV ′ and D ′′ ⊆ D ′ . Hence Im(h) = HV∪HNV ′′ ∪D ′′ with HNV ′′ ⊆ HNV and D ′′ ⊆ D.

Let R 1 = h -1 (HV), R 2 = h -1 (HNV ′′ ), and

We show first that R 1 = V hv : ⊇ Each v ∈ V hv (with its occurrence) can be injectively mapped to id ∈ HV such that verified(id, v) ∈ tr. Thanks to the definitions of g, the multiset of these v is in correspondence with an equal multiset included in g(HV). Since g(HV) = h -1 (HV). we deduce

. By definition of v, there exists id ∈ HV such that h(v) = id = g -1 (v). By definition of g, verified(id, value(v)) ∈ tr and thus v ∈ V hv .

It remains to show that R 2 ⊆ id m V id hnv . We already know that V id ⊆ m V id hnv . Hence we simply need to show that

By definition of g and since verified(f (v), value(v)) ∈ tr, we have value

. By definition of g and since verified(f

By definition, h(v) = id = f (ṽ) and we just showed value(ṽ) = value(v). By definition of f and since id ∈ HNV, we have voted(f (ṽ), value(ṽ)) ∈ tr, that is voted(id, value(v)) ∈ tr, hence (id, value(v)) ∈ V id . This allows us to conclude that R 2 ⊆ id m V id hnv , which concludes the proof of E2E-verifiability.

Appendix B.

Discussion on the sufficient conditions of [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF] We consider the scenario called (V 3 , A 3 ) in [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF]. Under this scenario, Belenios does not satisfy the property called

Intuitively, A 3 is the case where the decryption trustees, some voters, and the registrar are dishonest. The server is honest. V 3 corresponds to the scenario where voters check that their ballots belong to the final board, the one that is tallied. In that case, Belenios does satisfy E2E-verifiability, as proven in our files (see Belenios-tally). Indeed, voters who verify are ensured that their ballots are ready to be tallied, by definition. Moreover, since the server is honest, at most k votes can be added by the adversary, where k is the number of corrupted voters.

However, Belenios does not satisfy Φ • res , hence one cannot conclude that Belenios satisfies MS • E2F , the property closest to our notion of E2E-verifiability. The property Φ • res is defined as

This intuitively says that, whenever a ballot b is published on the bulletin board with credential cr then

• either cr is a credential corresponding to a corrupted voter • or there is a (honest) voter id with credential cr that cast a vote v, where v corresponds to the content of b. [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF] exhibits an attack trace against Φ • res , where the (dishonest) registrar sends a credential cr 1 to an honest voter Alice and also uses this credential to cast a ballot b A using the password of a dishonest voter. Then we obtain BBtally(cr 1 , b A ) while cr 1 is not corrupted and no honest voter cast a vote corresponding to b A . Hence Φ • res is violated. However, this is not an attack against E2E-verifiability since the result of the election would then consist of one dishonest vote, which is fine since the attack assumes at least one dishonest voter. As noticed by the authors of [START_REF] Baloglu | Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios[END_REF], this corresponds to a case where Alice would be prevented to vote since she can no longer use her credential cr 1 . Such a denial of service attack can also happen if the adversary simply stops the communication channel. In any case, Alice would notice an unexpected behavior if she attempts to vote.

More generally, this inconsistency in the results is due to the fact the MS • E2F property is not equivalent to our definition (Definition 1) of E2E-verifiability. Instead of identifying voters by their id, MS • E2F identifies voters by their cred. Unfortunately, two different voters may receive the same credential from a malicious registrar. Hence, identifying voters based on their credential is ambiguous.

Appendix C. Casting Helios in our framework

Continuing Example 5, we define the missing macros and processes.

For sake of generality, the macros update_ballot and update_gbl take as input the following data: e id is the election identifier, cur data is the current data associated to the voter ident, cur gbl data is the current global data, and b the ballot being processed. Moreover, they take as input the whole context of the bulletin board, i.e. nb vote the total number of ballots processed so far, i ident the number of accepted ballots for the given ident, and i gbl the total number of ballots accepted when the last ballot corresponding to ident was processed. All these elements may be useful to decide whether a ballot is valid and define how the data is updated.