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

Joseph Lallemand
email: joseph.lallemand@loria.fr

Voting: You Can't Have Privacy without Individual Verifiability

Keywords: Security and privacy → Mathematical foundations of cryptography, Formal security models, Logic and verification, e-voting, privacy, verifiability, provable cryptography, symbolic verification

Electronic voting typically aims at two main security goals: vote privacy and verifiability. These two goals are often seen as antagonistic and some national agencies even impose a hierarchy between them: first privacy, and then verifiability as an additional feature. Verifiability typically includes individual verifiability (a voter can check that her ballot is counted); universal verifiability (anyone can check that the result corresponds to the published ballots); and eligibility verifiability (only legitimate voters may vote).

We show that actually, privacy implies individual verifiability. In other words, systems without individual verifiability cannot achieve privacy (under the same trust assumptions). To demonstrate the generality of our result, we show this implication in two different settings, namely cryptographic and symbolic models, for standard notions of privacy and individual verifiability. Our findings also highlight limitations in existing privacy definitions in cryptographic settings.

INTRODUCTION

Electronic voting is often seen as a convenient way for running elections as it allows voters to vote from any place. Moreover, it eases the tally and it can therefore often be used for non trivial counting procedures such as Single Transferable Vote or Condorcet. Numerous voting systems have been proposed so far, like Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF],

Belenios [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF], Civitas [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF], Prêt-à-voter [START_REF] Ryan | Prêt à Voter with Paillier encryption[END_REF], or the protocols deployed in Estonia [START_REF] Heiberg | Improving the Verifiability of the Estonian Internet Voting Scheme[END_REF] or in Australia [START_REF] Brightwell | An overview of the iVote 2015 voting system[END_REF] to cite a few. On the other hand, many weaknesses or even attacks have been unveiled [START_REF] Springall | Security Analysis of the Estonian Internet Voting System[END_REF][START_REF] Wolchok | Security Analysis of India's Electronic Voting Machines[END_REF], from voting machines [START_REF] Gonggrijp | Studying the Nedap/Groenendaal ES3B Voting Computer: A Computer Security Perspective[END_REF] to Internet voting [START_REF] Wolchok | Attacking the Washington, D.C. Internet Voting System[END_REF].

In order to carefully analyse voting systems, security requirements have been defined. The two main security properties are:

• privacy: no one should know how I voted; • verifiability is typically described through the three following sub-properties.

individual verifiability: a voter can check that her ballot is counted; -universal verifiability: anyone can check that the results corresponds to the published ballots; -eligibility verifiability: only legitimate voters may vote.

These two main properties seem antagonistic and an impossibility result has even been established between verifiability and unconditional privacy [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF], that is, a notion of privacy that is independent of the power of the attacker.

The main contribution of this paper is to establish that, in fact, (computational) privacy implies individual verifiability, that is, guarantees that all the honest votes will be counted. This result holds for arbitrary primitives and voting protocols without anonymous channels. To show that this implication is not due to a choice of a very particular definition, we prove this implication in two very distinct contexts, namely symbolic and cryptographic models. In symbolic models, messages are represented by terms and the attacker's behaviour is typically axiomatised through a set of logical formulas or rewrite rules. Cryptographic models are more precise. They represent messages as bitstrings and consider attackers that can be any probabilistic polynomial time Turing machines. Proofs of security are made by reduction to well accepted security assumptions such as hardness of factorisation or discrete logarithm. In both models, we consider a standard notion of privacy, already used to analyse several protocols. In both cases, we establish that privacy implies individual verifiability for a (standard) basic notion of individual verifiability, namely that the result of the election must contain the votes of all honest voters.

We now describe the main idea of the result. Actually, we show the contrapositive implication: if there is an attack against individual verifiability, then there is an attack against privacy. To explain the idea, let's consider a very simple protocol, not at all verifiable. In this simple protocol, voters simply encrypt their votes with the public key of the election. The ballot box stores the ballots and, at the end of the election, it provides the list of recorded ballots to the talliers, who detain the private key, possibly split in shares. The talliers compute and publish the result of the election. The ballot box is not public and no proof of correct decryption is provided so voters have no control over the correctness of the result. Such a system is of course not satisfactory but it is often viewed as a "basic" system that can be used in contexts where only privacy is a concern. Indeed, it is typically believed that such a system guarantees privacy provided that the attacker does not have access to the private key of the election. In particular, the ballot box (that is, the voting server) seems powerless. This is actually not the case. If the ballot box aims at knowing how a particular voter, say Alice, voted, he may simply keep Alice's ballot in the list of recorded ballots and then replace all the other ballots by encryptions of valid votes of his choice, possibly following a plausible distribution, to make the attack undetected. When the result of the election is published, the ballot box will know all the votes but Alice's vote, and will therefore be able to deduce how Alice voted.

One may argue that such an attack is not realistic: the ballot box needs to be able to change all ballots but one. Note however that elections are often split in many small voting stations (sometimes as small as 20 voters in total [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF]). Therefore changing a few ballots can be sufficient to learn how Alice voted. Maybe more importantly, this attack highlights the fact that it is not possible to require privacy without verifiability as sometimes specified by national agencies. For example, in France, only privacy is required [START_REF]octobre 2010 portant adoption d'une recommandation relative à la sécurité des systèmes de vote électronique[END_REF]. In Switzerland, privacy is a pre-requisite and the level of verifiability depend on the percentage of voters that can vote electronically [START_REF]Ordonnance de la ChF sur le vote électronique (OVotE) du 13 décembre 2013[END_REF]. Our findings point out that if voters cannot trust some authorities w.r.t. the fact that their vote will be counted they cannot trust the same authorities w.r.t. their privacy, even for entities that do not have access to the secret keys. Beyond the attack explained on a simple (and naive) protocol, our proof that privacy implies individual verifiability shows that as soon as a protocol is not verifiable, then the adversary can take advantage of the fact that he may modify a vote without being detected in order to break privacy. Individual verifiability is only one part of verifiability. It does not account for universal nor eligibility verifiability. So our result cannot be used to conclude that a private voting scheme ensures all desirable verifiability properties. Instead, it demonstrates that there is no hope to design a private voting system if it does not include some degree of verifiability, namely individual verifiability at least.

Our results also emphasise issues in existing privacy definitions. Indeed, if privacy implies individual verifiability, how is it possible to prove Helios [START_REF] Bernhard | How Not to Prove Yourself: Pitfalls of the Fiat-Shamir Heuristic and Applications to Helios[END_REF] or Civitas [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus[END_REF] without even modelling the verification aspects? How can a system that is not fully verifiable like the Neuchâtel protocol be proved private [START_REF] Galindo | 2015 Neuchâtel's Castas-Intended Verification Mechanism[END_REF]? As already pointed out in [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF], existing cryptographic definitions of privacy (see [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF] for a survey) implicitly assume an honest voting ballot box: honest ballots are assumed to be properly stored and then tallied. Actually, we notice that the same situation occurs in symbolic models. Although the well adopted definition of privacy [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] does not specify how the ballot box should be modelled, most symbolic proofs of privacy (see e.g. [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus[END_REF][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][START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF]) actually assume that the votes of honest voters always reach the ballot box without being modified and that they are properly tallied. The reason is that the authors were aware of the fact that if the adversary may block all ballots but Alice's ballot, he can obviously break privacy. However, to avoid this apparently systematic attack, they make a very strong assumption: the ballot box needs to be honest. This means that previous cryptographic and symbolic privacy analyses only hold assuming an honest ballot box while the corresponding voting systems aim at privacy without trusting the ballot box. This seriously weakens the security analysis and attacks may be missed, like the attack of P. Roenne [START_REF] Roenne | [END_REF] on Helios, for which there is no easy fix.

Why is it so hard to define vote privacy w.r.t. a dishonest ballot box? Intuitively, vote privacy tries to capture the idea that, no matter how voters vote, the attacker should not be able to see any difference. The key issue is that the result of the election does leak some information (typically the sum of the votes) and the adversary may notice a difference based on this. This particularity makes vote privacy differ from privacy in other contexts, where the adversary really should learn no information. Therefore, most definitions of vote privacy (roughly) say that, no matter how honest voters voted, provided that the aggregation of the corresponding votes remains the same, then the attacker should not see any difference. However, as soon as the ballot box is dishonest, it may discard some honest ballots and break privacy, as already discussed. The first definition of privacy w.r.t. a dishonest ballot box [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] weakens privacy by requiring that among the ballots that are ready to be tallied, the (sub-)tally of the honest ones does not change. This preliminary definition has two limitations. First, it assumes that the tallied ballots are exactly the same as the cast ones, which is not the case of all protocols (e.g. in ThreeBallots [START_REF] Rivest | Three Voting Protocols: ThreeBallot, VAV and Twin[END_REF], only a part of the ballot is published; in BeleniosRF [START_REF] Chaidos | BeleniosRF: A Non-interactive Receipt-Free Electronic Voting Scheme[END_REF], ballots are re-randomised). Second, it does not model re-voting: the tally process cannot discard ballots due to some revote policy.

We propose here another approach. Instead of changing the privacy definition, we now include a model of the verification process: the ballots should be tallied only if the honest voters have successfully performed the tests specified by the protocol. We compare our definition with [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] and an original definition of privacy [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF] on a selection of well-studied protocols, that have different levels of verifiability (Helios, Civitas, Belenios, Neuchâtel, and our simplenon verifiable -protocol). We show again that our notion of privacy, w.r.t. a dishonest ballot box, implies individual verifiability. We do not consider our new definition of privacy as final but it opens the way to a better understanding of privacy in the context of fully dishonest authorities.

Threat model. We show that privacy implies individual verifiability, under the same trust assumptions, that is, trusting the same group of authorities, channels, etc. In symbolic models, the privacy definition does not make prior assumptions on the threat model. Instead, the encoding of the protocol defines which parties are trusted. In particular, as already discussed, existing proofs of privacy [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus[END_REF][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][START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] often implicitly assume that honest ballots reach the ballot box without any modification. We show that whenever privacy holds then individual verifiability holds, for the same encoding, hence the same assumptions. In contrast, most cryptographic definitions of privacy implicitly assume an honest ballot box. Therefore, we first show that privacy implies individual verifiability, assuming an honest ballot box, considering the standard definition of privacy by Benaloh [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF]. Then we show that privacy still implies individual verifiability, assuming a dishonest ballot box, considering our novel definition of privacy, that explicitly models the verification steps.

Related work. As already mentioned, [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] shows an impossibility result between universal verifiability and unconditional privacy.

We show in contrast that the commonly used (computational) definitions of privacy actually imply verifiability. The discrepancy between the two results comes from the fact that [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] considers unconditional privacy while most protocols achieve only computational privacy, that is against a polynomially bounded adversary. Interestingly, the impossibility result still holds between unconditional privacy and our notion of individual verifiability. [START_REF] Delaune | Coercion-Resistance and Receipt-Freeness in Electronic Voting[END_REF] establishes a hierarchy between privacy, receipt-freeness, and coercion resistance, while in a quantitative setting, [START_REF] Küsters | Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study[END_REF] shows that this hierarchy does not hold anymore. [START_REF] Cortier | SoK: Verifiability Notions for E-Voting Protocols[END_REF] recasts several definition of verifiability in a common setting, providing a framework to compare them. Besides [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF], none of these approaches relates privacy with verifiability. Many privacy definitions have been proposed as surveyed in [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF]. However, they all assume an honest ballot box. To our knowledge, [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] is the only exception, as already discussed in details. [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF] shows how to break privacy by replaying a ballot. If an attacker may replay Alice's ballot and cast it in his own name (or cast a related ballot), then he introduces a bias in the result, that leaks some information on Alice's vote. Note that this replay attack does not break individual verifiability: honest votes are correctly counted. We show here another breach for privacy: if an attacker may remove some honest votes, then he breaks privacy as well.

Roadmap. We first prove that privacy implies individual verifiability in symbolic models, in Section 3, and then in cryptographic models, in Section 4. These two parts are rather independent. In Section 6, we examine a selection of well-studied voting protocols and compare the effect of different (cryptographic) notions of privacy when the ballot box is dishonest.

The technical details and proofs omitted due to space constraints are available in the companion technical report [? ].

PRELIMINARIES

Notations: The multiset of elements a, a, b, c is denoted {|a, a, b, c | }. The union of two multisets S 1 and S 2 is denoted S 1 ⊎ S 2 .

In both cryptographic and symbolic models, we assume a set V of votes and a set R of possible results, equipped with an associative and commutative operator * (e.g. addition of vectors). A counting function is a function ρ that associates a result r ∈ R to a multiset of votes. We assume that counting functions have a partial tally property: it is always possible to count the votes in two distinct multisets and then combine the results.

∀V ,

V ′ ρ(V ⊎ V ′ ) = ρ(V ) * ρ(V ′ ) A vote v is said to be neutral if ρ(v) is neutral w.r.t. * .
Example 2.1. Consider a finite set of candidates C = {a 1 , . . . , a k }. In case voters should select between k 1 and k 2 candidates or vote blank, we can represent valid votes by vectors representing the selection of candidates

V k 1 ,k 2 = v ∈ {0, 1} k | k 1 ≤ k i=0 v i ≤ k 2 ∪ {v blank }
where v blank is the null vector (0, . . . , 0), representing a blank vote. In a mixnet-based tally, all the individual votes are revealed. Thus R is the set of multisets of votes in V k 1 ,k 2 and * is the union of multisets. The corresponding counting function is

ρ mix (V ) = V , where V is a multiset of elements of V k 1 ,k 2 .
In an homomorphic-based tally, the votes are added together. Thus R = N k , the set of vectors of k elements, and * is the addition of vectors. The corresponding counting function is

ρ hom (V ) = v ∈V v.
Both ρ mix and ρ hom have the partial tally property. The vote v blank is a neutral vote w.r.t. ρ hom but not ρ mix .

The result of the election r may have several representations. For example, a multiset may be represented by several lists (where the order changes). In symbolic models, the result will be represented by abstract terms and we wish our result to be independent of a particular choice of representation. Therefore, we will simply say that a representation R is a function that associates to a result r ∈ R a set of possible representations with an injectivity property:

∀r r ′ . R(r ) ∩ R(r ′ ) = ∅
Intuitively, a result can be associated to several representations but a given representation can correspond to at most one result.

For our proofs in a cryptographic setting, we will also assume that given an election result r and a set of votes V , one can decide efficiently (in polynomial time) whether r includes all the votes of V , that is, whether there exists V ′ such that r = ρ(V ⊎ V ′ ). This condition is satisfied by ρ mix and ρ hom and all standard counting functions.

SYMBOLIC MODEL 3.1 Model

In symbolic models, security protocols are often modelled through a process algebra, in the spirit of the applied pi-calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF], that offers a small, abstract language for specifying communications, where messages are represented as terms. We present here a calculus inspired from the calculus underlying the ProVerif tool [START_REF] Blanchet | Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif[END_REF].

3.1.1 Terms. We consider an infinite set of names N that model fresh values such as nonces and keys. We distinguish the set FN of free nonces (generated by the attacker) and the set BN of bound nonces (generated by the protocol agents). We also assume an infinite set of variables V = X ⊎ AX where X contains variables used in processes (agent's memory) while AX contains variables used to store messages (adversary's memory). Cryptographic primitives are represented through a set of function symbols, called signature F . Each function symbol has an arity, that is, the number of its arguments. We assume an infinite set C ⊆ F of public constants, which are functions of arity 0.

Example 3.1. The standard primitives, public keys, symmetric and asymmetric encryption, concatenation, as well as addition, can be modelled by the following signature.

F c = {pk/1, enc/2, aenc/2, ⟨•, •⟩/2, +/2}
The companion primitives (symmetric and asymmetric decryption, projections) are then represented by the following signature:

F d = {dec/2, adec/2, π 1 /1, π 2 /1}
Given a signature F , a set of names N , a set of variables V, the set of terms T (F , V, N ) is the set inductively defined by applying functions to variables in V and names in N . The set of names resp. variables) occurring in t is denoted names(t) (resp. vars(t)). A Processes: P, Q ::= 0 | ν n.P for n ∈ BN (n bound in P) | out(c, M).P | in(c, x).P for x ∈ X (x bound in P) | event(M 1 , . . . , M n ).P for event ∈ Ev of arity n

| P | Q | let x = M in P for x ∈ X (x bound in P) | if M = N then P else Q | !P
where M, N , M 1 , . . . , M n are messages and c ∈ Ch is a channel. term is ground if it does not contain any variable. The set of terms T (F , AX, FN ) represents the attacker terms, that is, terms built from the messages sent on the network and stored thanks to the variables in AX.

A substitution σ = {M 1 /x 1 , . . . , M k /x k } maps variables x 1 , . . . ,

x k ∈ V to messages M 1 , . . . , M k . Its domain is denoted dom(σ ) = {x 1 , . . . , x k }.
The application of σ to a term t is denoted tσ and is defined as usual. A substitution σ is ground if its messages M 1 , . . . , M k are ground.

The properties of the cryptographic primitives are modelled through an equational theory E, which is a finite set of equations of the form M = N where M, N ∈ T (F , X, ∅) are messages without names. Equality modulo E, denoted by = E , is defined as the smallest equivalence relation on terms that is closed under context and substitution. We denote disequalities modulo E by M E N .

Example 3.2. Considering the signature F c ∪ F d ∪ C from Example 3.1, the following equational theory describes the ability to decrypt symmetrically, asymmetrically, and to project pairs. It also characterises + as an associative and commutative operator.

dec(enc(x, y), y) = x adec(aenc(x, pk(y)), y) = x π 1 (⟨x, y⟩) = x π 2 (⟨x, y⟩) = y x + (y + z) = (x + y) + z x + y = y + x 3.1.2
Processes. The behaviour of protocol parties is described through processes. Let Ch be an infinite set of channel names, representing the channels on which the messages are exchanged. All channels will be public. We consider different channels nevertheless to model the fact that an attacker can identify the provenance of a message. We also consider a finite set Ev of event symbols, given together with their arity. Events are used to record that participants have reached a certain step, with some associated knowledge. Protocols are modelled through a process algebra, whose syntax is displayed in Figure 1.

As usual, we identify processes up to α-renaming, to avoid capture of bound names and variables.

A configuration of the system is a triple (E; P; ϕ) where:

• P is a multiset of processes that represents the current active processes; • E is a set of names, which represents the private names of the processes; • ϕ is a substitution with dom(ϕ) ⊆ AX that represents the messages sent on the network. We assume ϕ to be ground, that is for any x ∈ dom(ϕ), ϕ(x) is a ground term. The semantics of processes is given through a transition relation α --→ provided in Figure 2, where α is the action associated to the transition. τ denotes a silent action. Events are recorded but will be invisible to the attacker. Intuitively, process ν n.P creates a fresh nonce, stored in E, and behaves like P. Process out(c, M).P emits M on c and behaves like P. Process in(c, x).P inputs a term computed by the attacker (that is a term built from ϕ using an attacker term) on channel c and then behaves like P. Process event(M 1 , . . . , M n ).P triggers the event event(M 1 , . . . , M n ), and then behaves like P. Process P | Q corresponds to the parallel composition of P and Q. Process let x = M in P behaves like P in which x is replaced with M. Process if M = N then P else Q behaves like P if M and N are equal modulo E, and behaves like Q otherwise. The replicated process !P behaves as an unbounded number of copies of P.

We denote by w ---→ * the reflexive transitive closure of α --→, where w is the concatenation of all actions. We also write equality up to silent actions and events = τ .

A trace of a process P is any possible sequence of transitions starting from P. Traces correspond to all possible executions in the presence of an attacker that may read, forge, and send messages. Formally, the set of traces trace(P) is defined as follows.

trace(P) = {(w, new E.ϕ)|(∅; {P }; ∅) w ---→ * (E; P; ϕ)}
A sequence of actions t is blocking in a process P if it cannot be executed. Example 3.3. Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] is a simple voting protocol used in several elections, like the election of the recteur of the university of Louvainla-Neuve. A voter simply encrypts her vote with the public key of the election. This encrypted vote forms the ballot, which is sent to the ballot box. The voter may check that her ballot is on the ballot box since the ballot box is public. There are two ways for tallying, either homomorphic tally or mixnet-based tally. We model here the two options in an abstract way: given the ballots, the talliers output the aggregation of the decryption of the ballot. This aggregation could be the addition or just the votes in a random order. For simplicity, we describe here a simple version with only two honest voters A and B, a dishonest voter C, and a voting server S. This protocol can be modelled by the following process.

blocking(t, P)

P Helios (v a , v b ) = ν k as , k bs , k cs , k e . (out(c, k cs ).out(c, pk(k e )) | Voter(A, v a , c a , c ′ a , k as , k e ) | Voter(B, v b , c b , c ′ b , k bs , k e ) | Tally Helios (c a , c b , c c , c s , k as , k bs , k cs , k e ))
where Voter(a, v, c, c ′ , k, k e ) represents voter a willing to vote for v using the channels c and c ′ , the election key k e and the credential k to authenticate to the server, while Tally Helios represents the voting server.

(E; {P 1 | P 2 } ∪ P; ϕ) τ --→ (E; {P 1 , P 2 } ∪ P; ϕ) Par (E; {0} ∪ P; ϕ) τ --→ (E; P; ϕ) Zero (E; {ν n.P } ∪ P; ϕ) τ --→ (E ∪ {n}; {P } ∪ P; ϕ) New (E; {out(c, M).P } ∪ P; ϕ) ν ax n .out(c,ax n ) ----------------→ (E; {P } ∪ P; ϕ ∪ {M/ax n }) Out if M is a ground term, ax n ∈ AX and n = |ϕ | + 1 (E; {in(c, x).P } ∪ P; ϕ) in(c, R) -------→ (E; {P[Rϕ/x]} ∪ P; ϕ) In if R is an attacker term such that vars(R) ⊆ dom(ϕ) (E; {event(M 1 , . . . , M n ).P } ∪ P; ϕ) event(M 1 , ..., M n ) ----------------→ (E; {P } ∪ P; ϕ) Event if ∀i. M i is a ground message (E; {let x = M in P } ∪ P; ϕ) τ --→ (E; {P[M/x]} ∪ P; ϕ) Let-In if M is ground (E; {if M = N then P else Q } ∪ P; ϕ) τ --→ (E; {P } ∪ P; ϕ) If-Then if M, N are ground messages such that M = E N (E; {if M = N then P else Q } ∪ P; ϕ) τ --→ (E; {Q } ∪ P; ϕ) If-Else if M, N are ground messages such that M E N (E; {!P } ∪ P; ϕ) τ --→ (E; {P, !P } ∪ P; ϕ) Repl Figure 2: Semantics Voter(a, v, c, c ′ , k, k e )
simply sends an encrypted vote. To model the fact that voters communicate with the ballot box through an authenticated channel, we assume that a voter first sends her ballot privately to the server (using the encryption with k) and then sends the ballot on a public channel. Note that the key k is just a modelling artefact to abstract away the underlying password-based authenticated channel.

Voter(a, v, c, c ′ , k, k e ) = ν r . out(c, enc(aenc(⟨v, r ⟩, pk(k e )), k)). Voted(a, v). out(c ′ , aenc(⟨v, r ⟩, pk(k e )))

The voting server receives ballots from voters A, B, and C and then outputs the decrypted ballots, after some mixing, modelled through the + operator.

Tally Helios (c a , c b , c c , c s , k as , k bs , k cs , k e ) = in(c a , x 1 ).in(c b , x 2 ).in(c c , x 3 ). let y 1 = dec(x 1 , k as ) in let y 2 = dec(x 2 , k bs ) in let y 3 = dec(x 3 , k cs ) in if x 1 x 2 ∧ x 1 x 3 ∧ x 2 x 3 then out(c s , π 1 (adec(y 1 , k e )) + π 1 (adec(y 2 , k e )) + π 1 (adec(y 3 , k e )))
where we omit the null else-branches. ∧ is syntactic sugar for a succession of tests and if M N then P is syntactic sugar for if M = N then 0 else P. Intuitively, two sequences of messages are indistinguishable to an attacker if he cannot perform any test that could distinguish them. This is typically modelled as static equivalence [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF]. Definition 3.4 (Static Equivalence). Two ground frames new E.ϕ and new E ′ .ϕ ′ are statically equivalent if and only if they have the same domain, and for all attacker terms R, S with variables in dom(ϕ) = dom(ϕ ′ ), we have

(Rϕ = E Sϕ) ⇐⇒ (Rϕ ′ = E Sϕ ′ )
Two processes P and Q are in equivalence if no matter how the adversary interacts with P, a similar interaction may happen with Q, with equivalent resulting frames. Definition 3.5 (Trace Equivalence). Let P, Q be two processes. We write P ⊑ t Q if for all (s,ψ ) ∈ trace(P), there exists (s ′ ,ψ ′ ) ∈ trace(Q) such that s = τ s ′ and ψ and ψ ′ are statically equivalent. We say that P and Q are trace equivalent, and we write

P ≈ t Q, if P ⊑ t Q and Q ⊑ t P.
Note that this definition already includes the attacker's behaviour, since processes may input any message forged by the attacker.

Example 3.6. Ballot privacy is typically modelled as an equivalence property [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] that requires that an attacker cannot distinguish when Alice is voting 0 and Bob is voting 1 from the scenario where the two votes are swapped.

Continuing Example 3.3, ballot privacy of Helios can be expressed as follows: P Helios (0, 1) ≈ t P Helios (1, 0)

Voting protocols

We consider two disjoint, infinite subsets of C: a set A of agent names or identities, and a set V of votes. We assume given a representation R of the result.

A voting protocol is modelled as a process. It is composed of:

• processes that represent honest voters;

• a process modelling the tally;

• possibly other processes, modelling other authorities.

Formally, we define a voting process as follows.

Definition 3.7. A voting process is a process of the form

P = ν # " cred.ν cred 1 . . . ν cred p . ( Voter(a 1 , v a 1 , #" c 1 , # " cred, cred 1 ) | • • • | Voter(a n , v a n , #" c n , # " cred, cred n ) | Tally p ( #" c , # " cred, cred 1 , . . . , cred p ) | Others p ( #" c ′ , # " cred, cred 1 , . . . , cred p ))
where

a i ∈ A, v a i ∈ V, #" c i , #" c , #" c ′ are (distinct) channels, # "
cred and cred i are (distinct) names.

A voting process may be instantiated by various voters and vote selections. Given A = {b 1 , . . . , b n } ⊆ A a finite set of voters, and α : A → V that associates a vote to each voter, we define P α by replacing a i by b i and v i by α(b i ) in P.

Moreover, P must satisfy the following properties.

• Process Voter(a, v a , #" c , # " cred, cred) models an honest voter a willing to vote for v a , using the channels #" c , credentials cred (e.g. a signing key) and election credentials # " cred. It is assumed to contain an event Voted(a, v) that models that a has voted for v. This event is typically placed at the end of process Voter(a, v a , #" c , # " cred, cred). This event cannot appear in process Tally p nor Others p .

• Process Tally p ( #" c , # " cred, cred 1 , . . . , cred p ) models the tally. It is parametrised by the total number of voters p (honest and dishonest), with p ≥ n. It is assumed to contain exactly one output action on a reserved channel c r . The term output on this channel is assumed to represent the final result of the election.

∀α . ∀(tr , ϕ) ∈ trace(P α ). out(c r , r ) ∈ tr ⇒ ∃V . ϕ(r ) ∈ R(ρ(V ))

Tally p may of course contain input/output actions on other channels.

• Process Others p ( #" c ′ , # " cred, cred 1 , . . . , cred p ) is an arbitrary process, also parametrised by p. It models the remaining of the voting protocol, for example the behaviour of other authorities. It also models the initial knowledge of the attacker by sending appropriate data (e.g. the public key of the election or dishonest credentials). We simply assume that it uses a set of channels disjoint from the channels used in Voter and Tally p .

The channel c r used in Tally p to publish the result is called the result channel of P.

Example 3.8. The process modelling the Helios protocol, as defined in Example 3.3 is a voting process, where process Others p consists in the output of the keys: out(c, k cs ).out(c, pk(k e )).

We can read which voters voted from a trace. Formally, given a sequence tr of actions, the set of voters Voters(tr ) who did vote in tr is defined as follows.

Voters(tr

) = {a ∈ A | ∃v ∈ V. Voted(a, v) ∈ tr }.
The result of the election is emitted on a special channel c r . It should correspond to the tally of a multiset of votes. Formally, given a trace (t, ϕ) and a multiset of votes V , the predicate result(t, ϕ, V )

holds if the election result in (t, ϕ) corresponds to V . result(t, ϕ, V ) def = ∃x, t ′ . t = t ′ .out(c r , x) ∧ ϕ(x) ∈ R(ρ(V )).

Security properties

Several definitions of verifiability have been proposed. In the lines of [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF][START_REF] Küsters | Accountabiliy: Definition and Relationship to Verifiability[END_REF], we consider a very basic notion, that says that the result should at least contain the votes from honest voters. Definition 3.9 (symbolic individual verifiability). Let P be a voting process with result channel c r . P satisfies symbolic individual verifiability if, for any trace (t, ϕ) ∈ trace(P α ) of the form t ′ .out(c r , x)), there exists V c such that the result in t corresponds to

V a ⊎ V c , that is result(t, ϕ, V a ⊎ V c ), where V a = {|v | ∃a. Voted(a, v) ∈ t | }
Individual verifiability typically guarantees that voters can check that their ballot will be counted. Our notion of individual verifiability goes one step further, ensuring that the corresponding votes will appear in the result, even if the tally is dishonest. One of the first definitions of verifiability was given in [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF], distinguishing between individual, universal, and eligibility verifiability. Intuitively, our own notion of individual verifiability sits somewhere between individual verifiability and individual plus universal verifiability as defined in [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF]. A precise comparison is difficult as individual and universal verifiability are strongly tight together in [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF]. Moreover, [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF] only considers the case where all voters are honest and they all vote.

We consider the privacy definition proposed in [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] and widely adopted in symbolic models: an attacker cannot distinguish when Alice is voting v 1 and Bob is voting v 1 from the scenario where the two votes are swapped. Definition 3.10 (Privacy [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF]). Let P be a voting process. P satisfies privacy if, for any subtitution α from voters to votes, for any two voters a, b ∈ A\dom(α) and any two votes v 1 , v 2 ∈ V, we have

P α ∪{a →v 1 ,b →v 2 } ≈ P α ∪{a →v 2 ,b →v 1 }

Privacy implies verifiability

We show that privacy implies verifiability under a couple of assumptions, typically satisfied in practice.

First, we assume a light form of determinacy: two traces with the same observable actions yield the same election result. This excludes for example cases for voters chose non deterministically how they vote. Formally, we say that a voting process P with election channel c r is election determinate if, for any substitution α from voters to votes, for any two traces t, t ′ such that t = τ t ′ , (t .out(c r , x), ϕ) ∈ trace(P α ), and (t ′ .out(c r , x), ϕ ′ ) ∈ trace(P α ), then

ϕ(x) ∈ R(ρ(V ))) ⇒ ϕ ′ (x) ∈ R(ρ(V ))
This assumption still supports some form of non determinism but may not hold for example in the case where voters use anonymous channels that even hide who participated in the election.

Second, we assume that it is always possible for a new voter to vote (before the tally started) without modifying the behaviour of the protocol. Formally, a voting proces P is voting friendly if for all voter a ∈ A, there exists t ′′ (the honest voting trace) such that for all α satisfying a dom(α),

• for all (t, ϕ) ∈ trace(P α ), such that t = t ′ .out(c r , x) for some t ′ , x, for all v, there exists tr , ψ such that tr = τ t ′′ , Voted(a, v) ∈ tr , (t ′ .tr .out(c r , x),ψ ) ∈ trace(P α ∪{a →v } ), and

∀V . ϕ(x) ∈ R(ρ(V )) ⇒ ψ (x) ∈ R(ρ(V ∪{v})).
Intuitively, if a votes normally, her vote will be counted as expected, no matter how the adversary interfered with the other voters. • for all t ′ , x such that blocking(t ′ .out(c r , x), P α ), for all v, tr , ψ such that tr = τ t ′′ , we have blocking(t ′ .tr .out(c r , x), P α ∪{a →v } ). Intuitively, the fact that a voted does not suddenly unlock the tally. In practice, most voting systems are voting friendly since voters vote independently. In particular, process P Helios modelling Helios, as defined in Example 3.3, is voting friendly (assuming an honest tally). The voting friendly property prevents a fully dishonest tally since the first item requires that unmodified honest ballots are correctly counted. However, we can still consider a partially dishonest tally that, for example, discards or modifies ballots that have been flagged by the attacker.

Moreover, we assume that there exists a neutral vote, which is often the case in practice. Actually, this is a simplified (sufficient) condition. Our result also holds as soon as there is a vote that can be counted separately from the other votes (as formally defined in a companion technical report [? ]). Theorem 3.11 (Privacy implies individual verifiability). Let P be a voting friendly, election determinate voting process.

If P satisfies privacy then P satisfies individual verifiability.

The proof of this result intuitively relies on the fact that in order to satisfy privacy w.r.t. two voters Alice and Bob, a voting process has to guarantee that the vote of Alice is, if not correctly counted, at least taken into account to some extent. Indeed, if an attacker, trying to distinguish whether Alice voted for 0 and Bob for 1, or Alice voted for 1 and Bob for 0, is able to make the tally ignore completely the vote of Alice, the result of the election is then Bob's choice. Hence the attacker learns how Bob voted, which breaks privacy.

Therefore, we first we prove that if a protocol satisfies privacy, then if we compare an execution (i.e. a trace) where Alice votes 0 with the corresponding execution where Alice votes 1, the resulting election results must differ by exactly a vote for 0 and a vote for 1. Formally, we show the following property. Lemma 3.12. If a voting friendly, election determinate voting process P satisfies privacy, then it satisfies

[ t = τ t ′ ∧ (t, ϕ) ∈ trace(P α ∪{a →v 1 } ) ∧ (t ′ , ϕ ′ ) ∈ trace(P α ∪{a →v 2 } ) ∧ result(t, ϕ, V ) ∧ result(t ′ , ϕ ′ , V ′ ) ] =⇒ ρ(V ′ ⊎ {|v 1 | }) = ρ(V ⊎ {|v 2 | }).
This lemma is used as a central property to prove the theorem. Intuitively, we apply this lemma repeatedly, changing one by one all the votes from honest voters into neutral votes. Let r denote the result before this operation, and r ′ the result after. Let V a denote the multiset of honest votes, and V b the multiset containing the same number of neutral votes. Thanks to Lemma 3.12, we can show that r * ρ(V b ) = r ′ * ρ(V a ). Since V b only contains neutral votes, we have r = r ′ * ρ(V a ). This means that r contains all honest votes, hence the voting process satisfies individual verifiability.

The detailed proof of this theorem can be found in a companion technical report [? ].

COMPUTATIONAL MODEL

Computational models define protocols and adversaries as probabilistic polynomial-time algorithms.

Notation: We may write (id, * ) ∈ L as a shorthand, meaning that there exists an element of the form

(id, x) in L. If V is a multiset of elements of the form (id, v), we define ρ(V ) = ρ({|v | (id, v) ∈ V | }).

Voting system

We assume that the ballot box displays a board BB, that is a list of ballots. The nature of the ballots depend on the protocol we consider.

Definition 4.1. A voting scheme consists in six algorithms (Setup, Credential, Vote, VerifVoter, Tally, Valid)

• Setup(1 λ ), given a security parameter λ, returns a pair of election keys (pk, sk). • Credential(1 λ , id) creates a credential cred for voter id, for example a signing key. The credential may be empty as well.

Registered voters are stored in a list U. • Vote(id, cred, pk, v) constructs a ballot containing the vote v for voter id with credential cred, using the election public key pk. • VerifVoter(id, cred, L, BB) checks whether the local knowledge L of voter id is consistent with the board BB. For example, a voter may check that her (last) ballot appears on the bulletin board. • Tally(BB, sk, U) computes the tally of the ballots on the board BB, using the election secret key sk, assuming a list of registered voter identities and credentials U. The Tally algorithm first runs some test ValidTally(BB, sk, U) that typically checks that the ballots of BB are valid. Tally may return ⊥ if the tally procedure fails (invalid board or decryption failure for example). If Tally(BB, sk, U) ⊥ then it must correspond to a valid result, that is, there exists V such that Tally(BB, sk, U) = ρ(V ). • Valid(id, b, BB, pk) checks that a ballot b cast by a voter id is valid with respect to the board BB using the election public key pk. For example, the ballot b should have a valid signature or valid proofs of knowledge. The ballot b will be added to BB only if Valid(id, b, BB, pk) succeeds.

We will always assume a correct voting scheme, that is, tallying honestly generated ballots yields the expected result. Formally, for all distinct identities U = id 1 , . . . , id n , and credentials cred 1 , . . . , cred n , for all votes v 1 , . . . , v n , for all election keys (pk, sk),

if BB = [Vote(id i , cred i , pk, v i )|i ∈ 1, n ], then Tally(BB, sk, U) = ρ({|v 1 , . . . , v n | })
The tally algorithm typically applies a revote policy. Indeed, if voters may vote several times, the revote policy states which vote should be counted. The two main standard revote policies are 1. the last vote counts or 2. the first vote counts (typically when revote is forbidden). In what follows, our definitions are written assuming the last ballot revote policy. However, they can easily be adapted to the first ballot revote policy and all our results hold in both cases (as shown in a companion technical report [? ]).

The revote policy is either based on the identities or the credentials. We say that a voting system is id-based if there exists a a function open id which, given a ballot b, retrieves the associated identity. Formally, for any id, cred, pk, v, open id (Vote(id, cred, pk, v)) = id Similarly, we say that a voting system is cred-based if there exists a function open cred which, given a ballot b, the election secret key sk, and a list U of registered voters and credentials, retrieves the credential cred used by the voter to create the ballot. Formally, for any id, cred, sk, pk, v, open cred (Vote(id, cred, pk, v), sk, U ) = cred Note that some schemes are neither id-based nor cred-based, in particular when the ballots contain no identifier. Such schemes typically assume that voters do not revote since there is no means to identify whether two ballots originate from the same voter.

Security properties

As usual, an adversary is any probabilistic polynomial time Turing machine (PPTM). We define verifiability and privacy through gamebased properties.

Verifiability.

For verifiability, we propose a simple definition, inspired from [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF][START_REF] Küsters | Accountabiliy: Definition and Relationship to Verifiability[END_REF]. Intuitively, we require that the election result contains at least the votes of all honest voters. This notion was called weak verifiability in [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF] but we will call it individual verifiability to match the terminology used in symbolic settings. More sophisticated and demanding definitions have been proposed, for example controlling how many dishonest votes can be inserted [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF] or tolerating some variations in the result [START_REF] Küsters | Accountabiliy: Definition and Relationship to Verifiability[END_REF]. The main missing part (in terms of security) is that our definition does not control ballot stuffing: arbitrarily many dishonest votes may be added to the result. The reason is that ballot stuffing seems unrelated to privacy. Moreover, our definition assumes an honest tally, and thus does not capture universal verifiability aspects. The main reason is that existing privacy definitions in computational settings assume an honest tally and we compare the two notions under the same trust assumptions. We leave as future work to determine how to extend these two definitions to a dishonest tally, and whether the implication still holds.

Verifiability is defined through the game Exp verif A (λ) displayed on Figure 4. In a first step, the adversary may use oracles O reg (id) and O corr (id) (defined on Figure 3) to respectively register a voter and get her credential (in this case, the voter is said to be corrupted). Then the adversary may ask an honest voter id to vote for a given vote v through oracle O v vote (id, v). In this case, the adversary sees the corresponding ballot and the fact that id voted for v is registered in the list Voted. The adversary may also cast an arbitrary ballot b in the name of a dishonest voter id through oracle O cast (id, b).

Finally, the adversary wins if the election result does not contain

O reg (id) if (id, * ) ∈ U then stop else cred id ← Credential(1 λ , id) U ← U ∥(id, cred id ) O corr (id) if (id, * ) U ∨ (id, * ) ∈ CU then stop else CU ← CU ∥(id, cred id ) return cred id
where (id, cred id ) ∈ U

Definition 4.2 (Individual verifiability). A voting system is individually verifiable if for any adversary A,

P Exp verif A (λ) = 1 is negligible.
As mentioned in introduction, [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] shows an impossibility result between (unconditional) privacy and verifiability. [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] considers another aspect of verifiability, namely universal verifiability, that is, the guarantee that the result corresponds to the content of the ballot, even in presence of a dishonest tally. Interestingly, the same incompatibility result holds between individual verifiability and unconditional privacy, for the same reasons. Exactly like in [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF], a powerful adversary (i.e. not polynomial) could tally BB and BB ′ where BB ′ is the ballot box from which Alice's ballot has been removed and infer Alice's vote by difference. More generally, unconditional privacy is lost as soon as there exists a tally function that is meaningfully related to the result, which is implied by individual verifiability.

Privacy.

For privacy, we consider the old, well established definition of Josh Benaloh [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF]. More sophisticated definitions are been proposed later (see [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF] for a survey and a unifying definition). They aim in particular at getting rid of the partial tally assumption (needed in [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF]). Note however that they all assume an honest ballot box. Since we also assume partial tally, the original Benaloh definition is sufficient for our needs. In particular, we do not know if privacy implies verifiability for counting functions that do not have the partial tally property. This is left as future work.

Intuitively, a voting system is private if, no matter how honest voters vote, the adversary cannot see any difference. However, the adversary always sees the election result, that leaks how the group of honest voters voted (altogether). Therefore, the election result w.r.t. the honest voters has to remain the same. More formally, in a first step, the adversary uses oracles O reg (id) and O corr (id) to respectively register a voter and get her credential. Then the adversary may request an honest voter id to vote either for v 0 or v 1 through oracle O p vote (id, v 0 , v 1 ). Voter id will vote v β depending on the bit β. The adversary may also cast an arbitrary ballot b in the name of a dishonest voter id through oracle O cast (id, b). The election will be tallied, only if the set V 0 of votes v 0 yields the same result than the set V 1 of votes v 1 (where only the last vote is counted). Finally, the adversary wins if he correctly guesses β. Formally, privacy is defined through the game Exp priv, β A (λ) displayed on Figure 5. ). A voting system is private if for any adversary A,

Exp verif A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state ← A Oreg, Ocorr 1 (pk) BB, Voted ← [] A O v vote , O cast 2 (state, pk) r ← Tally(BB, sk, U) if r ⊥ ∧ ∀V c (finite) . r ρ({v i } 1≤i ≤k ⊎ V c ) then return 1 where Voted = {(id 1 , v 1 ), . . . , (id k , v k )} O v vote (id, v) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v) BB ← BB ∥b Voted ← Voted ′ ∥(id, cred id , v)
P Exp priv,0 A (λ) = 1 -P Exp priv,1 A (λ) = 1 is negligible.

Privacy implies individual verifiability

We show that privacy implies individual verifiability and we first list here our assumptions. As for the symbolic case, we assume the existence of a neutral vote. We also require that the tally can be performed piecewise, that is, informally, as soon as two boards BB 1 , BB 2 are independant then Tally(BB 1 ⊎ BB 2 ) = Tally(BB 1 ) * Tally(BB 2 ). This property is satisfied by most voting schemes. Formally, we characterize this notion of "independence" depending on whether a scheme is id-based or cred-based.

An id-based voting scheme has the piecewise tally property if for any two boards BB 1 and BB 2 that contain ballots registered for different agents and such that BB 1 ⊎ BB 2 is valid, that is, if

ValidTally(BB 1 ⊎ BB 2 , sk, U) ∧ ∀b ∈ BB 1 . ∀b ′ ∈ BB 2 . open id (b) open id (b ′ ),
then their tally can be computed separately:

Tally(BB 1 ⊎ BB 2 , sk, U) = Tally(BB 1 , sk, U) * Tally(BB 2 , sk, U). (*)
We also assume that the tally only counts ballots cast with registered ids, i. Similarly, a cred-based voting scheme has the piecewise tally property if for any two boards BB 1 and BB 2 that contain ballots associated to different credentials, that is ∀b

∈ BB 1 . ∀b ′ ∈ BB 2 . open cred (b, sk, U) open cred (b ′ , sk, U)
then their tally can be computed separately (Property (*)). We also assume that registering more voters does not change the tally: if U, U ′ share no credentials and ∀b ∈ BB. ( * , open cred (b, sk, U∪ U ′ )) U ′ , then Tally(BB, sk, U) = Tally(BB, sk, U ∪ U ′ ).

We say that a (id-based) voting scheme is strongly correct if whatever valid board the adversary may produce, adding a honestly generated ballot still yields a valid board. This property is formally defined through the game Exp

ValidTally A (λ) displayed in Figure 6. A similar assumption was introduced in [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF]. For example, Helios is strongly correct.

A voter credential typically includes a private part used to generate a signing key for example. It should not be possible for an adversary to forge a ballot with an honest credential. Formally, we say that a voting scheme has non-malleable credentials, if for any adversary A,

P Exp NM A (λ) = 1 is negligible
where Exp NM A (λ) is defined on Figure 7. For example, Belenios and Civitas have non-malleable credentials. Theorem 4.4 (Privacy implies individual verifiability). Let V be an id-based, strongly correct, voting scheme that has the piecewise tally property. If V is private, then V is individually verifiable.

Similarly, let V be a cred-based voting scheme that has the piecewise tally property and non-malleable credentials. If V is private, then V is individually verifiable.

The proof of this theorem is inspired by the same intuition as in the symbolic case: if an attacker manages to break verifiability, that is, to obtain that not all votes from the honest voters are counted correctly, then there also exists an attack against privacy. Indeed, consider a scenario with additional, new voters, whose votes should compensate those cast by the initial voters. By performing the attack on verifiability for the initial voters, the attacker reaches a state where, in the result of the election, they are no longer compensated by the new votes. This allows the attacker to break privacy.

More precisely, the general idea of the proof is as follows. Consider an attacker A that breaks individual verifiability, i.e. wins the game Exp verif with non negligible probability. We construct an attacker B that breaks privacy, i.e. wins Exp priv, β . B starts by registering, and corrupting, the same voters as A, using oracles O reg and O corr . Let id 1 , . . . , id n be this first set of voters. B then registers another set of n voters id ′ 1 , . . . , id ′ n , where the id ′ i are fresh identities, that A does not use.

B then simulates A, using the oracle O p vote to simulate A's calls to O v vote . Specifically, when A calls O v vote (id, v), B calls the oracle O p vote (id, v, v blank ), where v blank is a neutral vote. Once B is done simulating A, it triggers the new voters id ′ i to vote, by calling

Exp priv, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) BB, V 0 , V 1 ← [] state 2 ← A O p vote , O cast 2 (state 1 , pk) if ρ(V 0 ) = ρ(V 1 ) then r ← Tally(BB, sk, U) β ′ ← A 3 (state 2 , pk, r ) return β ′ O p vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) BB ← BB ∥b V 0 ← V ′ 0 ∥(id, v 0 ) V 1 ← V ′ 1 ∥(id, v 1 ) return b where (id, cred id ) ∈ U and V ′ 0 (resp. V ′ 1 ) is obtained from V 0 (resp. V 1 ) by removing all instances of (id, * ) O cast (id, b) if (id, * ) ∈ CU ∧ Valid(id, b, BB, pk) then BB ← BB ∥(id, b) Figure 5: Privacy Exp ValidTally A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state ← A Oreg, Ocorr 1 (pk) (BB, id, v) ← A O v t vote 2 (state, pk) b ← Vote(id, cred id , pk, v) where (id, cred id ) ∈ U if (id, * ) ∈ U\CU ∧ (∀b ′ ∈ BB. open id (b ′ ) id) ∧ ValidTally(BB, sk, U) ∧ ¬ValidTally(BB| |b, sk, U) then return 1 O vt vote (id, v) if ∃cred id .(id, cred id ) ∈ U\CU then return Vote(id, cred id , pk, v) Figure 6: ValidTally game Exp NM A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state ← A Oreg, Ocorr 1 (pk) L ← [] b ← A Oc 2 (state, pk) if b L ∧ ∃(id, cred id ) ∈ U\CU. open cred (b, sk, U ) = cred id then return 1 O c (id, v) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v) L ← L ∥b return b
where (id, cred id ) ∈ U

p vote (id ′ i , v blank , v i )
, where v i is the (last) vote cast by id i . The vote of each id ′ i compensates the vote of id i , so that the condition ρ(V 0 ) = ρ(V 1 ) from Exp priv holds. B then obtains the result r of the election, which is equal to r 1 * r 2 , where r 1 is the tally of the ballots cast by A, and r 2 the tally of the additional ballots cast by B. Then:

• if β = 0: then all the votes cast by the id ′ i were v blank , and the result is thus r = r 1 . Since A breaks individual verifiability, r 1 does not contain the honest votes, i.e., for all multiset V c of votes, r ρ(v 1 , . . . , v n ) * ρ(V c ).

• if β = 1 however, the votes cast by the id ′ i were the v i , and the partial tally r 2 is therefore r 2 = ρ(v 1 , . . . , v n ). Hence, the result r does contain the honest votes. Therefore, by observing whether the final result of the election contains the honest votes, B is able to guess β, and wins Exp priv .

PRIVACY WITH A DISHONEST BOARD

Our main theorem states that privacy implies individual verifiability. However, the privacy definition introduced by Benaloh assumes an honest ballot box, as most existing privacy definitions of the literature [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF]. Therefore, our main theorem shows that whenever a voting scheme is private w.r.t. an honest ballot box, then it is also individually verifiable w.r.t. an honest ballot box, which is of course a rather weak property. However, intuitively, our proof technique does not rely on the trust assumptions.

As pointed out in introduction, extending cryptographic privacy definitions to a dishonest ballot box is difficult. Consider the natural extension of privacy as displayed in Figure 8: the game is the same than Exp priv, β A (λ) except that the adversary arbitrarily controls the ballot box. Unfortunately, an adversary can always win this new game. Indeed, he may simply query O d vote (id 1 , 0, 1) and O d vote (id 2 , 1, 0), yielding respectively ballots b id 1 and b id 2 . Then the adversary choses BB = b id 1 . The tally will return β, hence the adversary wins. This corresponds to the fact that an adversary may always isolate a voter and break her privacy.

Privacy with careful voters

To solve this issue, we choose another approach, which consists in explicitly modelling the verification steps made by voters: the tally will be performed only if honest voters have successfully run their checks (e.g. checking that their ballot belongs to the bulletin board). Therefore, we extend the privacy game as follows. The adversary arbitrarily controls the ballot box and may request honest voters to vote through O p,c vote (id, v 0 , v 1 ) as before. Note that there is no need for the O cast oracle since the adversary may add directly his own

Exp dis, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) V 0 , V 1 ← [] state 2 , BB ← A O d vote 2 (state 1 , pk) if ρ(V 0 ) = ρ(V 1 ) then
r ← Tally(BB, sk, U)

β ′ ← A 3 (state 2 , pk, r ) return β ′ O d vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) V 0 ← V ′ 0 ∥(id, v 0 ) V 1 ← V ′ 1 ∥(id, v 1 ) return b where (id, cred id ) ∈ U and V ′ 0 (resp. V ′ 1 ) is obtained from V 0 (resp. V 1 )
by removing all instances of (id, * ) To run her verification test (using algorithm VerifVoter), the voter has access to the ballot box BB forged by the adversary as well as her local state L id that contains in particular her previously generated ballots. The tally is performed only if all honest voters have successfully performed their test and if, as previously, the set V 0 of left votes v 0 yields the same result than the set V 1 of right votes v 1 . Formally, privacy with careful voters is defined through the game Exp priv-careful displayed on Figure 9. Definition 5.1 (Privacy with careful voters). A voting system is private against a dishonest board with careful voters if for any adversary A,

P Exp priv-careful,0 A (λ) = 1 -P Exp priv-careful,1 A (λ) = 1 is negligible.
While this definition models a dishonest ballot box, it implicitly assumes that all voters see the same (possibly dishonest) ballot box. This is a very common assumption in voting, that needs to be achieved by external means.

Similarly, we extend individual verifiability to individual verifiability against a dishonest board as expected, assuming that the tally is performed only if all honest voters have successfully performed their test. The formal definition of individual verifiability against a dishonest board can be found in a companion technical report [? ].

Privacy implies individual verifiability against a dishonest box too

We need to assume that the verification test run by honest voters (VerifVoter) is consistent with how the voter voted. Namely, if the voter's intended ballot is the one that is selected from the board by the revote policy (e.g. appears last w.r.t. this voter), then this voter must be satisfied with the board (that is, VerifVoter passes). Conversely, if the test VerifVoter fails for voter id then adding ballots unrelated to id (or her credential) will not change this fact (VerifVoter will still fail). These assumptions are formally stated in a companion technical report [? ].

Theorem 5.2 (Privacy implies individual verifiability against a dishonest board). Let V be an id-based, strongly correct voting scheme that has the piecewise tally property. If V is private against a dishonest board with careful voters, then V is individually verifiable against a dishonest board with careful voters.

Exp priv-careful, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) V 0 , V 1 , L id (for all id in U) ← [] state 2 , BB ← A O p,c vote 2 (state 1 , pk) H ← [] state 3 ← A O happy BB 3 (state 2 ) if ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H and ρ(V 0 ) = ρ(V 1 ) then r ← Tally(BB, sk, U) else r ← ⊥ β ′ ← A 4 (state 3 , pk, r ) return β ′ O p,c vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) V 0 ← V ′ 0 ∥(id, v 0 ) V 1 ← V ′ 1 ∥(id, v 1 ) L id ← L id ∥(b, v β ) return b where (id, cred id ) ∈ U and V ′ 0 (resp. V ′ 1 ) is obtained from V 0 (resp. V 1 )
Similarly, let V be a cred-based voting scheme that has the piecewise tally property and non-malleable credentials. If V is private against a dishonest board with careful voters, then V is individually verifiable against a dishonest board with careful voters.

COMPARING PRIVACY

We compare different notions of privacy, with and without an honest ballot box, on four standard protocols (Helios, Belenios, Civitas, and Neuchâtel) as well as on our simple protocol, sketched in introduction.

To our knowledge, the only other definition of privacy with a dishonest ballot box is the privacy notion introduced by Bernhard and Smyth [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF]. We first start by discussing this definition.

PrivacyBS

The privacy notion introduced by Bernhard and Smyth [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] is recalled in Figure 10 (PrivacyBS). The adversary may request a voter id to vote for v 0 or v 1 (depending on the bit β) through the oracle O bs vote (id, v 0 , v 1 ). He produces an arbitrary ballot box BB and the tally will be performed provided that, looking at honest ballots that appear in BB, counting the corresponding left and right votes yields the same result.

The main interest of [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] is to highlight the fact that previous definitions implicitly assume an honest ballot box. The first attempt at defining privacy w.r.t. a dishonest ballot box (PrivacyBS) has several limitations. First, it strongly assumes that the ballots that appear in the ballot box are exactly the same than the cast ballots. This is not

Exp BS, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) L ← [] state 2 , BB ← A O bs vote 2 (state 1 , pk) if ∀v . | {b |b ∈ BB ∧ ∃v ′ . (b, v, v ′ ) ∈ L} | = | {b |b ∈ BB ∧ ∃v ′ . (b, v ′ , v) ∈ L} | then r ← Tally(BB, sk, U) β ′ ← A 3 (state 2 , pk, r ) return β ′ O bs vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) L ← L ∥(b, v 0 , v 1 ) return b
where (id, cred id ) ∈ U the case for example of the ThreeBallots protocol [START_REF] Rivest | Three Voting Protocols: ThreeBallot, VAV and Twin[END_REF] where the ballot box only contains two shares (out of three) of the original ballot. It is not applicable either to a protocol like BeleniosRF [START_REF] Chaidos | BeleniosRF: A Non-interactive Receipt-Free Electronic Voting Scheme[END_REF] where ballots are re-randomised before their publication. Second, it requires ballots to be non-malleable [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF]. This means that, as soon as a ballot includes a malleable part (for example the voter's id like in Helios, or a timestamp), privacy cannot be satisfied. This severely restricts the class of protocols that can be considered. Third, Pri-vacyBS does not account for a revote policy. As soon as revote is allowed (for example in Helios), then PrivacyBS is broken since some ballots may not be counted. Indeed, an attacker may call O bs vote (id 1 , 1, 0), followed by O bs vote (id 1 , 0,

∈ BB|∃v ′ . (b, v, v ′ ) ∈ L}| = |{b ∈ BB|∃v ′ . (b, v ′ , v) ∈ L}| = 1 where L = [(b 1 , 1, 0), (b ′ 1 , 0, 1)].
Hence the tally is computed. According to the revote policy, only b ′ 1 is counted, and the result is β, which lets the attacker win Exp BS .

Protocols

We consider four standard protocols (Helios, Belenios, Civitas, and Neuchâtel) as well as our simple protocol, presented in introduction. We briefly explain each of them in this section. In what follows E = (gen, enc, dec) denotes an encryption algorithm.

Simple. We detail the simple protocol sketched in introduction. Recall that voters simply send their encrypted votes to the ballot box, and, at the end of the voting phase, the tally computes and publishes the result of the election. No revote is allowed, and the voters do not have any means of verifying that their vote is taken into account. Identities and credentials are not used in this protocol. The corresponding algorithms of this protocol are:

• Vote(id, cred, pk, v) = enc(pk, v)

• VerifVoter(id, cred, L, BB) = true (voters do not make any checks)

• Tally(BB, sk, U) checks that all the ballots in BB are distinct, and returns ⊥ if not. The tally performs a random permutation of the ballots, decrypts all of them and returns the multiset of the votes they contain. • Valid(id, b, BB, pk) checks that b does not already occur in BB.

Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] is similar to Simple, except that revote is allowed, and the last vote cast by each id is counted. To make this revote policy possible, the ballots contain the id of the voter: Vote(id, cred, pk, v) = (id, enc(pk, v)). enc(pk, v) here also includes a proof that v is a valid vote. Credentials are unused. The tally computes the result of the election similarly to Simple except that it also features an homomorphic mode, where the tally homomorphically computes the sum of the ballots in BB, decrypts the resulting ciphertext and returns the result. Moreover, the tally returns a proof of correct decryption. In addition, the board which will be tallied is made public, allowing the voters to check that their last ballot is indeed the last ballot with their id on the board:

VerifVoter(id, cred, L id , BB) = the last element in L id is the last ballot registered for id in BB.

Similarly to Simple, the Valid function checks that there is no duplicated ciphertext and also checks that the ballot is submitted under the right id.

Valid(id, (id ′ , c), BB, pk) = (id = id ′ ) ∧ c does not occur in BB

This models an authenticated channel between the ballot box and each voter: a voter id may not cast a vote in the name of id ′ .

Belenios [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF] is similar to Helios, except that voters sign their encrypted vote thanks to their credential:

Vote(id, k, pk, v) = (id, signElGamal(v, pk, k))

where signElGamal(•, •, •) denotes the combination of the (ElGamal) encryption and the signature. As for Helios, it also includes a proof that v is a valid vote. Tally checks that there exists a bijection between the ids and the credentials in the final board, i.e. that the same id is always associated with the same signature, and vice versa. The revote policy counts the last ballot corresponding to a given credential. Voters can verify that their last ballot is indeed the last one signed by their key on the board.

Civitas [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF]. In Civitas, voters privately receive a credential, that is published encrypted on the bulletin board. To cast a vote, a voter encrypts her vote, also encrypts her credential, and produces a proof π of well-formedness that links the two ciphertexts together. The corresponding ballot is of the form Vote(id, cred, pk, v) = (enc(pk, cred), enc(pk, v), π ).

The voters can verify that their vote will be taken into account by checking that it is present on the board that will be tallied.

VerifVoter(id, cred, L id , BB) = b ∈ BB
where b is the ballot in L id . In theory, revote is allowed. However, we unveil a small discrepancy in how revote should be performed. highly cumbersome for an average voter and we could not find its description in [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF]. Therefore, we simply assume here that honest voters do not revote.

Neuchâtel [START_REF] Galindo | 2015 Neuchâtel's Castas-Intended Verification Mechanism[END_REF]. Voters privately receive a code sheet, where each candidate is associated to a (short) code. To cast a vote, voters send their encrypted votes to the ballot box, similarly to Simple or Helios. The ballot box then provides a return code allowing the voter to check that the ballot has been received and that it encrypts their candidate, as intended. This offers a protection against a dishonest voting client (e.g. if the voter's computer is corrupted). No revote is allowed. Since the bulletin board is not published, voters cannot check that their ballots really belong to the final board (used for tally), which we model by VerifVoter(id, cred, L, BB) = true . Voters have to trust the voting server (or other internal components) on this aspect.

Attacks

Simple. As described in introduction, a dishonest ballot box may break ballot privacy of any voter by simply replacing the other votes by votes of its choice. In other words, even if the ballot box does not detain any decryption key, it can learn how Alice's voted.

Neuchâtel. Exactly like the Simple protocol, a dishonest ballot box may break ballot privacy of any voter by simply replacing the other votes. This is due to the fact that voters have no control over the ballots that are actually tallied. Note that the Neuchâtel protocol actually includes internal mechanisms that render such an attack difficult. However, from the point of view of a voter, if the ballot box is compromised, her privacy is no longer guaranteed.

Helios. Helios is also vulnerable to an attack when the ballot box is compromised. This attack is due to P. Roenne [START_REF] Roenne | [END_REF]. It involves two honest voters id 1 , id 2 , and a dishonest voter id 3 . The attacker may call O Belenios and Civitas remain private against a dishonest board as long as voters perform their verification checks. We formally prove privacy according to our definition Priv-careful.

Comparison

We summarise our findings in Figure 11. As explained in Section 5, the naive extension of the privacy definition to a dishonest board (PrivDis-Naive) is immediately false for any protocol.

All of our five protocols satisfy privacy against an honest ballot box. We rely here on previous results of the literature, except for Civitas (and of course the Simple protocol). Indeed, Civitas has been proved to be coercion-resistant [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF] in a rather different setting. Therefore we show here that it satisfies the Benaloh definition.

PrivacyBS fails to detect the attack on the Neuchâtel protocol and the Simple protocol since it requires that the tally of the honest ballots present on the final board does not leak information. Conversely, it cannot prove Belenios private as it does not properly handle revoting as explained in Section 6.1.

CONCLUSION

We show a subtle relation between privacy and verifiability, namely that privacy implies individual verifiability, which is rather counterintuitive. Our result holds in a cryptographic as well as a symbolic setting, for various trust assumptions. In contrast, privacy does not seem to imply universal verifiability nor eligibility verifiability. To show that there is indeed no implication, we plan to exhibit counter-examples, as simple as possible.

Our result assumes counting functions that have the partial tally property. Our proof technique does not extend immediately to more complex counting functions such as STV or Condorcet. We plan to study how privacy and individual verifiability are related in this context. Also, our results implicitly discard anonymous channels: computational models do not account for anonymous channels while our election determinism assumption discards at least some use of anonymous channels. Intuitively, in presence of anonymous channels, an attacker may be able to modify a ballot without being able to tell which one, hence breaking verifiability without breaking privacy. It would be interesting to identify which kind of anonymous channels and more generally, which form of non determinism, can still be tolerated.

Our findings also highlight a crucial need for a ballot privacy definition in the context of a dishonest ballot box, in a cryptographic setting. So far, privacy has only been proved assuming an honest ballot box, which forms a very strong trust assumption that was probably never made clear to voters nor election authorities.

We propose a first attempt at modelling privacy against a dishonest board, assuming that honest voters checks their ballots as expected by the voting protocol. We do not see our definition as final. In particular, assuming that all voters check their vote is highly unrealistic. In a realistic setting, it is more likely that a (small) fraction of honest voters perform the required tests while the others stop after casting their vote. We plan to explore how to adapt our definition to a quantitative setting, in the lines of [START_REF] Küsters | Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study[END_REF].

Figure 1 :

 1 Figure 1: Syntax for processes.

def=

  ∀ϕ. (t, ϕ) trace(P).

3. 1 . 3

 13 Equivalence. Sent messages are stored in a substitution ϕ while private names are stored in E. A frame is simply an expression of the form new E.ϕ where dom(ϕ) ⊆ AX. It represents the knowledge of an attacker. We define dom(new E.ϕ) as dom(ϕ).

Figure 3 :

 3 Figure 3: Registration and corruption oracles

Figure 4 : Verifiability Definition 4 . 3 (

 443 Figure 4: Verifiability

  e. ∀BB, sk, U. Tally(BB, sk, U) = Tally(BB ′ , sk, U) where BB ′ = [b ∈ BB | (open id (b), * ) ∈ U]; and that registering more voters does not change the tally: if U, U ′ have no id in common and ∀b ∈ BB. (open id (b), * ) U ′ , then Tally(BB, sk, U) = Tally(BB, sk, U ∪ U ′ ).

Figure 7 :

 7 Figure 7: Credential non-malleability

Figure 8 :

 8 Figure 8: Privacy against a dishonest board (PrivDis-Naive)

Figure 9 :

 9 Figure 9: Privacy game against a dishonest board with careful voters (Priv-careful)

Figure 10 :

 10 Figure 10: PrivacyBS [9]

  1), obtaining ballots b 1 , b ′ 1 , and return the board BB = [b 1 , b ′ 1 ]. The equality condition on the number of ballots in BB produced by O bs vote holds, since for v = 0, 1: |{b

  1 , 0, 1) twice and O p,c vote (id 2 , 1, 0) once, obtaining ballots (id 1 , b 1 ), (id 1 , b ′ 1 ), (id 2 , b 2 ). The adversary then returns the board [(id 1 , b ′ 1 ), (id 2 , b 2 ), (id 3 , b 1 )]. All ballots are different, hence no weeding is needed. The result of the tally is then ρ({|0, 1, 0| }) if β = 0 and ρ({|1, 0, 1| }) if β = 1. The attacker can therefore observe the difference in the result, which breaks privacy.

  (id, cred id ) ∈ U\CU then if VerifVoter(id, cred id , L id , BB) then H ← H ∥id

	by
	removing all instances
	of (id, * )
	O happy BB (id)

if

  Assume for example that the last ballot should be counted. Since an adversary may recast old ballots generated by an honest voter, a voter should memorise all the ballots he generated and check that they appear in the right order on the ballot box. Such a check seems Figure 11: Comparison of several privacy definitions (✓: the protocol is private, ✗: there exists an attack on privacy)

	Protocol	Honest board [6] PrivDis-Naive PrivacyBS [9] Priv-careful
	Simple (no revote)	✓	✗	✓	✗
	Helios	✓	✗	✗	✗
	Belenios	✓	✗	✗	✓
	Civitas (no revote)	✓	✗	✓	✓
	Neuchâtel (no revote)	✓	✗	✓	✗

ACKNOWLEDGMENTS

The authors would like to thank Esfandiar Mohammadi and the anonymous reviewers for their helpful comments and suggestions that greatly contributed to clarify the notions presented in the paper. This work has been partially supported by the European Research Council (ERC) under the European Union's Horizon 2020 research (grant agreement No 645865-SPOOC).


Daniel Burgos
email: daniel.burgos@ou.nl

Colin Tattersall
email: colin.tattersall@ou.nl

Martin Dougiamas
email: martin@moodle.org

Hubert Vogten
email: hubert.vogten@ou.nl

Rob Koper
email: rob.koper@ou.nl

A First Step Mapping IMS Learning Design and Moodle

Keywords: IMS Learning Design, Moodle, Integration, Mapping Categories: H.4.2, D.2.1, D.2.12

Mapping the specification IMS Learning Design and the Course Management System Moodle is a logical step forward on interoperability between eLearning systems and specifications in order to increase the best acceptance of the specifications into the widespread world of the eLearning systems and to ensure the standardization of the outputs from the systems to be used in others. IMS Learning Design and Moodle look for a common understanding focused on the integration of information packages modelled by each part in the other. The final goal aims at Moodle playing an IMS LD package. A second step will map a Moodle course to be used in any IMS LD complaint tool. The Unit of Learning in IMS LD and the course in Moodle become the perfect couple where to find several elements that should match each other. This paper shows how to make this understanding, mapping related elements in both to get a list of pairs easy to translate from one to another, and to define also a list of requirements for this protocol.

Introduction to IMS Learning Design and Moodle

The mutual understanding between IMS-LD and Moodle seems like an improvement for both parts. IMS-LD provides a pedagogical flexible approach in the creation of UoLs, as well as the specification support and the technical background focused on standardization and interoperability; and Moodle provides a well-known and easy-tolearn CMS and an active community of non-technical profile. To this end, Moodle and The Open University of The Netherlands established a working group in June 2005, then hosted by the UNFOLD Project and Learning Network for Learning Design and currently supported by the ProLearn and TENCompetence projects.

IMS Learning Design

IMS Learning Design, or simply IMS-LD, [START_REF] Imsld | IMSLD: "IMS Learning Design[END_REF]] is a specification to represent and encode learning structures and methods for learners and teachers. Furthermore, IMS-LD is focused on the design of pedagogical methods able to manage learning activities linked to learning objects within a learning flow. This learning flow consists of plays, acts, activities, activity structures and environments and it is flexible enough to provide several personalized itineraries depending on the role assigned or on a set of rules. The usual life-cycle starts with a lesson plan modelled according to the IMS-LD specification, defining roles, learning activities, services and several other elements, inside a XML document called Manifest [START_REF] Tattersall | IMS Learning Design Frequently Asked Questions[END_REF]]. An information package written in IMS Content Packaging [START_REF] Imscp | IMSCP: "IMS Content Packaging[END_REF]] is used as a container of the resources and links them with the IMS-LD structure, defined in the Organizations section of the IMS CP package. Later, the Manifest is packaged with the nested resources in a compressed ZIP file, meaning a Unit of Learnig (UoL) [START_REF] Koper | [END_REF]. Therefore, the UoL is a compressed file with a) an XML manifest, describing method, plays, acts, roles, activities, environments, properties, conditions and/or notifications of the Learning Design specification and also pointing to the related resources; and b) a set of files or resources mentioned in the XML manifest. Once the UoL is validated, published and run in a player, it will player will coordinate the teachers, the students, the activities during the learning process. A user will follow the learning path created for him or for his role and will carry out the related activities in order to complete satisfactorily the Unit of Learning.

Figure 1: IMS Learning Design and three levels specification

IMS-LD consists of three levels (Figure 1). Each level itself provides specific features to the Unit of Learning. Level A provides method, plays, acts, roles, roleparts, learning activities, support activities and environments; Level B provides properties, conditions, calculations, monitoring services and global elements; and Level C adds notifications. Every layer is made upon the previous one. Level A is the main part of the specification, as it provides the baseline to build any Unit of Learning, Level B adds powerful features to create more complex e-learning lesson plans, and Level C sums a specific and useful trigger element.

Every single step between the creation and the use needs an IMS-LD compliant tool. The UoLs can be created with general purpose editors or with specific IMS-LD editors, like CopperAuthor [ Van der Vegt 2005], Cosmos [Miao 2005] or Reload LD Editor [Bolton 2004], and they can be run with several tools and engines, like CopperCore [START_REF] Vogten | CopperCore 3.0[END_REF] or Sled [START_REF] Ouuk | OUUK: "Sled player[END_REF]]. However, current tools do not allow for an easy editing of rich and flexible UoLs. They make the creation of adaptive UoLs technically possible, but too difficult for a non-technical user. It is the same with general purpose editors, like XML Spy. A creator has to know the technical editors and the specification in depth. A higher level layer with a more visual metaphor is still missing, although on its way. The TENCompetence Project, for instance [TENCompetence 2005] is developing a visual LD Editor. Also, Complutense University is developing the <e-LD> project, using UML diagrams to represent the flow of the different Units of Learning. Nevertheless, for the time being, a significant effort is still needed to create adaptive IMS-LD UoLs. As an example, there is a repository with a number of runnable sample UoLs [LN4LD 2005;[START_REF] Ounl | OUNL: "DSpace[END_REF] focused on several educational issues.

Moodle

Moodle [Dougiamas 2003] is a Course Management System (CMS) easy to install and to use and wide abroad disseminated, with more than 100.000 registered users, 12.000 registered websites and translation into 70 languages. Also, Moodle has a very strong virtual community of active users carrying out an increasing amount of face-to-face and online activities, and supporting each other via the official site and a number of ad hoc assorted websites. Moodle is able to manage every feature of a course and the related environment, such as user definition, groups, access, resources, internal links and a long et cetera. This is a difference with IMS-LD. From a social constructionist approach a course is created from scratch in a few minutes. Moodle also allows for the execution of other information packages, like SCORM, LAMS and Content Packaging, as an encapsulated module inside a course. On the other hand, the pedagogical expressiveness of Moodle is limited by the absence of features included in the IMS-LD model, such as defined adaptive learning flow, flexible roles and adaptive content. Currently, Moodle is working intensively to provide these missing features so that it is able to support IMS-LD more fully over time. The main issue is that IMS-LD and Moodle are not comparable at all, as they have different approaches to work on e-learning as well as they are different releases [START_REF] Berggren | Practical and Pedagogical Issues for Teacher Adoption of IMS Learning Design Standards in Moodle LMS[END_REF]].

Basic approach on mapping IMS-LD and Moodle

There are a few attempts to integrate UoLs with stand-alone LD players like Sled and Moodle [START_REF] Burgos | Modelado y uso de escenarios de aprendizaje en entornos b-learning desde la práctica educativa[END_REF]. Sled is able to run a UoL stored in a LD server via an Internet Explorer player in the client (Telcert). A link from a Moodle resource to the ip address where Sled is allocated allows a simple first level of integration. This structure is not focused on the reusability of the lesson plans but on the integration of current systems to form a de facto more complex approach, collecting several technologies. Other attempt looks into the communication between the IMS-LD based engine called Coppercore and external systems and services, like <e-Adventure>, that executes adaptive educational games fully integrated in Units of Learning [START_REF] Burgos | [END_REF] What the mapping of Moodle and IMS-LD aims to is the re-usability of a lesson plan/course/UoL of Moodle into an IMS-LD compliant tool, or the other way around; this re-usable information package could be used as a base for a further development or as they are actually defined. Furthermore, this mapping is focused on the interoperability and the reusability of an information package/UoL, no matter the original platform that is used for it. Moodle has already started this mapping exercise with LAMS, SCORM and IMS Content Packaging.

In order to achieve the best understanding between IMS-LD and Moodle, we define a three step process:

1. Moodle is able to export one course to a UoL, translating the Moodle markup internal language to the IMS-LD XML based notation. In this first step, we find couples that identify specific elements of Moodle and their mirrors in IMS-LD. These elements represent the core of a Moodle course. Additional elements that are not required could be left aside of mapped as external services.

2. Moodle is able to import one UoL into the Content Management System and translate the IMS-LD notation into a Moodle notation. The biggest challenge is focused on the translation of Level B elements in Moodle, since Moodle does not support several of such elements, like conditions and global elements.

3. Moodle is able to play a UoL inside the system, following one of the approaches on types of integration between information packages and players suggested in [Tattersall et al. 2006]: Moodle stores an IMS-LD information package and it runs an internal player. This integration can be implemented in several ways: a) a full integration where there is a communication of properties and states between both parts; b) a half-way integration where the information package is inside the other system, but there is no communication between them; and c) a low integration where there is a link between both applications, but the information package is not hosted in the foreign system.

To realize these three steps we need to establish a general framework, with some restrictions. Since both parts are different in essence (Moodle is a CMS, while IMS-LD is a specification) a constraints list is required in order to find a common agreement which the understanding could be built upon. Specifically:

1.  Besides the Moodle course, the rest of the Course Management System environment is out of scope (calendars, blocks, log-in, language…) as they are used as processes and instructions and not like a core part of the basic unit of interchange for information (i.e., a Moodle course or an IMS-LD UoL).  2. There is a need for matching every single Moodle feature-component to an equivalent in IMS-LD or to define it like an external process/instruction.

3. In order to make taxonomy of the elements in a Moodle course and to find a mirror in the IMS-LD specification, we define four main groups: 1) Setting (basic configuration), 2) Activity, 3) Resource, 4) Administration (out of scope).

If we take a Moodle course we can match every element of the course with an element in the basic structure of an IMS-LD Unit of Learning.

The first step: Exporting a Moodle course to an IMS-LD Unit of Learning

The first step in the integration process is focused on the exportation of a Moodle single course to an IMS-LD UoL. In order to achieve this goal we establish a list of assumptions: a) there is no round tripping for the first stage, b) the exportation is completely made in batch mode (therefore, no dialog nor user interaction), and c) this task is planned as an iterative process where the first iteration gets the basic skeleton for conversion and the subsequent versions will extend it. IMS-LD is defined as a metaphor built around a theater using roles, plays and acts. Inside, some elements describe the educational framework: learning objectives, activities, environments, property of visibility, method, type of learning flow, etc. In Figure 1, there are several couples of elements IMS-LD & Moodle defined in the most basic structure of a Moodle course:

Mapping services

Some activities in Moodle need a special process, as they have some basic data used for the appropiate execution (i.e., forum, wiki, quiz…). Every activity or resource in Moodle needs to export some additional information that is not supported by IMS-LD, i.e., timing in Forums or grades in Workshops. If IMS-LD is not able to manage this information it will be lost and no later retrieval will be possible from IMS-LD to Moodle, in future versions, although no round tripping is assumed in the first approach.

A possible way is to associate a file with all the extra information related to an activity. For instance, a Moodle Forum is matched to an asynchronous conferencetype service in IMS-LD and there is a linked file with the information about starting time, ending time, or discussions policy. We could call the file serviceparams.xml. This file is a resource in the content package, type servicecontent, although other types are possible: webcontent, imsldcontent and imsqti_item_xmlv2p0. The field serviceparams.xml needs to be associated with the service service-conference, but this is not possible yet in the current IMS-LD 1.0´s information model. One approach is to associate an additional learningobject with a service. The final approach is as follows:

<imsld:environment> identifier="env-Topic-0-News-Forum"> <imsld:title> Moodle Summary Topic </imsld:title> <imsld:service identifier="service-conference" isvisible="true"> <imsld:conference conference-type="synchronous"> ... </imsld:conference> </imsld:service> <imsld:learning-object identifier="ForumParams"> <imsld:item identifier="PARAMS" identifierref="RefToParams"/> </imsld:learning-object> </imsld:environment> … <imscp:resource identifier="RefToParams" type="servicecontent" href="params.xml"> <imscp:file href="params.xml" /> </imscp:resource> Following this structure we could map any resource or activity without any lost of relevant information in Moodle. Although this approach of Moodle is miss-using the notion of a learning object, it could serve as a temporary solution until a modification of the XML Scheme in a new version of IMS-LD could happen.

Conclusions

IMS Learning Design and Moodle are two entities that work on the process to reach a kind of integration that allows for the exportation of a Moodle course to an IMS-LD format, the importation a UoL to a Moodle CMS, and the execution of an IMS-LD information package into a Moodle CMS. Following this three-step process a working group formed by Moodle and The Open University of The Netherlands looks for an understanding between both eLearning parts. The final objective is to achieve some level of interoperability and re-usability of online lesson plans and courses.

The first step to take is focused on the exportation issue and it aims to get a basic mapping between both, taking a simple Moodle course that could be extended with additional features in a second round. For this exportation, a challenge is to keep some information in services or activities that Moodle uses for their configuration and execution. An approach points to keep this information in a file stored inside the information package as a resource and to link it as a learning object to the called service. This way, all the needed information is fully exported to an IMS-LD package but leaving it out of the main manifest, where it could not be properly handle, as there are no possible match yet. A second approach points to a modification of the XML Scheme in IMS-LD 1.0 where this situation could be manage directly.

Figure 2 :

 2 Figure 2: Basic match between an IMS-LD UoL and a Moodle course.

Table 1 .

 1 Table 1 shows the result: Elements in an IMS-LD Unit of Learning mapped to elements in a Moodle course.

	Issue	Moodle	feature-	IMS-LD structure		Remarks
		component
	0	Full course		1 UoL, 1 play, 1 act, 1
				activity	structure	(type
				selection)
	1.1	Setting: Full name	Title of Learning Design
	1.2	Setting: Short name	Title of Play
	1.3	Setting: Hidden sections	Activity			Possible,	but
				Structure:IsVisible		suggested for a next
							iteration
	1.4	Setting: summary		LD learning objectives
	1.5	Setting: Your word for	roles:learner:title
		Students
	1.6	Setting: Your word for	roles:staff:title
		Teachers
	2.0	Topic		Learning activity		If a resource or an
	2.1	Topic 0		Learning activity (first	activity is defined
				one)			there will be an
	2.2	Summary of Topic	Activity Description		environment
							If there is no
							activity description
							in Topic it should be
							auto-generated with a
							standard text or just
							empty
	2.3	Activity: Chat		Synchronous conference	Services
				(conference-type)
	2.4	Activity: Forum		Asynchronous conference	Services
				(conference-type)
	2.5	Activity: Glossary	-			Generate	as
							dynamic HTML
	2.6	Activity: Quiz		-			Possibly	it
							generates QTI
	2.7	Activity: Scorm		No match		For	a	next
							iteration
	2.8	Activity: Survey		External			Generated	by
							Level B
	2.9	Activity: Workshop	External			Generated	by
							Level B
	3.0	Resource		Learning object		All the resources
							ended as learning
							objects	except
							Directory and Link
	3.1	Resource: Directory	-			Generated	by
							Level B
	3.2	Resource: Label		Learning object		Could map to a
							title of environment
							if needed
	3.3	Resource: Link to file	Learning object		File should be