Myrto Arapinis

Véronique Cortier

Steve Kremer

When are three voters enough for privacy properties?

Protocols for secure electronic voting are of increasing societal importance. Proving rigorously their security is more challenging than many other protocols, which aim at authentication or key exchange. One of the reasons is that they need to be secure for an arbitrary number of malicious voters. In this paper we identify a class of voting protocols for which only a small number of agents needs to be considered: if there is an attack on vote privacy then there is also an attack that involves at most 3 voters (2 honest voters and 1 dishonest voter). In the case where the protocol allows a voter to cast several votes and counts, e.g., only the last one, we also reduce the number of ballots required for an attack to 10, and under some additional hypotheses, 7 ballots. Our results are formalised and proven in a symbolic model based on the applied pi calculus. We illustrate the applicability of our results on several case studies, including different versions of Helios and Prêt-à-Voter, as well as the JCJ protocol. For some of these protocols we can use the ProVerif tool to provide the first formal proofs of privacy for an unbounded number of voters.

Introduction

Electronic voting has been adopted in several countries, such as the United States, Estonia, Australia, Norway, Switzerland, and France, to conduct legally binding elections (or at least trials for some of them). Electronic voting systems should ensure the same properties than the traditional paper ballots systems, despite the fact that malicious users may easily intercept ballots and try to forge fake ones. One crucial property is vote privacy: no one should know how a particular voter voted. Symbolic models have been very successful in the analysis of more traditional protocols that aim at confidentiality or authentication. Many decision techniques and several tools have been developed (see [START_REF] Blanchet | An efficient cryptographic protocol verifier based on Prolog rules[END_REF][START_REF] Rusinowitch | Protocol insecurity with finite number of sessions is NPcomplete[END_REF][START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF] to cite only a few) which have been successfully applied to a large number of case studies including widely deployed protocols such as TLS [START_REF] Bhargavan | Cryptographically verified implementations for tls[END_REF]. Vote privacy in symbolic models can be expressed through a rather simple and natural property [START_REF] Kremer | Analysis of an electronic voting protocol in the applied picalculus[END_REF]: an attacker should not be able to distinguish the situation where Alice votes 0 and Bob votes 1 from the situation where the votes are swapped:

V Alice (0) | V Bob (1) ≈ V Alice (1) | V Bob (0)
Despite its apparent simplicity, this property is difficult to check for several reasons. Firstly, most existing decision techniques apply to reachability properties (such as authentication and confidentiality) but not to indistinguishability properties. Another major difficulty comes from the fact that e-voting systems involve less standard cryptographic primitives and sometimes even specially designed, ad-hoc primitives (like for the protocol used in Norway [START_REF] Gjøsteen | Analysis of an internet voting protocol[END_REF]). Typical primitives in e-voting are homomorphic encryption, zero-knowledge proofs, reencryption mixnets, etc. Some techniques and tools [START_REF] Blanchet | Automated Verification of Selected Equivalences for Security Protocols[END_REF][START_REF] Tiu | Automating open bisimulation checking for the spi calculus[END_REF][START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF][START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF] for indistinguishability properties have recently been developed to automatically check indistinguishability properties and some of them can handle part of the primitives needed in e-voting. For example, ProVerif and Akiss have both been successfully applied to analyse some voting protocols [START_REF] Kremer | Analysis of an electronic voting protocol in the applied picalculus[END_REF][START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Backes | Automated verification of remote electronic voting protocols in the applied pi-calculus[END_REF][START_REF] Arapinis | Reduction of equational theories for verification of trace equivalence: re-encryption and ac[END_REF][START_REF] Cortier | Attacking and fixing helios: An analysis of ballot secrecy[END_REF][START_REF] Arapinis | Practical Everlasting Privacy[END_REF]. However, a third source of difficulty is the fact that voting systems are typically parametrized by the number of voters: both the bulletin board and the tally processes have to process as many ballots as they receive. This is typically modeled by considering processes parametrized by the number of voters. Even though parameterized protocols can be encoded in a formalism such as the applied pi calculus, such encodings are complicated and generally beyond the capabilities of what automated tools support. ProVerif, which to the best of our knowledge is the only tool that supports verification of indistinguishability properties for an unbounded number of sessions (i.e. allowing replication) generally fails to prove vote privacy. One exception is a case study of the Civitas voting system by Backes et al. [START_REF] Backes | Automated verification of remote electronic voting protocols in the applied pi-calculus[END_REF] using ProVerif. The other tools for indistinguishability (e.g. SPEC [START_REF] Tiu | Automating open bisimulation checking for the spi calculus[END_REF], Akiss [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF], and APTE [START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF]) can only handle a finite number of sessions. So case studies have to consider a finite number of voters [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Arapinis | Reduction of equational theories for verification of trace equivalence: re-encryption and ac[END_REF][START_REF] Cortier | Attacking and fixing helios: An analysis of ballot secrecy[END_REF][START_REF] Arapinis | Practical Everlasting Privacy[END_REF] unless proofs are conducted by hand [START_REF] Cortier | Attacking and fixing helios: An analysis of ballot secrecy[END_REF][START_REF] Cortier | A formal analysis of the norwegian e-voting protocol[END_REF]. Contributions. Our main contribution is a reduction result for a reasonnably large class of voting protocols. If there is an attack on privacy for n voters, we show that there also exists one that only requires 3 voters: 2 honest voters are necessary to state the privacy property and then 1 dishonest is sufficient to find all existing attacks. This result significantly simplifies security proofs: there is no longer need to consider arbitrarily many voters, even in manual proofs. Moreover, this result allows the use of automated tools for checking equivalence properties and justifies previous proofs conducted for a fixed number of voters (provided at least one dishonest voter was considered).

Several protocols assume voters may revote several times. This is for example the case of Helios or Civitas. Revoting is actually crucial for coercion-resistance in Civitas. When revoting is allowed, this should be reflected in the model by letting the ballot box accept an unbounded number of ballots, and retaining only the valid ones according to the revote policy. This aspect is typically abstracted in any existing formal analysis. We show that we can simplify the analysis by reducing the total number of ballots to 10 for typical revoting policies (e.g. the last vote counts) and typical tally functions. Altogether, our result amounts in a finite model property: if there is an attack on privacy on n voters that may vote arbitrarily, then there is an attack that only requires 3 voters and at most 10 ballots. We can further reduce the number of ballots to 7 for a class of protocols that has identifiable ballots, that is ballots that reveal the corresponding public credentials. Of course, only 3 ballots are sufficient when revoting is disallowed.

Our result holds in a rather general setting provided that the e-voting system can be modeled as a process in the applied-pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Of course, this reduction result cannot hold for arbitrary systems. For example, if the tally phase checks that at least 4 ballots are present then at least 4 voters are necessary to conduct an attack. So we model what we think to represent a "reasonable" class of e-voting systems. The process modeling the voter may be an arbitrary process as long as it does not depend on cre-dentials of other voters and provided voters do not need to interact once the tally phase has started. This corresponds to the "vote and go" property, that is often desirable for practical reasons, but also excludes some protocols such as [START_REF] Okamoto | Receipt-free electronic voting schemes for large scale elections[END_REF]. Once the vote is casted the authorities proceed as follows.

-The bulletin board (if there is one) performs only public actions such as publishing a received ballot, possibly removing some parts and possibly after some public tests, i.e. tests that anyone could do as well. Typical public tests are checks of signature validity, well-formedness of the ballots, or validity of zero-knowledge proofs. Alternatively, we may consider an arbitrary bulletin board in case it is corrupted since it is then part of the adversarial environment. -Next, a revote policy is applied. We consider two particular revote policies: the policy which selects the last ballot, which is the most common one, and the policy that selects the first one, which encodes the situation where revoting is prohibited. -Finally, the tally is computed according to some counting function. We consider in particular two very common functions: the multiset and the additive counting functions. The multiset counting function returns the votes in an arbitrary order and corresponds for example to the output of a decryption mixnet. The additive counting function returns the number of votes received by each candidate.

We believe that these conditions are general enough to capture many existing evoting schemes.

Applications. To illustrate the applicability of our result, we re-investigate several existing analyses of e-voting protocols. First, we consider several versions of the Helios protocol [START_REF] Adida | Helios: web-based open-audit voting[END_REF], both in its mixnet and homomorphic versions. These versions also include the Belenios [START_REF] Cortier | Election verifiability for helios under weaker trust assumptions[END_REF] protocol. We are able to use the ProVerif tool to show privacy for the mixnet versions of these protocols for a bounded number of voters and ballots. Our reduction result allows immediately to conclude that vote privacy also holds for an arbitrary number of voters. The homomorphic version of Helios is out of reach of existing tools due to the presence of associative and commutative symbols. However, our reduction result does apply, which means that the manual proof of Helios conducted in [START_REF] Cortier | Attacking and fixing helios: An analysis of ballot secrecy[END_REF] did not need to consider arbitrarily many voters and could be simplified. In case one wishes to adapt this proof to Belenios [START_REF] Cortier | Election verifiability for helios under weaker trust assumptions[END_REF], our reduction result would alleviate the proof. The Prêt-à-Voter [START_REF] Ryan | Prêt-à-voter with re-encryption mixes[END_REF] protocol (PaV) has been analysed using ProVerif for 2 honest voters [START_REF] Arapinis | Reduction of equational theories for verification of trace equivalence: re-encryption and ac[END_REF]. Adding a third, dishonest, voter, we can apply our result and obtain the first proof of vote privacy for an arbitrary number of voters. Unfortunately, ProVerif did not scale up to verify automatically the protocol in presence of a dishonest voter. We were also able to apply our result (and a proof using ProVerif) to a protocol by Moran and Naor and to the JCJ protocol implemented in Civitas (without a ProVerif proof).

Related work. To our knowledge, the only other reduction result applying to voting protocols was proposed by Dreier et al. [START_REF] Dreier | Defining privacy for weighted votes, single and multi-voter coercion[END_REF]. Their result states that it is sufficient to prove vote privacy for two honest voters when the protocol is observationally equivalent to a protocol consisting of the parallel composition (not sharing any secret) of a partition of the set of voters. Applicability has however only been shown to examples where this trivially holds, e.g. [START_REF] Okamoto | Receipt-free electronic voting schemes for large scale elections[END_REF][START_REF] Fujioka | A practical secret voting scheme for large scale elections[END_REF] as these protocols use completely public tallying mechanisms. In general, proving the required equivalence does not seem easier than proving directly vote secrecy. Moreover, it does not apply to some well known protocols such as Helios since a dishonest voter is needed to mount the vote replay attack [START_REF] Cortier | Attacking and fixing helios: An analysis of ballot secrecy[END_REF].

The results of [START_REF] Comon-Lundh | Security properties: two agents are sufficient[END_REF][START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF] show how to reduce the number of agents, in the case of trace properties [START_REF] Comon-Lundh | Security properties: two agents are sufficient[END_REF] and equivalence properties [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF]. The major difference with our work is that [START_REF] Comon-Lundh | Security properties: two agents are sufficient[END_REF][START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF] simply reduce the number of agent identities while the number of sessions (or processes) remains the same. In contrast, we do not only reduce the number of voter identities but also the number of ballots the ballot box needs to process, yielding a simpler process.

Modelling security protocols

As usual in symbolic protocol analysis we model protocol messages as terms. Protocols are modelled in a process calculus, similar to the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF].

Messages

We assume an infinite set of names N = {a, b, k, n, . . .} (which are used to represent keys, nonces, . . . ) and an infinite set of channels Ch = {c, c 1 , ch, ch 1 , . . .} (which are used to represent communication channels). We also consider a set of variables X = {x, y, . . .}, and a signature Σ consisting of a finite set of function symbols.

Terms are defined as names, variables, and function symbols applied to other terms. In particular, a channel is not a term. Let N ⊆ N and X ⊆ X , the set of terms built from N and X by applying function symbols in Σ is denoted by T (Σ, N ∪ X). We write fv (t) (resp. fn(t)) for the set of variables (resp. names) occurring in a term t. A term is ground if it does not contain any variable.

Example 1. We model asymmetric encryption, signatures, and pairs by the signature

Σaenc def = {aenc/3, adec/2, pk/1, sig/2, checksig/2, getmsg/1, vk/1, •, • /2, π1/1, π2/1}
where f /i denotes that f has arity i. Consider term t def = pk(sk), aenc(pk(sk), r, m) where sk, r, m ∈ N . The term t represents a pair consisting of the public key pk(sk) associated to the private key sk and the encryption of message m with public key pk(sk) using randomness r. To improve readability, we may sometimes write t 1 , . . . , t n instead of t 1 , . . . t n-1 , t n . . . . We denote by = [t 1 , . . . , t n ] the list of terms t 1 , . . . , t n and by t 0 :: the list obtained by adding the term t 0 to the head of the list, i.e., t 0 :: = [t 0 , t 1 , . . . , t n ]. Sometimes we interpret lists as multisets and we write 1 = # 2 for the equality of the multisets corresponding to these lists.

A substitution is a partial function from variables to terms. The substitution σ that maps

x i to t i (1 ≤ i ≤ n) is denoted {x 1 → t 1 , . . . , x n → t n }
and we write dom(σ) = {x 1 , . . . , x n } for the domain of σ. We denote by ∅ the substitution whose domain is empty. We always suppose that substitutions are acyclic. As usual we extend substitutions to terms and write tσ for the application of σ to term t.

To model algebraic properties of cryptographic primitives, we define an equational theory by a finite set E of equations u = v with u, v ∈ T (Σ, X ). We define = E to be the smallest equivalence relation on terms, that contains E and that is closed under application of function symbols and substitutions of terms for variables.

Example 2. Continuing Example 1 we define the equational theory E aenc by the following equations.

adec(x k , aenc(pk(x k ), x r , x m )) = x m checksig(sig(x, y), vk(y)) = ok π i ( x 1 , x 2 ) = x i (i ∈ {1, 2}) getmsg(sig(x, y)) = x
Then we have that adec(sk, π 2 (t)) = Eaenc m.

To illustrate our calculus we consider the Helios e-voting protocol as running example. The Helios protocol relies on zero knowledge proofs. We next specify the equational theory for the particular zero knowledge proofs built by the Helios participants.

Example 3. The Helios zero knowledge proofs can be modelled by the signature

Σ zkp def = {zkp E /3, checkzkp E /2, okzkp E /0} ∪ {zkp m DM /3, checkzkp m DM /3, okzkp m DM /0} m∈N
In case of homomorphic tally, the voters should also prove that their vote is valid, which can be modeled in a similar way. When submitting an encrypted vote, voters are required to prove that the encryption is well-formed, that is to say, that they know the corresponding plaintext and randomness. This is reflected by the following equation. In the decryption mixnets-based variant of the Helios protocol, the talliers output a zero knowledge proof of correct mix and decryption. Such a proof establishes that the output of the decryption mixnet is indeed a permutation of the content of the encrypted ballots received as input. This is captured by the following infinite set of equations. For all m ∈ N, and all {i 1 , . . . , i m } = {1, . . . , m},

checkzkp m DM (zkp m DM (xk, xciph, xplain), xciph, xplain) = okzkp m DM with xciph = (aenc(pub(xk), xr 1 , xv 1 ), . . . , aenc(pub(xk), xr m , xv m )) and xplain = (xv i1 , . . . , xv im ).
In all the examples of this section, we will consider the signature Σ = Σ aenc ∪ Σ zkp and the equational theory

E = E aenc ∪ E zkp .
We say that a symbol + is associative and commutative (AC in short) w.r.t. an equational theory E if E contains the two equations:

x + y = y + x x + (y + z) = (x + y) + z 2.

Processes

We model protocols using a process calculus. Our plain processes are similar to plain processes in applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] and are defined through the grammar given in Figure 1 where c is a channel, t, t 1 , t 2 are terms, x is a variable, n is either a name or a channel, and i ∈ N is an integer. The terms t, t 1 , t 2 may contain variables. The process 0 does nothing. P | Q behaves as the parallel execution of processes P and Q. νn.P restricts the scope of n. When n is a name, it typically represents a freshly

P, Q := 0 P | Q νn.P !P if t 1 = t 2 then P else Q c(x).P c t .Q i : P Fig. 1.
Syntax of plain processes generated, secret value, e.g., a key or a nonce, in P . When n is a channel, it declares a private channel, that cannot be accessed by the adversary. Replication !P behaves as an unbounded number of copies of P . The conditional if t 1 = t 2 then P else Q behaves as P if t 1 and t 2 are equal in the equational theory and as Q otherwise.

The process c(x).P inputs a message t on channel c, binds it to x and then behaves as P where x has been replaced by t. c t .Q outputs message t on channel c before behaving as Q. Our calculus also introduces a phase instruction, in the spirit of [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF][START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF], denoted i : P . We denote by Phase(P ) the set of phases that appears in P , that is the set of j such that j : Q occurs in P . By a slight abuse of notations, we write Phase(P ) < Phase(Q) if any phase in Phase(P ) is smaller than any phase in Phase(Q).

As usual, names and variables have scopes, which are delimited by restrictions and inputs. We write fv (P ), bv (P ), fn(P ) and bn(P ) for the sets of free and bound variables, and free and bound names of a plain process P respectively. Example 4. A voter in Helios proceeds as follows. She computes her ballot by encrypting her vote with the public key pk(skE) of the election. The corresponding secret key is shared among several election authorities, which is not modeled here. Then she casts her ballot together with her identity and a zero knowledge proof through an authenticated channel. All this information will be published on a public bulletin board. The process V (pk(skE), cred, id, v) models the actions of a voter with identity id and credential cred casting a ballot for candidate v:

V (pk(skE), cred, id, v) def = νr. bb id, sig(bal, cred), prf
where bal = aenc(pk(skE), r, v) and prf = zkp E (r, v, bal). The authenticated channel is modelled by a signature although Helios relies on a login/password mechanism.

Extended processes keep track of additional information during an execution: the names that have been bound, the currently active processes that are running in parallel, the history of messages that were output by the process and the current phase.

Definition 1 (Extended process). An extended process is a tuple (E; P; Φ; i) where:

-E is a set of names and channels that are restricted in P and Φ; -P is a multiset of plain processes with fv (P) = ∅; -Φ = {x 1 → u 1 , . . . , x n → u n } is a ground substitution where u 1 , . . . , u n represent the messages previously output to the environment. i is an integer denoting the current phase.

Example 5. The following extended process models two honest Helios voters id A and id B ready to cast their ballots v A and v B respectively in a first phase, and the Helios tallying authorities T al ready to tally the cast ballots in a second phase

Helios(v A , v B ) def = (E 0 , 1 : V A | 1 : V B | 2 : T al, ∅, 1)
where E 0 is a set of names with cred A , cred B ∈ E 0 ,

V A def = V (pk(skE), cred A , id A , v A ) and V B def = V (pk(skE), cred B , id B , v B )
model the two honest voters where V is defined in Example 4, and

T al def = bb(xb A ).bb(xb B ).T
for some process T modelling the tallying authorities.

Given A = (E; P; Φ; i), we define the set of free and bound names of A as fn(A) = (fn(P) ∪ fn(Φ)) E, and bn(A) = bn(P) ∪ E. Similarly free and bound variables are defined as fv (A) = (fv (P) ∪ dom(Φ)), and bv (A) = bv (P). An extended process A is closed if fv (A) = dom(Φ).

The operational semantics of our calculus is defined by a labelled transition system which allows to reason about processes that interact with their environment. The transition relation A -→ B relates two ground extended processes A and B and is decorated by a label , which is either an input (c(M )), an output (νx.c x ), or a silent action (τ ). Silent actions are standard, while visible input and output actions are interactions with the adversary on public channels. An output label νx.c x reflects that messages are output "by reference": the label contains the variable added to dom(Φ) which maps to the ground message that was output. The input label c(M ) contains the term M used by the adversary to compute the message: M may be constructed from previous outputs (adressed through variables in dom(Φ)), but is not allowed to use private names. The transition relation is formally defined in the companion technical report [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF]. Notations. Given a set S we denote by S * the set of all finite sequences of elements in S. We may also write ũ for the finite sequence u 1 , . . . , u n . Let A be the alphabet of actions (in our case this alphabet is infinite and contains the special symbol τ ). For every w ∈ A * , the relation w -→ on processes is defined in the usual way, i.e., we write

A w -→ A when w = 1 2 • • • n and A 1 -→ A 1 2 -→ . . . n -→ A . For s ∈ (A {τ }) * ,
Helios(v A , v B ) νy A .bb y A = ====== ⇒ νy B .bb y B = ====== ⇒ phase 2 = === ⇒ (E; T ; Φ; 2)
where

-E = E 0 ∪ {r A , r B }, -Φ = {y A → id A , sig(bal A , cred A ), prf A , y B → id B , sig(bal B , cred B ), prf B } where bal C = aenc(pk(skE), r C , v C ) and prf C = zkp E (r C , v C , bal C ) for C ∈ {A, B}.
A frame ϕ = νE.Φ consists of a set of names E and a substitution Φ = {x 1 → u 1 , . . . , x n → u n }. The names E are bound in ϕ and can be α-converted. Moreover names can be added (or removed) to (from) E as long as they do not appear in Φ. We write ϕ = α ϕ when frames ϕ and ϕ are equal up to α-conversion and addition/removal of unused names. In this way two frames can always be rewritten to have the same set of bound names. When A = (E; P; Φ; i) is an extended process, we define φ(A)

def = νE.Φ.
Given a frame ϕ = νE.Φ an attacker can construct new terms building on the terms exposed by ϕ. For this the attacker applies a recipe on the frame. A recipe R for a frame ϕ is any term such that fn(R) ∩ E = ∅ and fv (R) ⊆ dom(Φ). An attacker is unable to distinguish two sequences of messages if he cannot construct a test that distinguishes them. This notion is formally captured by static equivalence [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] of frames. Definition 2 (Static equivalence). Two frames ϕ 1 = α νE.Φ 1 and ϕ 2 = α νE.Φ 2 are statically equivalent, noted ϕ 1 ∼ ϕ 2 when dom(Φ 1 ) = dom(Φ 2 ), and for all recipes M and N of ϕ 1 we have that

M Φ 1 = E N Φ 1 iff M Φ 2 = E N Φ 2 .
Note that in the above definition the frames ϕ 1 and ϕ 2 have the same set of recipes as they bind the same names E and their substitutions have the same domain. Example 7. Let Φ be the substitution of Example 6 and Indeed, an attacker may distinguish between these two frames as soon as he has the secret key skE, by simply decrypting the ballots.

Φ = {y A → id A , sig(bal A , cred A ), prf A , y B → id B , sig(bal B , cred B ),
Given two extended processes A 1 and A 2 , we often write A 1 ∼ A 2 for φ(A 1 ) ∼ φ(A 2 ). Given an extended process A we define its set of traces as

traces(A) def = {(tr, B) | A tr = ⇒ B}
We can now define what it means for an attacker to be unable to distinguish two processes even if he is allowed to actively interact with them. This notion of indistinguishability is naturally modelled by trace equivalence. Intuitively, as the sequence of visible actions in the labels encode the adversary's actions the definition requires that for the same interaction with the adversary the protocols produce indistinguishable outputs.

In this section we explain how we formally model e-voting protocols and state the assumptions needed for our results.

Since many e-voting protocols use zero-knowledge proofs, we consider a signature Σ with zkp, checkzkp, okzkp ∈ Σ and we assume an equational theory that can be described by an AC-convergent (possibly infinite) rewrite theory such that the only rules in which zkp, checkzkp, and okzkp occur, are of the form:

checkzkp(zkp(U 1 , . . . , U m ), V 1 , . . . , V n ) → okzkp
where zkp, checkzkp, okzkp do not occur in the U i , V j . Since the terms U i , V j are left unspecified, this captures most existing zero-knowledge proofs. In particular, it covers the zero-knowledge proofs considered in Example 3. A voting protocol is a family of processes As usual it is sufficient to consider voting processes that model only the honest voters and the tally (the dishonest voters are left unspecified as part of the environment, and their credentials are public). We may assume w.l.o.g. that the tally process starts with a fresh phase and first reads the ballots on the board. Formally, we assume that voting processes are of the form:

{Π n h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb )} n h ,n d ,
Π n h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb ) def = V ( c r 1 ) | V ( c r 2 ) | • • • | V ( cr n h ) | tall : bb(x 1 ). . . . .bb(x m ).T n,m (Cr n , K pv , K pb )
where Cr n = Cr h n h ∪ Cr d n d , and for all i ∈ {1, . . . , n h }, c r i ∈ Cr h n h . Furthermore, we require that Phase(V ) < tall, Phase(T n,m ) = ∅ and T n,m (Cr n , K pv , K pb ) contains at most one output which is performed on the channel tal. We note that from the above structure of a voting process it follows that all traces are prefixes of traces of the form tr •phase tall•bb(RB 1 ). . .bb(RB m )•νy.tal y .

V ( cr) models an honest voter, whose credentials are cr. T n,m (Cr n , K pv , K pb ) is the remainder of the tallier process. It is parameterised by the number m of ballots it accepts and the number n of eligible voters. We require that V ( cr) be independent of n and m and does not use any other credentials, i.e. fn(V ( cr)) ∩ Cr n ⊆ { cr}. These are the only restrictions on the voter process and we believe them to be reasonable and natural.

An e-voting protocol proceeds in two phases: vote casting and tallying. During the vote phase all voters simply cast their ballots. The tally phase proceeds as follows. First m ballots are input. Then a public test is applied to these ballots to carry out a first validity check, e.g. verify some zero knowledge proofs ensuring that the ballots are well formed. Next, the revote policy is applied to remove votes cast by a same voter, e.g., keep only the last one. Finally, the process performs the tally and outputs the result.

Public tests

As explained above, the ballot box may apply public tests to the casted ballots. Public tests are Boolean combinations over atomic formulas of the form M = N where M, N ∈ T (Σ, X), i.e. they do not contain any names. An atomic formula is satisfied when M = E N and we lift satisfaction to tests as expected.

We assume a family of tests {Test m } m∈N where m is the number of casted ballots that are tested and Test m contains m distinguished variables x 1 , . . . , x m to be substituted by the ballots. We write Test m ([B 1 , . . . , B m ]) = when the test Test m {x 1 → B 1 , . . . , x m → B m } is satisfied. Finally we say that a test is voting-friendly whenever satisfaction is preserved on sublists of ballots, that is

Test m ([B 1 , . . . , B m ]) = implies Test h ([B i1 , . . . , B i h ]) = for any 1 ≤ i 1 < • • • < i h ≤ m.
We believe this condition to be natural. It discards contrived tests that would accept a ballot only if another ballot is present. Conversely, we may consider tests that discard lists with duplicate ballots.

Example 8. The public test applied by the tallying authorities in the Helios protocol consists of two parts. First, a local test that checks the zero knowledge proofs of each submitted ballot, and second, a global test that checks that encrypted votes are pairwise distinct. This is to avoid the replay attack mentioned in [START_REF] Cortier | Attacking and fixing helios: An analysis of ballot secrecy[END_REF]

Revote policies

Many e-voting protocols offer voters the possibility to cast several votes, keeping eventually only one vote per voter, e.g. the last submitted ballot. Which vote is kept depends on the particular policy. Re-voting intends to guarantee some protection against coercion. We formalize the notion of policy as a function Policy n,m which takes a list of m terms (intuitively, the vote and credential) and a set of n credentials (honest and dishonest) and returns the sublist of selected terms to be tallied. A protocol will depend on a family of such policy functions {Policy n,m } n,m∈N . We consider two particular, but standard revote policies. The most usual one selects the last cast vote:

Policy n,m last ([V 1 , . . . , V m ], Cr n ) def = [V i1 , . . . , V i k ]
where each V ij = (v, cr) is the last occurence of the credential cr ∈ Cr n in the list [V 1 , . . . , V m ]. We also consider the policy which only keeps the first vote of each voter:

Policy n,m first ([V 1 , . . . , V m ], Cr n ) def = [V i1 , . . . , V i k ]
where each V ij = (v, cr) is the first occurence of the credential cr ∈ Cr n in the list

[V 1 , . . . , V m ]
. Such a policy typically models the norevote policy (a voter cannot revote).

Extracting ballots and counting votes

A voting protocol should tally the ballots "as expected". Formally, what is expected can be formalized through an extract and a counting function. Given a ballot B, and two sets of terms K pb and K pv representing the public and private material, the extraction function Extract returns the corresponding vote and credential, or ⊥ when a ballot is not well formed., i.e., Extract(B, K pv , K pb ) ∈ (V × Cr n ) ∪ {⊥}. Moreover, we lift the extract function to lists of m ballots by applying the function pointwise, i.e.,

Extract m ([B 1 , . . . , B m ], K pv , K pb ) def = [Extract(B 1 , K pv , K pb ), . . . , Extract(B m , K pv , K pb )]
Similar extract functions have been introduced in [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF] to define ballot privacy. Similarly the counting function defines how the protocol is supposed to tally the votes. The function Count takes as input a list of pairs (v, cr) ∈ V × Cr and returns a list of terms as the election result. Definition 4. Let {Count } ∈N be a family of counting functions. {Count } ∈N is votingfriendly if for all m, n and lists of terms W 1 of size m, W 2 of size n we have that

1. if W 1 = # W 2 then Count m (W 1 ) = # Count n (W 2 ); 2. if Count m (W 1 ) = # Count n (W 2 ) then Count m+1 ((v 1 , cr 1 ) :: W 1 ) = # Count n+1 ((v 2 , cr 2 ) :: W 2 ) iff v 1 = v 2
The first assumption requires that the result does not depend on the order in which votes are provided (intuitively, only valid votes are kept at this stage). We believe this property to be natural and it excludes contrived counting functions that would, e.g., only keep votes at even positions. The second assumption states that we may count "step by step". This is more restrictive since it excludes the majority function, i.e., the function that only outputs the name of the candidate that received most votes. But, it captures the most common result functions, namely the multiset and the additive counting functions.

Example 10. The multiset counting function typically arises in mixnet based tallies, which simply output the list of votes (intuitively once votes have been shuffled).

Count 1 Mix ([V 1 ]) def = [v] and Count m Mix ([V 1 , . . . , V m ]) def = v :: Count m-1 Mix ([V 2 , . . . , V m ])
where V 1 = (v, cr) and m > 1. The additive counting function can be defined similarly.

For simplicity consider a binary vote, where we just want to count the number of 1's:

Count 1 HE ([V 1 ]) def = v and Count m HE ([V 1 , . . . , V m ]) def = v + Count m-1 HE ([V 2 , . . . , V m ])
where V 1 = (v, cr), m > 1 and + is an AC symbol. Both functions are voting-friendly.

Properties

When verifying security properties of e-voting protocols it is common to only consider processes whose runs satisfy a particular property. For instance, vote secrecy is typically expressed as the indistinguishability of two processes modelling the situations where two honest voters swap their votes. We need however to ensure that these two honest voters have indeed cast their votes successfully to avoid trivial attacks. Indeed, in a run where the attacker blocks one of these voters, but not the other, the election result will be different and the two processes would be distinguished. Therefore when checking vote secrecy one typically adds a check that guarantees that the two honest votes are counted. We simply require that a check check( How such a check is implemented is left unspecified, it could be by listening to private channels, successively checking signatures, etc.

E-voting processes

As often when considering trace equivalence (e.g. [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF]), we assume processes to be deterministic. More precisely, we require the vote phase to be determinate: if the same sequence of labels leads to two different processes then the two resulting frames have to be statically equivalent. This typically holds for standard voting processes since the voter's behaviour is deterministic. For the tallying phase we slightly relax this notion and require what we call almost determinate. This relaxed notion only requires that there exists an output of a tally (among all possible outputs, as the particular tally may be chosen non-deterministically) that ensures static equivalence. This allows us to capture some non-deterministic behaviors such as mixnet tally. 2) Whenever the tally produces an output (that is (νy.tal y , A 2 ) ∈ traces(A 1 )) then it outputs a triple yφ(A 2 ) = res, nvotes, zkp where res is the result computed by counting the votes once the extraction function and the revote policy have been applied on the bulletin board; nvotes is the number of votes that has been counted; zkp is a (valid) zero-knowledge proof that would not be valid for any other list of ballots different from BB; either res is the only result the tally can produce from BB (typically in the homomorphic case) or the tally can produce any permutation of it (typically in the mixnet case).

A fully formal definition can be found in the companion technical report [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF]. We believe most existing protocols satisfy these requirements.

For many protocols ballots can be associated to the public credentials that were used to cast them. This is the case for Helios and some of its variants where ballots either contain the voter identity (in the original Helios) or are signed using private credentials (in the Belenios system). As we will see in the next section we can get tighter bounds for this class of protocols. Formally we define protocols with identifiable ballots as follows.

∀1 ≤ i ≤ m. if Extract([RB i φ(A)], K pv , K pb ) = (V, cr) then R i φ(A) = pub( cr)
where

R i = R{x → RB i }.
Throughout the section we consider two voting protocols

{Π n h ,n d ,m i (Cr h n h , Cr d n d , K pv , K pb )} n h ,n d ,m∈N
for 1 ≤ i ≤ 2 which are voting-friendly for check i , {Test m } m∈N , {Policy n,m } n,m∈N , Extract m i , {Count i } ∈N . Note that we assume the same public test for both protocols. Moreover we assume that n h ≥ 2 and m ≥ n h + n d .

Let E 0 be a set of names, and Φ 0 a ground substitution representing the initial attacker knowledge. {A n h ,n d ,m 0 } n h ,n d ,m∈N and {B n h ,n d ,m 0 } n h ,n d ,m∈N are two families of extended processes defined as follows

A n h ,n d ,m 0 def = (E 0 ∪ Cr h n h , Π n h ,n d ,m 1 (Cr h n h , Cr d n d , K pv , K pb ), Φ 0 , 0) ∀n h , n d , m ∈ N B n h ,n d ,m 0 def = (E 0 ∪ Cr h n h , Π n h ,n d ,m 2 (Cr h n h , Cr d n d , K pv , K pb ), Φ 0 , 0) ∀n h , n d , m ∈ N

Our reduction results apply to equivalences of the form

A n h ,n d ,m 0 ≈ B n h ,n d ,m
0 for all m, n h , n d . Vote privacy is typically modelled in this way [START_REF] Kremer | Analysis of an electronic voting protocol in the applied picalculus[END_REF]. The proofs of the results presented in this section could not be included due to lack of space, but are available in the technical report [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF].

Our first result states that attacks on such equivalences require at most 3 voters.

Proposition 1. If A k h ,k d , 0 ≈ B k h ,k d , 0 then A 2,k d , 0 ≈ B 2,k d , 0 for k d = 0 or k d = 1.
Note that this case does not yet bound the number of ballots to be considered. In particular, when re-voting is allowed the attacker may a priori need to submit several ballots in order to distinguish the two processes. In other words, the ballot box is still parameterized by the number of ballots to be received. However, whenever we assume that Π 1 and Π 2 do not allow voters to revote, we can deduce immediately that 3 ballots suffice to capture any attack. More formally, we encode this situation by letting k = and considering the re-vote policy that only keeps the first vote of each voter.

Theorem 1. If {Policy n,m } n,m∈N = {Policy n,m first } n,m∈N and A k h ,k d ,k 0 ≈ B k h ,k d ,k 0 where k = k h + k d , then A 2,k d ,k 0 ≈ B 2,k d ,k 0 for k d = 0 or k d = 1 and k = 2 + k d .
Intuitively, the case where k d = 0 corresponds to the case where an attacker can distinguish the processes playing only with two honest voters. This case for instance arises when analyzing a naive protocol where each voter simply signs his vote, hence offering no anonymity at all. The case where k d = 1 corresponds to the case where the attacker computes a vote which depends on the honest votes. The above results state that an attacker does not need more then one ballot in that case. An example of such an attack is the vote copy attack on Helios described in [START_REF] Cortier | Attacking and fixing helios: An analysis of ballot secrecy[END_REF]. We could actually encode any attack with 2 voters into an attack with 3 voters by letting the adversary play like a useless, honest, voter. This would require however to formalize the fact that the attacker may always simulate an honest voter, that is, the voting process.

We now consider the case where re-voting is allowed. In this case we can bound the number of ballots that need to be considered to 4 + 2k (for k number of voters in total).

Proposition 2. If

A k h ,k d , 0 ≈ B k h ,k d , 0 , then there exists min ≤ 4 + 2k such that A k h ,k d , min 0 ≈ B k h ,k d , min 0 where k = k h + k d .
Combining the reductions on the number of voters and the number of ballots we obtain the following theorem.

Theorem 2. If

A k h ,k d , 0 ≈ B k h ,k d , 0 , then there exists k d ∈ {0, 1}, min ≤ 4 + 2k such that A 2,k d , min 0 ≈ B 2,k d , min 0 where k = 2 + k d .
This is an immediate consequence of Propositions 1 and 2 and yields a bound of 4+2×3=10. When protocols have identifying ballots (Definition 7) we can tighten our reduction of the number of ballots: we only need to consider 4 + k ballots.

Corollary 1. If Π 1 and Π 2 have identifying ballots and A k h ,k d , 0 ≈ B k h ,k d , 0 , then ∃ min ≤ 4 + k. A k h ,k d , min 0 ≈ B k h ,k d , min 0 where k = k h + k d .
This is a corollary of the proof of Proposition 2. With identifiable ballots, we know that the ballots selected by the revoting policy on the left and on the right hand-side are the same. Again, we combine this result with the reduction on the number of voters.

Theorem 3. If Π 1 and Π 2 have identifying ballots and A k h ,k d , 0 ≈ B k h ,k d , 0 then ∃k d ∈ {0, 1}, min ≤ 4 + k such that A 2,k d , min 0 ≈ B 2,k d , min 0 where k = 2 + k d .
This follows from Corollary 1 and Proposition 1 and yields a bound of 4+3=7 ballots.

Case studies

We apply our results on several case studies: several versions of Helios [START_REF] Adida | Helios: web-based open-audit voting[END_REF][START_REF] Cortier | Election verifiability for helios under weaker trust assumptions[END_REF][START_REF] Bulens | Running mixnet-based elections with helios[END_REF] and Prêt-à-Voter [START_REF] Ryan | Prêt-à-voter with re-encryption mixes[END_REF], as well as the JCJ protocol [START_REF] Juels | Coercion-resistant electronic elections[END_REF] implemented in the Civitas system [START_REF] Clarkson | Civitas: Toward a secure voting system[END_REF]. For some of these protocols we show that the ProVerif verification tool [START_REF] Blanchet | An efficient cryptographic protocol verifier based on Prolog rules[END_REF] can be used to perform a security proof that, thanks to our results, is valid for an arbitrary number of voters and ballots.

For the other protocols, ProVerif is not able to verify the protocols, either due to the fact that equational theories with AC symbols are not supported by ProVerif or simply because of a state explosion problem. In these cases we show that our results nevertheless apply. Given recent progress in automated verification for equivalence properties [START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF][START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Cheval | Proving more observational equivalences with proverif[END_REF] we hope that verification of some of these protocols will be possible soon. Our results would also be useful to simplify proofs by hand.

The results in this section are summarized in Figure 2. Our hypotheses were always satisfied wherever applicable. For several protocols, we could not conduct the analysis with ProVerif, either because the equational theory is out of reach of the tool or because we had to stop ProVerif execution after a couple of hours. The case studies are further detailed in the companion report [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF]. The results in this section rely on ProVerif scripts available at http://3voters.gforge.inria.fr.

Conclusion

In this paper we propose reduction results for e-voting protocols that apply to vote privacy. We believe they also apply to stronger properties such as receipt-freeness. Our first reduction result states that whenever there is an attack, there is also an attack with only two honest voters and at most one dishonest voter. This considerably simplifies the proofs and encodings otherwise needed to verify such protocols using automated verification tools. We moreover consider the case where the protocol allows a voter to cast multiple votes and selects one vote according to a given re-vote policy, e.g. select the last vote casted. In that case verifying privacy is still complicated even when restricted to three voters. We therefore show a second reduction result that allows to consider at most 10 ballots. In case the protocol has identifiable ballots we reduce the number of necessary ballots to 7. We have shown that the hypotheses of our theorems are satisfied by many protocols: several variants of Helios, Prêt-à-Voter, as well as Civitas. For several of these protocols we were able to apply automated tool verification and provide the first automated proofs for an unbounded number of voters and ballots. For the decryption mixnets-based PaV protocol, we even provide the first proof of vote privacy.

An interesting direction for future work is to further tighten the bound on the number of ballots, possibly characterizing properties enjoyed by voting protocols. We also foresee to show similar reduction results for other properties of e-voting, such as verifiability. Given that the result is stated in a symbolic model, we also plan to investigate if the result can be transposed to a computational model.

  checkzkp E (zkp E (xr, xv, aenc(xpk, xr, xv)), aenc(xpk, xr, xv)) = okzkp E .

the relation s =Example 6 .

 s6 ⇒ on processes is defined by: A s = ⇒ B if, and only if there exists w ∈ A * such that A w -→ B and s is obtained by erasing all occurrences of τ from w. Continuing our running example we illustrate the operational semantics by the following transitions

  prf B } where bal C = aenc(pk(skE), r C , v D ) and prf C = zkp E (r C , v D , bal C ) for C, D ∈ {A, B} with C = D. Since adec(skE, π 1 (π 1 (getmsg(y A ))))Φ = E v A , but adec(skE, π 1 (π 1 (getmsg(y A ))))Φ = E v A , we have that νskE.νr A .νr B .Φ ∼ E νskE.νr A .νr B .Φ while νr A .νr B .Φ ∼ E νr A .νr B .Φ

Definition 3 (

 3 Trace equivalence). Let A and B be two closed extended processes. A is trace included in B, written A B, if for every trace (tr, A ) ∈ traces(A) there exists B such that (tr, B ) ∈ traces(B) and A ∼ B . A and B are trace equivalent, denoted A ≈ B, if A B and B A.

  . Such checks are formally reflected by the family of tests {Test m } m∈N with T est m ([B 1 , . . . , B m ]) def = i=m i=1 lTest(B i ) i =j i,j∈{1,...,m} gTest(B i , B j ) lTest(B) def = if B = id, bal, prf and checkzkp E (getmsg(bal), prf ) = E okzkp E ⊥ otherwise gTest(B, B ) def =    if B = id, bal, prf and B = id , bal , prf and getmsg(bal) = getmsg(bal ) ⊥ otherwise

Example 9 .

 9 The Extract function for the Helios protocol decrypts the encrypted vote and associates it with the signature associated to the ballot: Extract(B, {skE}, {pk(skE)}) def = (v, (id, cred)) if B = id, bal, prf and bal = E sig(aenc(pk(skE), r, v), cred) ⊥ otherwise

[b 1 -

 1 , . . . , b m ]) applied to a list ballots [b 1 , . . . , b m ] satisfies the two following requirements: If check([b 1 , . . . , b m ]) holds then we can identify two (intuitively honest) ballots b i1 , b i2 such that check holds for any sublist containing b i1 and b i2 . -If check([b 1 , . . . , b m ]) does not hold then it does not hold either for any sublist of these ballots or if some ballots are replaced by invalid ones (that is replaced by ⊥).

Fig. 2 .

 2 Fig.2. Summary of application of our results on case studies. A × in the "ProVerif" column indicates that we could not successfully run the analysis with ProVerif.

  m∈N where n h and n d are the number of honest and dishonest voters respectively; -Cr h n h (resp. Cr d n d ) is the set of n h (resp. n d ) voting credentials which determines the set of honest eligible voters (resp. dishonest eligible voters), such that Cr h n h ∩ Cr d n d = ∅. Each credential cr ∈ Cr h n h ∪ Cr d n d is a sequence of terms; m is the number of ballots accepted during the tally; -K pv (resp. K pb ) is the set of all private (resp. public) material.

  Definition 5. An e-voting protocol {Π n h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb )} n h ,n d ,m∈N is almost determinate if for any set of names E 0 , any initial attacker knowledge Φ 0 , any m, n h , n d ∈ N, and any traces (tr, A 1 ), (tr, A 2) ∈ traces(E 0 , Π n h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb ), Φ 0 , 0) we have that =====⇒ A 2 and A 1 ∼ A 2We can now put all the pieces together and link e-voting protocols to the notions of public tests, revote policies, extraction and counting functions and properties.Definition 6. An e-voting protocol{Π n h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb )} n h ,n d ,m∈N is voting friendly w.r.t. check, {Test m } m∈N , {Policy n,m } n,m∈N , Extract, {Count } ∈N if it is almost determinate, if {Test m } m∈N , {Policy n,m } n,m∈N , Extract, are voting-friendly, and if for any set of names E 0 , any initial attacker knowledge Φ 0 , any m, n h , n d , and any trace (tr •νx.phase tall.bb(RB 1 ). . .bb(RB m ), A 1 ) of (E 0 , Π n h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb ), Φ 0 , 0), the resulting list of ballots BB = [B 1 , . . . , B m ] (where B i = RB i φ(A 1 )) satisfies the following properties. 1) The tally is successful (that is (νy.tal y , A 2 ) ∈ traces(A 1 )) if and only if BB passes the test and the check (Test m (BB) = and check(BB) = )

	∀A 1 . A 1	νx.tal x =====⇒ A 1 ⇒ ∃A 2 . A 2	νx.tal x

  Definition 7. An e-voting protocol {Πn h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb )} n h ,n d ,m∈N has identifiable ballots if for all n h , n d , m ∈ N, for any trace (tr •νx.phase tall.bb(RB 1 ). . .bb(RB m )•νy.tal y , A) of Π n h ,n d ,m (Cr h n h , Cr d n d , K pv , K pb ))there exists a recipe R and a variable x such that

Acknowledgments. This work has received funding from the European Research Council (ERC) under the EU's Horizon 2020 research and innovation program (grant agreement No 645865-SPOOC) and the ANR project SEQUOIA ANR-14-CE28-0030-01.


Improving SLAM with drift integration

Guillaume Bresson 1,2 , Romuald Aufrère 3,4 and Roland Chapuis 3 Abstract-Localization without prior knowledge can be a difficult task for a vehicle. An answer to this problematic lies in the Simultaneous Localization And Mapping (SLAM) approach where a map of the surroundings is built while simultaneously being used for localization purposes. However, SLAM algorithms tend to drift over time, making the localization inconsistent. In this paper, we propose to model the drift as a localization bias and to integrate it in a general architecture. The latter allows any feature-based SLAM algorithm to be used while taking advantage of the drift integration. Based on previous works, we extend the bias concept and propose a new architecture which drastically improves the performance of our method, both in terms of computational power and memory required. We validate this framework on real data with different scenarios. We show that taking into account the drift allows us to maintain consistency and improve the localization accuracy with almost no additional cost.

I. INTRODUCTION

In the quest for making vehicles autonomous, the scientific community revolving around mobile robotics has furnished an impressive amount of work towards localization without any prior knowledge. A vehicle must be able to locate itself accurately in its environment so as to take the right decisions (choose which path to follow for instance) in total autonomy. While some could think of GPS as the solution to this localization problem, it has quickly emerged that it was not enough, both in terms of accuracy (or cost needed to reach a proper accuracy with devices like RTK-GPS's) and reliability (urban canyons, etc.). The topic of Simultaneous Localization And Mapping (SLAM) has thus become part of the key to this localization issue.

While many SLAM solutions, relying on various sensors and methods, have been proven to work, some aspects are often overlooked, such as how to properly handle the inherent SLAM drift or how to have a framework which could work with different settings (as proposed in [START_REF] Kummerle | g2o: A general framework for graph optimization[END_REF]) and deal with high-level issues (detect loops, integrate geo-referenced information, take into account the localization drift, etc.).

The localization provided by SLAM algorithms tend to drift over time [START_REF] Bar-Shalom | Estimation with Applications to Tracking and Navigation[END_REF]. Improving the localization capabilities is thus tightly linked to the integration of all sorts of information that can help reduce this drift. We can divide them in three categories that overlap. Geo-referenced data is a first way to counter the drift as it is not affected by it [START_REF] Conte | Vision-Based Unmanned Aerial Vehicle Navigation Using Geo-Referenced Information[END_REF]. Finding loops in the trajectory (recognizing previously visited places) is another way. By identifying previously perceived landmarks, it becomes possible to reduce the drift to what it was when landmarks were first seen [START_REF] Martinelli | Some Results on SLAM and the Closing the Loop Problem[END_REF]. Last, information coming from external agents (other vehicles, infrastructure, etc.) can at least constrain the drift as they are not similarly (or at all) affected by it [START_REF] Bresson | Consistent Multi-robot Decentralized SLAM with Unknown Initial Positions[END_REF]. In order to properly integrate this knowledge in a SLAM algorithm, a global sensor independent architecture should be prefered.

In this article, we propose a solution to solve both problems with a drift model integrated inside a dedicated architecture. Based on previous works [START_REF] Bresson | Consistent Multi-robot Decentralized SLAM with Unknown Initial Positions[END_REF], we improve the overall performance of our system with a new drift integration and a different handling of the map state. We present here an application to the loop closing problem using a data association process which is not sensor dependent as well as an example of geo-referenced integration.

We will first present related work regarding SLAM drift in Section II. Then, in Section III, we will give further details about the drift model that we previously introduced in [START_REF] Bresson | Consistent Multi-robot Decentralized SLAM with Unknown Initial Positions[END_REF]. Next, in Section IV, we will focus on the new architecture proposed in this paper to deal with the drift problem. We will expose the integration of a feature-based SLAM and how the drift is taken into account. Finally, an experimental validation will be provided in Section V along with various metrics and resource consumption comparisons.

II. RELATED WORK

The drift is causing the computed localization (and therefore the map as well) to slowly diverge from its true value. Moreover, the uncertainty associated to the vehicle pose does not include the real pose. It means that the computed estimate is inconsistent and should not be trusted.

The divergence problem affecting SLAM algorithms has been stated several times in the literature. The use of nonlinear models that need to be linearized is one of the reason causing the divergences. Indeed, linearizations made far from the true value tend to produce optimistic estimates [START_REF] Bar-Shalom | Estimation with Applications to Tracking and Navigation[END_REF]. The consequence is that the localization slowly drifts over time. Of course, the use of any sensor from whose errors accumulate over time (odometer for instance) will also provoke this phenomenon. Correlations between sensor data are also a source of overconfidence [START_REF] Julier | A Counter Example to the Theory of Simultaneous Localization and Map Building[END_REF]. Indeed, most of the time, it is wrongly considered that data coming from the same sensor are not temporally linked. It also appears that an approximation regarding the vehicle orientation has a stronger impact on the divergence than a translation error [START_REF] Bailey | Consistency of the EKF-SLAM Algorithm[END_REF]. The literature regarding SLAM drift usually considers two ways of dealing with it: by avoiding it or by reducing it when possible.

The former category includes submapping approaches [START_REF] Estrada | Hierarchical SLAM: realtime accurate mapping of large environments[END_REF] where new reference frames are regularly set. At a submap level, most of the drift is avoided. It can be an issue as creating too much submaps leads to an information loss. However, the global map linking all the submaps is still affected by the divergence. In a similar manner, robot-centric methods are often considered to avoid drift [START_REF] Castellanos | Robocentric Map Joining: Improving the Consistency of EKF-SLAM[END_REF]. Estimates are always given with relation to the robot pose thus limiting consistency problems as they do not accumulate over time. However, as for submapping techniques, divergence is not solved when considered out of the robot-centered frame which is needed to detect loop closures and in many other applications. Some authors have worked on reducing errors with smoothing approaches [START_REF] Dellaert | Square Root SAM: Simultaneous localization and mapping via square root information smoothing[END_REF]. Even with such methods, the remaining drift could still be taken into account to improve consistency.

Regarding reducing drift, in [START_REF] Conte | Vision-Based Unmanned Aerial Vehicle Navigation Using Geo-Referenced Information[END_REF], satellite images are used to obtain an absolute localization. The satellite images are compared to the output of a standard camera. The vehicle pose can be computed based on these absolute, and so driftfree, correspondences. A geo-referenced database is also a good way to remove the drift and maintain consistency. However, most of the time, absolute information can only be integrated punctually and there is no guarantee that the system will not drift in-between. In [START_REF] Martinelli | Some Results on SLAM and the Closing the Loop Problem[END_REF], the authors show that even if closing the loop reduces the drift, the results will always be overconfident because of approximations regarding the links between landmarks. Cole and Newman in [START_REF] Cole | Using Laser Range Data for 3D SLAM in Outdoor Environments[END_REF] propose to redistribute errors in a probabilistic manner around the past trajectory. Even if better results are obtained, the resulting map is not always consistent. Besides, the vehicle pose will certainly be diverging without knowing so before finding any loop closing.

The solutions presented in this last paragraph can all be applied to reduce the drift. However, it appears mandatory to be able to represent the drift at any time even without such information. This is why we propose here to model the drift and to integrate it inside a Kalman filter so as to estimate it conjointly with the vehicle state and the map.

III. DRIFT

We define the localization bias as the parameters allowing to compensate the drift. As the drift tends to grow with the distance traveled, the localization bias evolves according to the curvilinear abscissa. As so, at a curvilinear abscissa s, the bias is defined as: The localization bias follows a dynamic model. Indeed, the bias at a curvilinear abscissa s strongly depends on the one preceding it at s -∆s. Starting from the evolution equation of a continuous stochastic linear system [START_REF] Thrun | A Probabilistic Online Mapping Algorithm for Teams of Mobile Robots[END_REF], we can write:

ḃ(s) = A c b(s) + B c u(s) + M c ε(s) ( 2
)
where b is the bias vector, u the input vector and ε the evolution noise which is assumed white. A c is the state matrix associated to b, B c expresses the link between u and b and M c the link between ε and b.

The drift is considered to evolve similarly across its three parameters and as such, a simple random walk can be used as an approximate model. Considering so, A c = 0, B c = 0 and M c = I (identity matrix), and the drift evolution becomes:

ḃ(s) = ε(s) (3)
By discretizing Equation (3), we obtain the following bias evolution:

b s = Ab s-∆s + ε ∆s = exp(A c ∆s)b s-∆s + ε ∆s = b s-∆s + ε ∆s (4)
with ε ∆s being the drift (white noise) affecting the vehicle between s -∆s and s.

In order to ensure consistency at any time, the uncertainty regarding the drift occurring between s -∆s and s must be considered. It is expressed as follows:

P ε∆s = ∆s 0 exp(A c s)P ε exp(A T c s)ds (5)
with P ε being the uncertainty associated to ε(s).

Based on Equations ( 4) and ( 5), the bias uncertainty P bs is calculated as:

P bs = P bs-∆s + ∆sP ε (6)
We consider here a stationary process. Even though the bias evolution is not identical in every situation (for instance, turning might have a stronger impact on the rotation drift than going straight), this approximation is sufficient if P ε is properly characterized. As a consequence of the stationarity hypothesis, P ε can be experimentally defined, based on the observed quadratic divergence over the distance traveled.

Considering the vehicle pose

v k = x k y k θ k T at
a time k corresponding to the curvilinear abscissa s, the localization bias can be integrated as follows (where u stands for unbiased):

v u k = R(b θs ) 0 2×1 0 1×2 1 v k + b s =   cos(b θs ) -sin(b θs ) 0 sin(b θs ) cos(b θs ) 0 0 0 1   v k + b s (7)
Similarly, for a landmark l i k = l ix k l iy k T , the localization bias can be taken into account:

l ui k = R(b θs )l i k + b xs b ys (8)
Based on Equations ( 7) and ( 8), we can also infer how the uncertainty regarding the vehicle pose and a landmark position will be affected by the drift integration. However, integrating the bias localization directly into the SLAM process where these estimates are computed will not prevent the system from being inconsistent. Indeed, observations will lower the bias uncertainty while it should not be the case. A dedicated architecture is thus needed to avoid this phenomenon.

IV. GLOBAL ARCHITECTURE

The objective of this architecture is twofold: providing a framework in which any feature-based SLAM algorithm can take into account and handle the drift as well as integrating all the possible means to estimate it thanks to the ensured consistency. To do so, the initial SLAM should be decorrelated from the part responsible for the drift estimation. It has the advantage to avoid mixing uncertainties and to allow the use of any feature-based SLAM algorithm. This led us to the organization presented in Figure 1. It can be noted that the low-level SLAM algorithm just communicates with the rest of the architecture by providing landmark and vehicle estimates. A dedicated process takes these incoming landmarks and vehicle poses and builds a proper map, designed to be consistent due to the bias integration. Specific modules, whose goal is the drift estimation, can then be developed (squared in blue in Figure 1) by taking advantage of this new consistent map. Each module provides a way to estimate the bias. The drift estimation module is in charge of activating them and provides the information to fuse to the Extended Kalman Filter (EKF). So as to balance the computing requirements, landmarks do not need to be kept in the low-level algorithm when they are not visible anymore. As associations (loops for instance) are sought in the high-level, it is not useful to have all the landmarks in the low-level (and thus allowing the use of Visual Odometry algorithms). This way, the architecture does not add much to a classic SLAM in terms of memory or processing power required.

An EKF is used to handle the high-level map. Its goal is to connect the bias estimates together based on Equation (4) and update them when an information allowing so is available (loop closing, geo-referenced data, etc.). Bias estimates are regularly inserted (by the Bias integration module) based on the distance traveled in order to represent the drift along the trajectory. While there should ideally be a bias estimate per landmark, it would require an important amount of resources to handle them and would not improve much the localization quality. With no prior knowledge about the drift (ε = 0), its initialization via the Kalman Filter is simple:

b s = b s-∆s (9)
In order to connect the current bias to its previous estimate, we first initialize its variance to infinite values inside the covariance matrix and use the EKF to refine it. To do so, let define the observation function h b which makes the difference between two consecutive bias estimates:

h b (b s , b s-∆s ) = b s -b s-∆s (10)
We define the observation error as follows:

R b = P bs -P bs-∆s (11)
H b , the Jacobian matrix associated to h b , can be computed:

H b = 0 3×3(n-2) -I 3×3 I 3×3 ( 12
)
where n is the number of bias estimates in the state vector. A Kalman update is then performed to link together bias estimates and properly initialize the uncertainty of the new bias estimate b s . The lack of knowledge about ε makes the Kalman innovation equal to zero, meaning that only the covariance matrix will be affected by the update.

Instead of inserting landmarks and vehicle poses into the state vector, we chose to only have connected bias estimates. The main motivation is to reduce the memory used by the storage of a rapidly growing covariance matrix as well as the processing power needed to properly insert a new element inside the map. Indeed, the EKF requires several multiplications involving the whole state vector and covariance matrix and, even though it is not an important burden with a few landmarks, it quickly becomes unbearable with hundreds of them. As high-level landmarks and vehicle poses only depend on the bias estimation, there is no loss of information. The only constraint comes from the data association process which will be later discussed in this section. The high-level architecture is depicted in Figure 2.

Incoming landmarks are stored along with the current vehicle pose and the respective variances (1). The crosscovariances recomposed thanks to the previously presented drift integration are indicated in blue here (2). The vehicle state vector taking into account the bias (3) is here to help the data association process.

In order to correct the drift, landmarks must be associated and fused. The three modules presented earlier in Figure 1 work similarly. They consider incoming landmarks and look for associations across landmarks already in the highlevel (stored in (1) in Figure 2). The difference lies in the fact that the fusion does not affect the same bias estimates. In case of information coming from another vehicle for instance, the bias estimates of both vehicles involved are updated when an association is found. For geo-referenced Fig. 2. High-level architecture information, the bias estimates of the vehicle with which information is fused are concerned. Regarding loop closing, the fusion occurs between landmarks already mapped and new ones, which means that the bias estimates regarding these two sets of landmarks become directly connected. In each case, the cross-covariances recomposed (2) are able to properly spread the impact of an update on all the bias estimates concerned.

Let consider that a new landmark l j (associated to a bias b j ) corresponds to a landmark already mapped l i , the observation z = l j and its covariance R = P lj as received from the low-level SLAM (or a distant vehicle, or already known geo-referenced information). The association found means that l uj = l ui which allows us to define the nonlinear observation function h f as:

h f (b i , b j ) = R(b θj ) T R(b θi )l i + b xi b yi - b xj b yj (13)
The Jacobian H f associated to the function h f is then computed and used in the Kalman equations to update the state vector composed of bias estimates. All the bias estimates will be affected by the update. Of course, the farthest from the fusion point, the less concerned by the update will be bias estimates. By only working with the bias estimates, it allows the overall process to be faster while not preventing to compute unbiased landmarks or a drift-free vehicle pose if needed.

Concerning the data association, we use the fact that the bias model allows us to achieve consistency as a way to constrain and drive the association process. However, as consistent landmarks are not immediately available, correspondences cannot be directly sought. Instead of landmarks, we decided to work with vehicle poses. Like shown in Figure 2, a separate state vector is maintained with vehicle poses integrating the bias. Each time a new bias estimate is initialized, so is a vehicle pose in this vector. The idea is to reduce the search space around potential association areas. To do that, vehicle poses which are compatible, meaning that the vehicle could potentially be located in these already visited areas, are used. This unary constraint is computed as follows:

D 2 ik = (v ui -v u k ) T (P vu i + P vu k ) -1 (v ui -v u k ) < χ 2 d,α (14)
where v ui is the vehicle pose associated to the bias b i and v u k is the current one.

The acceptation threshold, below which an association is possible, is based on the Chi-squared distribution χ 2 d,α , with d = 3 (degrees of freedom) and the desired confidence α set to 0.95.

Only landmarks mapped between the different portions where vehicle poses are compatible will be tested in the association process, thus drastically reducing the number of potential pairings and the processing time required.

Once potentially already seen landmarks are extracted, they are tested with the newly mapped landmarks. To do so, we use the Geometric Constraints Branch and Bound (GCBB) method [START_REF] Neira | Linear time vehicle relocation in SLAM[END_REF]. The idea is to find sets of landmarks with similar binary geometric constraints. Corresponding landmarks should share the same geometric organization. Considering two potential associations a ij = (l i , l j ) and a kl = (l k , l l ), a binary geometric constraint is a relation between l i and l k which is also satisfied between l j and l l . In our case, l i and l k would be new landmarks and l j and l l , previously mapped landmarks. The geometric constraint used here is the relative distance between the landmarks (the distance between l i and l k must be similar to the one between l j and l l ). Binary constraints can be computed beforehand (and are limited to landmarks already satisfying the unary constraint). A tree of the potential sets of associations is then explored to find the best correspondences.

By using the consistency provided by the bias integration, we are able to limit the exploration time needed to find associations. The use of binary geometric constraints has the advantage to allow us to find pairings between landmarks which are not affected by the same orientation drift.

With geo-referenced information, the data association differs as landmarks are not necessarily expressed with relation to the same reference (local frame or absolute frame). In this case, we only use the geometric organization of new landmarks with the GCBB algorithm to associate them with geo-referenced ones.

V. EXPERIMENTS

We present two experiments to validate our approach. The first one shows a loop closure and the second one the integration of geo-referenced information. In both experiments, an electric vehicle (VIPALab) was manually driven at around 2 meters per second. Here, we do not consider the low-level SLAM to only focus on the high-level. Landmark positions and vehicles poses are received regularly without knowing what sensors or algorithms are used in the lowlevel (interested readers can refer to [START_REF] Bresson | Real-time monocular slam with low memory requirements[END_REF] for more information regarding the low-level SLAM).

The first trajectory presents a loop of approximately 100 meters. The vehicle returns to its starting point and continues for several meters in order to have enough landmarks to detect loop closures. Throughout the trajectory, 372 landmarks were mapped, with around 40 common to both passages (around the starting point of the trajectory). We compare the proposed algorithm to its previous version [START_REF] Bresson | Consistent Multi-robot Decentralized SLAM with Unknown Initial Positions[END_REF]. In this previous version, the architecture is different and the association algorithm is based on Indivudal Compatibility between landmarks. Both Matlab implementations are checked against the same trajectory.

Figure 3 shows the trajectories performed. It can be noticed that the trajectory out of the low-level SLAM slowly drifts from the ground truth (provided by a RTK-GPS). Conversely, when integrating the bias, the algorithm is able to detect the loop and correct the trajectory. Of course, the farthest part from the closing point is the less affected by the correction. Similar results are obtained by our previous architecture, showing that integrating landmarks in the highlevel state vector does not improve the localization accuracy (both trajectories are superimposed). The data association process worked well in both cases, allowing to close the loop several times around the starting point of the trajectory. For the first closure, individual compatibility between landmarks retained 160 of them (out of 372) for the GCBB process and individual compatibility between vehicle poses led to 145 landmarks for GCBB. These similar numbers show that using vehicle poses to limit the exploration tree of GCBB works as efficiently as using directly individual compatibility between landmarks. Landmarks integration inside the highlevel state vector is consequently not essential to the data association process. Concerning the accuracy of the obtained localization, we measured the Root-Mean-Square Error (RMSE) based on the ground truth. Results are visible in Figure 4. Closing the loop allows us to have a better position accuracy especially in the late trajectory (the beginning is quite similar).We obtain almost identical results between the approach of this paper and [START_REF] Bresson | Consistent Multi-robot Decentralized SLAM with Unknown Initial Positions[END_REF] (both curves are superimposed). The landmarks associated are the same in both methods hence the similar results. What is interesting is that the RMSE would have grown without the bias integration if the trajectory had continued because of the angular drift. This effect would have been prevented with our algorithm. As the primary goal of the bias model is to ensure consistency, we measured the Consistency Index (CI), as defined in [START_REF] Paz | Divide and Conquer: EKF SLAM in O(n)[END_REF], which is based on the Normalized Estimation Error Squared (NEES) and the Chi-square test. A CI lower than 1 means that the estimate is consistent with the ground truth. Conversely, estimates whose CI is greater than 1 are optimistic (inconsistent). CI curves with no association performed are pictured in Figure 5 and in Figure 6 when the loop is closed. The bias model allows us to achieve consistency even without applying any loop closure. It is obviously not the case without the bias integration as the CI quickly grows. Once again, similar results are obtained for both architectures showing that estimating only bias values in the EKF is sufficient. Consistency Index during the trajectory with no association performed.In green: CI of the low-level SLAM. In blue: CI with the approach presented in this paper. In red (superimposed with blue): CI with the previous bias integration. The black line represents the consistency threshold.

The main motivation behind this architecture was to provide a faster and less memory thrifty bias integration. Figure CI with the approach presented in this paper. In red (superimposed with blue): CI with the previous bias integration. [START_REF] Conte | Vision-Based Unmanned Aerial Vehicle Navigation Using Geo-Referenced Information[END_REF] shows the computing time taken by each algorithm all along the trajectory. The new architecture shows impressive results by using in average around 0.25 ms per iteration (integration of new landmarks and new bias estimate if needed) near the end of the trajectory while our previous implementation needs more than 220 ms for the same thing. It makes our approach suited for long trajectories. If necessary, bias estimates can easily be separated in substates and so reduce the time needed by the current architecture even more. In terms of memory consumption, the same trend can be noted (see Figure 8). Storing the different state vectors and covariance matrices requires almost 5 MB of memory at the end of the trajectory with the previous architecture whereas the new approach only uses around 100 KB. The exponential growth of our previous architecture is also way less pronounced with the new bias integration. In the second experiment, we show the integration of georeferenced landmarks. The context is the same as for the previous experiment. We start the trajectory with the georeferenced landmarks already known. The geo-referenced landmarks are created beforehand using the RTK-GPS. We generated 20 landmarks at mid-distance of the trajectory, with less than half common with the mapping process. As mentioned previously, we only use the geometric criterion to recognize these landmarks. The results can be seen in Figure 9. We can see that the integration of the geo-referenced landmarks allows us to correct the orientation drift that occurs during the bend. The localization is greatly improved even with only a few landmarks. The GCBB algorithm was able to find the common landmarks only using the geometric criterion (9 out of 20 were associated to the SLAM map). As previously, the RMS Error and the CI obtained by our algorithm are exposed in Figures 10 and11 The RMS Error is below 50 centimeters all along the trajectory and is under 20 centimeters close to the fusion point. Without new information to characterize the drift, it starts to grow again by the end of the trajectory. Without the bias integration, the error reaches 4 meters and would have gone further if the trajectory had continued. Regarding consistency, the same behavior can be observed. During the bend and without our dedicated architecture, consistency is lost. The Covariance Index goes above a value of 300 by the end of the trajectory and keeps on growing as there is no way to consider the drift. With the architecture presented in this paper, the CI stays below 1 meaning that consistency is maintained throughout the whole trajectory, even when no information to estimate the drift is available.

VI. CONCLUSION

We have presented a new architecture allowing us to take into account the drift inherent to SLAM algorithms. Thanks to this approach, the consistency of the computed localization can be maintained even without information to correct it. The new bias integration introduced in this paper requires very little resources compared to previous approaches thus permitting to consider drift integration even with long trajectories.

The bias model is integrated outside of the classic SLAM algorithm. It has the advantage to allow the use of any feature-based SLAM algorithm. The inclusion of the localization bias in the high-level EKF-SLAM provides an easy way to estimate the drift as consistency is ensured. Absolute information, loop closing or distant information can be easily integrated. We introduced a new data association process that takes advantage of the consistency provided by the bias model. Thanks to it, it becomes possible to detect loops without relying on clues of a specific sensor. Results showed that the localization obtained is consistent and that the overall architecture allows better performance over our previous approach.

We plan to expand this framework to various scenarios using diverse SLAM algorithms. A different bias model is also envisaged to deal with non-systematic errors that cannot be covered by motion models.

  b s = b xs b ys b θs T (1) with b xs and b ys representing a position bias and b θs an angular bias.

Fig. 1 .

 1 Fig. 1. Bias integration architecture

Fig. 3 .

 3 Fig. 3. Trajectories performed. In green: trajectory computed by the lowlevel SLAM. In blue: trajectory computed with the approach presented in this paper. In red (almost identical to the blue one): trajectory computed with the previous bias integration. In black: ground truth (RTK-GPS).

Fig. 4 .

 4 Fig. 4. Root-Mean-Square Error during the trajectory. In green: RMSE of the low-level SLAM. In blue: RMSE with the approach presented in this paper. In red (almost identical to the blue one): RMSE with the previous bias integration.

  Fig. 5.Consistency Index during the trajectory with no association performed.In green: CI of the low-level SLAM. In blue: CI with the approach presented in this paper. In red (superimposed with blue): CI with the previous bias integration. The black line represents the consistency threshold.

Fig. 6 .

 6 Fig.6. Consistency Index during the trajectory with associations. In blue: CI with the approach presented in this paper. In red (superimposed with blue): CI with the previous bias integration.

Fig. 7 .

 7 Fig. 7. Processing time required by the high-level algorithm.

Fig. 8 .

 8 Fig. 8. Memory used by the high-level algorithm. In blue: memory used by the approach presented in this paper. In red: memory used by the previous bias integration.

Fig. 9 .

 9 Fig. 9. Trajectories performed. In green: trajectory computed by the lowlevel SLAM. In blue: trajectory computed with the approach presented in this paper. Circled in red: location of the geo-referenced landmarks. In black: ground truth (RTK-GPS).

  with relation to their counterpart which does not integrate the drift.

Fig. 10 .

 10 Fig. 10. Root-Mean-Square Error during the trajectory. In green: RMSE of the low-level SLAM. In blue: RMSE with the approach presented in this paper.

Fig. 11 .

 11 Fig. 11. Consistency Index during the trajectory with associations (zoomed view). In green: RMSE of the low-level SLAM. In blue: RMSE with the approach presented in this paper. The black line represents the consistency threshold.