Kris Mcglinn
email: kris.mcglinn@scss.tcd.ie

Matthias Weise

SWIMing: Supporting Use Case Data Requirements Modelling for Managing Data Across the Building Life Cycle

Keywords: Exchange requirements, Use case management, BIM, MVD

Data exchange and data sharing is still one of the big challenges in the AEC industry. BIM and open standards like IFC, SAREF or CityGML and lately the use of Semantic Web technologies provide a sound basis to implement exchange requirements derived from typical AEC use cases. Meanwhile many solutions are available that may already solve the problem in question. However, it is very challenging to find out what is available and how to align it with specific requirements.

Introduction

SWIMing is a Coordination and Support Action (CSA) with the goal of supporting EU-funded projects working in the area of improving energy efficiency of buildings and districts, to increase their impact through the adoption of open BIM standards. It is focusing on use case specifications and is following the IDM/MVD methodology developed by buildingSMART. The first step in this methodology is to identify use cases and to extract meta-data such as involved stakeholders, covered building life-cycle stages or data domains. While this information helps to classify use cases it does not give detailed insights into the exchange requirements and how these fit together and integrate into the BIM-based design process. In order to do so, SWIMing is proposing to build-up a shared use case repository that collects detailed Exchange Requirements as well as its implementation in data structures. We will show the current state of this repository and how it can support other projects to identify data structures and links to existing standards so that they can better manage the data requirements of their project. We will explain available features of the repository and will discuss potential extensions that help to better analyze and compare requirements.

Taking into account the whole Building Lifecycle (BLC), which defines the life of a building from design, construction, operation and maintenance, refurbishment/ renovation and on to eventual demolition/recycling [START_REF] Smith | Building Information Modeling: A Strategic Implementation Guide for Architects[END_REF][START_REF] Wong | Enhancing environmental sustainability over building life cycles through green BIM: a review[END_REF], buildings are responsible for around 40 % of total EU energy consumption [START_REF] Balaras | European residential buildings and empirical assessment of the Hellenic building stock, energy consumption, emissions and potential energy savings[END_REF]. The EU has established the Energy Performance of Buildings Directive (EPBD) which aims to reduce energy consumption across the BLC as part of its overall goal of cutting EU energy consumption by 20 % by 2020 [5].

Reducing building energy consumption across the BLC requires the exploration of new and novel use cases for monitoring and predicting energy consumption and also the re-evaluation of existing use cases to determine if existing building processes may be refined and made more efficient. One enabler for this is Building Information Modelling (BIM) [START_REF] Wong | Enhancing environmental sustainability over building life cycles through green BIM: a review[END_REF]. BIM is a concept which has arisen to address the management and interoperability of the data exchanged between different computer aided tools employed at different stages of the BLC [START_REF] Eastman | BIM Handbook: A guide to Building Information Modeling for Owners, Managers, Designers[END_REF]. Access to reliable structured data plays a key role in all aspects of energy management across the BLC, as ICT solutions ranging from energy and performance modelling tools to operational decision support tools, rely on this for their correct operation.

The leading standard developed around the concept of BIM is Industry Foundation Classes (IFC) [START_REF] Liebich | IFC4 -Addendum 1[END_REF], which is also the only BIM ISO standard [8]. IFC is a non-proprietary exchange format for describing buildings in terms of the semantics of constituent building elements. It enables the passing of information between different stakeholders involved in different stages of the BLC and addresses several core data domains required for building architecture, engineering and construction processes. Many commercially available tools support exporting their models in IFC, e.g. REVIT, Autodesk, ArchiCAD, MagiCAD and IES.

However, in practice, barriers exist to the use of IFC. For instance, the conversion of IFC data to and from tool specific data models often result in data loss [START_REF] Solihin | Toward robust and quantifiable automated IFC quality validation[END_REF][START_REF] Eastman | Exchange model and exchange object concepts for implementation of national BIM standards[END_REF]. Nonetheless, IFC is a well-established standard, which supports many use cases relevant to the BLC, and while it may not currently meet all building data requirements.

Making building processes open and interoperable using IFC is viewed as a better alternative than closed vendor specific proprietary models and has significantly increase its use over the past decade in the design stage and also in the construction domain [START_REF]Smart Market Report: The Business Value of BIM in North America: Multi-Year Trend Analysis and User Ratings[END_REF].

To make the process of using IFC simpler, so that data exchanges can be identified and tools can support those data requirements while still being interoperable with the IFC schema, the Information Delivery Manual (IDM) and Model View Definitions (MVD) have been developed by the non-profit organization buildingSMART. IDM can help identify and capture the exact information exchange requirements to meet a business use case.

As the IDM methodology is agnostic about the particular data schema used to meet data exchange requirements, it is also possible to map data requirements to data structures other than IFC if they are not yet covered, or fall outside its scope. The issue remains though about how to link these models and maintain interoperability. Linked Data (LD), which is used by the W3C Data Activity, provides a possible solution to this problem. LD is a structured form of data storage, distributed across the web, and which is supported by tools to easily query that data. By integrating BIM into the wider web of data, building information can be queried alongside all other Linked Open Data (LOD) sources, which include data on materials and systems (e.g. sensor and state of building devices data) which make up the building, profiles of occupants, and information about weather patterns and regional and global energy prices. Together this information can make for more meaningful analysis of energy consumption and its relation to the localized costs of materials, systems and personnel in existing and future buildings.

© IFIP International Federation for Information Processing 2016 Published by Springer International Publishing AG 2016. All Rights Reserved B. Bozic et al. (Eds.): CHDDH 2016, IFIP AICT 482, pp. 124-126, 2016. DOI: 10.1007/978-3-319-46224-0

SWIMing: Supporting Use Case Data Requirements Modelling


Véronique Cortier

David Galindo

Mathieu Turuani

A formal analysis of the Neuchâtel e-voting protocol

Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously.

In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and verifiability properties. Our analysis mostly confirms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast verifiability, even if the voter's device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically-binding elections has been realized.

Introduction

Remote electronic voting (or Internet voting) allows voters to vote from their home or when they are travelling. It is also seen as a means to get feedback from citizens on a more regular basis. Therefore, Internet voting has been used in legally binding elections in several countries, including e.g. Estonia [START_REF] Heiberg | The application of i-voting for estonian parliamentary elections of 2011[END_REF], Australia [START_REF] Brightwell | An overview of the ivote 2015 voting system[END_REF], France [START_REF] Pinault | E-voting at expatriates' mps elections in france[END_REF] or Switzerland [START_REF] Galindo | Neuchâtel's Cast-as-Intended Verification Mechanism[END_REF]. Of course, designing and implementing a secure electronic voting system is a difficult task and many attacks or weaknesses have been discovered on deployed systems (see e.g. [START_REF] Wolchok | Attacking the Washington, D.C. Internet Voting System[END_REF][START_REF] Springall | Security Analysis of the Estonian Internet Voting System[END_REF]). Voting protocols should offer some basic security guarantees, such as ballot privacy (no one knows how I voted) as well as verifiability (voters can check the voting process) with as few trust assumptions as possible.

On an academic level, several Internet voting protocols have been developed and some of them offer a prototype implementation or even a voting platform. This is for example the case of Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF], Civitas [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF], Belenios [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF], or Select [START_REF] Küsters | sElect: A Lightweight Verifiable Remote Voting System[END_REF]. These protocols are well documented and typically come with a proof of their security, at least w.r.t. privacy, in a symbolic or a cryptographic model (see e.g. [START_REF] Bernhard | How Not to Prove Yourself: Pitfalls of the Fiat-Shamir Heuristic and Applications to Helios[END_REF][START_REF] Juels | Coercion-Resistant Electronic Elections[END_REF][START_REF] Küsters | sElect: A Lightweight Verifiable Remote Voting System[END_REF][START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF]). On the other hand, industrial scale protocols are being deployed and now also aim at offering some verifiability properties. For instance some systems offer voters to check their vote. Some examples are: the Estonian [START_REF] Heiberg | Improving the verifiability of the estonian internet voting scheme[END_REF] protocol, where voters can check their vote during a short period of time; the so-called Norwegian protocol [START_REF] Gjøsteen | The norwegian internet voting protocol[END_REF], that does so using return codes; or the New South Wales iVote protocol [START_REF] Brightwell | An overview of the ivote 2015 voting system[END_REF]. The systems deployed in Norway and New South Wales have been (co)-developed by Scytl, a company specialized in e-voting solutions. Each of those systems has been adapted to suit the requirements and needs of each jurisdiction. Contributions. In this paper, we analyze the next generation of the Norwegian protocol [START_REF] Gjøsteen | The norwegian internet voting protocol[END_REF][START_REF] Galindo | Neuchâtel's Cast-as-Intended Verification Mechanism[END_REF], that has been deployed and is being used in the Swiss cantons of Neuchâtel and Fribourg [START_REF] Swiss | Swiss post's e-voting solution[END_REF]. Our main contribution is a thorough analysis of the Neuchâtel protocol (as specified in [START_REF] Galindo | Neuchâtel's Cast-as-Intended Verification Mechanism[END_REF][START_REF] Scytl | Swiss On-line Voting Protocol[END_REF]) in ProVerif. The tool ProVerif [START_REF] Blanchet | Automatic verification of security protocols in the symbolic model: The verifier proverif[END_REF][START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF] is a state-of-the-art tool for the formal analysis of security protocols. We are able to prove ballot privacy (modelled as an equivalence property) as well as cast-as-intended and recorded-as-cast verifiability (modelled as a reachability property).

It should be noted that the Neuchâtel protocol, as well as most industrial-scale protocols, is not fully verifiable according to the academic tradition, since the content of the ballot box is not publicly disclosed. Instead, the protocol aims at providing cast-asintended verifiability: if the voting server registers a ballot in the name of a voter then the ballot contains the vote intended by the voter, even if the voting device is corrupted and tries to cast a vote for another voting option. Cast-as-intended is achieved through return codes: after casting a vote, a voter receives a code and checks (on her voting card) that it matches the code displayed next to her intended choice. The Neuchâtel protocol additionally guarantees recorded-as-cast verifiability: if a voter completes the voting process then she is guaranteed that her ballot, as built by her voting device, has reached the voting server. These two verifiability properties hold under the assumption that the voting server is not compromised. Note that cast-as-intended verifiability is not offered by academic systems such as Civitas [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF] and Belenios [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF]. Often when it is offered quite a burden is placed on the voter: this is the case for Helios (cast-oraudit mechanism [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF][START_REF] Kiayias | Ceremonies for end-to-end verifiable elections[END_REF]), where the voter needs to use two voting devices that are not simultaneously compromised. Namely, the device used for auditing the vote needs to be different from the device used to cast the vote.

In order to prove our security claims, we present a detailed model of the protocol, that includes for example the authentication phase after which the voter retrieves her voting credentials (i.e. by opening a password-protected keystore). Whereas such an initialization phase must be present in any real-world e-voting system, it is omitted in virtually every security analysis. Even worse, such authentication mechanism is typically not specified by the protocols in the academic literature. This is not necessarily surprising, and it might stem from the fact academic research artefacts often do not get used in practice and thus do not need to be described as a fully detailed system. Additionally, we capture in our model elections where voters can select k options among n voting options (while systems in the literature are often analysed in the case of elections where voters selects 1 option among n or even 1 among 2).

We chose to perform an automated security analysis using ProVerif (instead of a manual proof) precisely to be able to model as many details as possible. We also believe that our model could serve as a basis for further studies of other voting protocols, as it is easier to adapt a symbolic model than a manual proof.

One difficulty we had to face resides in the fact that ProVerif does not handle well protocols with global states. This is of particularly critical importance in the case of the Neuchâtel protocol, since it becomes insecure (w.r.t. cast-as-intended) as soon as revoting is allowed. It is therefore crucial to model the fact that each voter votes "at most once", and to do it in such a way that ProVerif can still handle the resulting model and provide a proof. Again, we believe that the techniques developed here to circumvent this issue are likely to be found useful elsewhere.

Our analysis mostly confirms the security of the protocol: we prove in ProVerif ballot privacy against a dishonest voting server as well as cast-as-intended and recordedas-cast against a dishonest voting device, for an unbounded number of voting options and of voters. However, while modelling the protocol, we also discovered small variations thereof, which could realistically come up when implementing the protocol in a real scenario, that would render the protocol insecure in practice.

Related Work.

The study most closely related to this paper is the analysis of the Norwegian protocol [START_REF] Cortier | A formal analysis of the norwegian e-voting protocol[END_REF], that solely studies ballot privacy. The Norwegian protocol is an ancestor of the Neuchâtel protocol. The goal of the analysis in [START_REF] Cortier | A formal analysis of the norwegian e-voting protocol[END_REF] was to provide a modelling as precise as possible of the protocol's underlying primitives (with associativity and commutativity properties) and prove ballot privacy by hand, which was accomplished by developing some general lemmas regarding equivalence. A brief analysis was also performed in ProVerif but in a quite abstract model. Reusing the previous model was deemed to be not possible, as the Neuchatel protocol has evolved quite significantly and the resulting equational theories for the atomic primitives are different.

Earlier research proposed the first symbolic models of electronic protocols. This includes a model of JCJ [START_REF] Backes | Automated verification of remote electronic voting protocols in the applied pi-calculus[END_REF] and Helios [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF][START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF]. These models solely study privacy properties and consider a simpler scenario where voters select one candidate among a finite number of options. These protocols also allow revoting, which significantly simplifies the analysis in ProVerif (cf. the discussion above on dealing with a global state).

Computational proofs of privacy and/or some verifiability properties have been provided for Helios [START_REF] Bernhard | How Not to Prove Yourself: Pitfalls of the Fiat-Shamir Heuristic and Applications to Helios[END_REF], Civitas [START_REF] Juels | Coercion-Resistant Electronic Elections[END_REF], Select [START_REF] Küsters | sElect: A Lightweight Verifiable Remote Voting System[END_REF], Belenios [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF] and [START_REF] Kiayias | DEMOS-2: scalable E2E verifiable elections without random oracles[END_REF] for example. Cyrptographic models are more accurate w.r.t. the underlying primitives and consider a more powerful attacker, which may for example exploit algebraic properties of the primitives. Most of these proofs are done by hand, with the exception of [START_REF] Cortier | Machine-checked proofs of privacy for electronic voting protocols[END_REF], that provides a mechanized proof of ballot privacy for Helios-like protocols. Given their complexity, these proofs focus on the core of the protocol, abstracting away many details, including detailed analysis of the high-level interactions between the different parties of the protocol (e.g. computational proofs would typically assume a secure channel between the voter and the ballot box, without being explicit nor studying how this is done). The intrinsic complexity of computational proofs of elaborated protocols,

Overview of the Neuchatel's system

The Neuchâtel voting protocol involves four main participants: the Voter (V), that casts a vote with the help of a Voting Device (VD); the Voting Server (S), that interacts with the voter's device to store the voter's ballot in a database, and next it computes return codes that need to be approved by the voter V; finally the Tallying Authority (T), that computes the result of the election by tallying the ballots database built by the server.

For the sake of clarity, we summarize the Neuchâtel protocol in the case of a selection of k " 2 choices among n voting options v 1 , . . . , v n . Our analysis accounts however for several values of k other than k " 2. A synthetic view of the protocol is provided in Figure 1.

Tallying Authority (T). Creates an ElGamal asymmetric encryption key pair ppk b , sk b q. The public encryption key pk b is communicated to the Registrar. Once the election is closed, the authority T computes and outputs the result of the election as follows.

From each ballot to be counted, it extracts the ElGamal encryption of the vote. Next, T applies a mixnet to the resulting ciphertext list, decrypts every entry with the corresponding election decryption key sk b and computes a zero-knowledge proof of correct decryption. The result is simply the multiset of the decrypted votes.

Voter (V). The voter V associated to id enters into her voting device VD her password pwd id and her preferred voting choices v 1 , v 2 . At some point, VD displays short return codes src 1 , src 2 to the voter. The voter retrieves the codes src id v1 and src id v2 linked to v 1 , v 2 from her voting card. If the displayed and the retrieved code sets coincide, the voter confirms her votes by entering the confirmation code cc id . Finally, VD displays a short finalization code sfc, which should be equal to the code sfc id on the voter's card. In this case, V is ensured that her ballot contains her intended voting options and that it has been accepted by the voting server S.

Voting Device (VD). The device VD uses the voter's password pwd id to obtain a keystore ks id , from which it retrieves the voters' key pair ppk id , sk id q. Next, the device computes a ballot b " pctxt, pv 1 q sk id , pv 2 q sk id , ec 1 , ec 2 , pk id , Pq that is received by the Voting Server. The ballot consists of several parts:

• ctxt " aenc `pk b , φpv 1 , v 2 q, r ˘is an encryption of voting choices v 1 , v 2 using an ElGamal encryption algorithm aenc, and a bijective compacting function φ that maps any list of integers to a single integer (this relies on the uniqueness of prime factors decomposition).

• so-called partial return codes pv 1 q sk id , pv 2 q sk id allow the Voting Server to compute the short return codes src id v1 , src id v2 that appear in the voter's voting card; • the remaining components serve to guarantee consistency between ciphertext ctxt and the partial return codes pv 1 q sk id , pv 2 q sk id , by using a zero-knowledge proof P.

If the ballot is accepted by the server S, the voting device VD receives short return codes src 1 , src 2 from the server and displays them to the voter V. Next, on input of the finalization code ccid entered by the voter, it computes and sends pcc id q sk id to the server. Finally, the server sends a short finalization code sfc, to be displayed to the voter.

Voting Server (S). It interacts with a voter V with identifier id through her voting device VD as follows. Firstly, the server receives the voter's identifier id from VD and replies with the corresponding keystore ks id . Next it receives from VD a ballot b " pctxt, pv 1 q sk id , pv 2 q sk id , ec 1 , ec 2 , pk id , Pq, and checks that it is a valid ballot. In particular, it verifies the zero-knowledge proof P and checks that voter V did not vote already. If valid, the ballot is stored in a database bb. From the partial return codes pv 1 q sk id and pv 2 q sk id , the server can compute the values rc 1 and rc 2 through a keyed pseudo-random function, and retrieve their corresponding short return codes src 1 , src 1 by looking into a table M. These short codes are sent to VD. Next, if the voter is satisfied with the return codes, S receives the value pcc id q sk id , from which it can compute fc (same way as rc) and retrieve it's short code sfc by looking again into M. The server S also retrieves a validity proof crf id from M, that tells whether the retrieved code sfc is valid or not. If all the tests pass, S adds the confirmation values sfc and crf id to the database (cb here), to keep track that the ballot b was successfully confirmed, and sends sfc to VD.

Framework

In the coming sections we present a ProVerif model of the Neuchatel protocol. A detailed presentation of the syntax and semantics of ProVerif can be found in [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF]. For M, N, U ::

= terms x | n | f pM 1 , . . . , M k q
where x P V, n P N , and f P C the sake of readability, we give next an overview of the protocol, focusing on the parts that are more relevant to our model. Notations and definitions are mainly borrowed from [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF].

D::= expressions M | hpD 1 , . . . , D k q where h P C Y D φ::= formula M " N | φ 1 ^φ2 | φ 1 _ φ 2 | φ P, Q::= processes 0 nil outpN, M q; P output inpN, x : T q; P input P | Q parallel composition !P replication new a : T ; P restriction let x : T " D in P assignment if φ then P conditional eventpM q; P event

Syntax

We assume a set V of variables, a set N of names, a set T of types. By default in ProVerif, types include channel for channel's names, and bitstrings for bitstrings (also written any). The syntax for terms, expressions, and processes is displayed in Figure 2.

Terms and expressions. Symbols for functions are split into two sets of constructors C and destructors D respectively. Terms are built over names, variables and constructors and represent actual messages sent over the network, while expressions may also contain destructors and represent cryptographic computations. Function symbols are given with their types: gpT 1 , . . . , T n q : T means that the function g takes n arguments as input of types respectively T 1 , . . . , T n and returns a result of type T . A substitution is a mapping from variables to terms, denoted tU 1 {x 1 , . . . , U n {x n u. The application of a substitution σ to a term U , denoted U σ, is obtained by replacing variables by the corresponding terms and is defined as usual. We only consider well typed substitutions.

The evaluation of an expression is defined through rewrite rules. Specifically, each destructor d is associated with a rewrite rule of the form dpU 1 , . . . , U n q Ñ U , over terms. Then the evaluation of an expression is recursively defined as follows:

• gpD 1 , . . . , D n q evaluates to U , denoted gpD 1 , . . . , D n q ó U , if @i, D i ó U i , and g is a constructor (g P C) and U " gpU 1 , . . . , U n q; or g is a destructor (g P D) and there exists a substitution σ such that U i " U 1 i σ, U " U 1 σ, where dpU 1 1 , . . . , U 1 n q Ñ U 1 is the rewrite rule associated to g.

• gpD 1 , . . . , D n q evaluates to fail, denoted gpD 1 , . . . , D n q ó fail, otherwise.

The evaluation φ of a formula is defined by M " M " J, M " N " K otherwise, and is then extended to ^, _, as expected.

Example 1. To model the simple theory of encryption and concatenation, we consider a type symkey for symmetric keys and the sets of constructors and destructors with their associated rewrite rules as follows:

C basic " t pair pany, anyq : any, encpsymkey, anyq : any u D basic " t proj 1panyq : any, proj 2panyq : any, decpsymkey, anyq :

any u R basic " t proj 1ppair px, yqq Ñ x, proj 2ppair px, yqq Ñ y, u decpx, encpy, xqq Ñ x
We often write pm 1 , m 2 q instead of pair pm 1 , m 2 q and pm 1 , m 2 , . . . , m k q stands for pm 1 , pm 2 , p. . . , m k qqq.

Processes. Figure 2 provides a convenient abstract language for describing protocols (formally modeled as processes). The output of a message M on channel N is represented by outpN, M q; P while inpN, x : T q; P represents an input on channel N , stored in variable x. Process P | Q models the parallel composition of P and Q, while !P represents P replicated an arbitrary number of time. new a : T ; P generates a fresh name of type T and behaves like P . let x : T " D in P else Q evaluates D and behaves like P unless the evaluation fails, in which case it behaves like Q. eventpM q; P is used to specify security property: the process emits an event (not observable by an attacker) to reflect that fact that it reaches some specific state, with some values, stored in M .

The set of free names of a process P is denoted fnpP q, and the set of it's free variables by fv pP q. A closed process is a process with no free variables. Following ProVerif's handy notations, we may write inpc, " xq.P instead of inpc, y : T q.if x " y then P , where T is the type of x. Similarly, we may write inpc, px : T, y : T 1 qq.P instead of inpc, z : anyq.let x : T " proj 1pzq in let y : T 1 " proj 2pzq in P .

Example 2. In the Neuchâtel voting protocol, the Voter interacts with a Voting Device (e.g. her computer or cell phone) to cast her vote. Initially, the voter receives a voting card with her personal data for the election, including a password pwd (used to derive the voter's key and id), one short return code src for each candidate in the Voter pc, pwd , j 1 , j 2 , src 1 , src 2 , cc id , sfc id q :" outpc, ppwd , j 1 , j 2 qq;

(* Sends password & choices. *) inpc, psrc 1 1 : any, src 1 2 : anyqq;

(* Gets the return codes. *) if psrc 1 1 " src 1 ^src 1 2 " src 2 q _ psrc 1 1 " src 2 ^src 1 2 " src 1 q then eventpconfirmed ppwd , j 1 , j 2 qq;

(* Checks ok; Reaches 'confirmed '. *) outpc, cc id q;

(* Confirms the vote. *) inpc, "sfc id q;

(* Final confirmation. *) eventphappyppwd , j 1 , j 2 qq.

(* All ok; Reaches 'happy'. *)

Figure 3: The Voter Process list, a confirmation code cc id (sent if the received return codes are valid), and a short finalization code sfc id (that should correspond to the server's last acknowledgement message). For simplicity, we model an election where voters have to select two options. We model a voter that votes for two options j 1 , j 2 , with corresponding return codes src 1 , src 2 (read from the voting card). The corresponding process is defined in Figure 3. It communicates on channel c with the voting device. It includes two events that witness some important states of the voter. They will be used later to formally state security properties (see Section 5), and are defined by: C voter " t confirmed ppassword , int, intq : any, happyppassword , int, intq : any u

Semantics

A configuration E, P is given by a multiset P of processes, representing the current state of the processes, and a set E " pN pub , N priv q representing respectively the public and private names used so far. The semantics of processes is defined through a reduction relation Ñ between configuration, defined in Figure 4. A trace is a sequence of reductions between configurations E 0 , P 0 Ñ ¨¨¨Ñ E n , P n . We say that a trace E 0 , P 0 Ñ ˚E1 , P 1 executes an event M if it contains a reduction E, P Y teventpM q; P u Ñ E, P Y tP u for some E, P, P .

Properties

As usual, we assume that protocols are executed in an unstrusted network, meaning that communications over a public network are fully controlled by an attacker who may eavesdrop, intercept, or send messages. This is easily modeled by executing a protocol P 0 in parallel with an arbitrary process Q. Formally, we assume given a set of public constructors, subset of the constructors. An adversarial process w.r.

Correspondence

Many security properties can be stated as "if Alice reaches some state (e.g. finishes her session) then Bob must have engage a conversation with her". This is for example the case of many variants of agreement properties [START_REF] Lowe | A hierarchy of authentication specifications[END_REF]. ProVerif allows to specify correspondence properties between events. Definition 1. A closed process P 0 satisfies the correspondence

P 0 m ľ i"1 li ł j"1 eventpM ij q
where the M i,j do not contain names, if for any (adversarial) closed process Q such that fnpQ Ă fnpP 0 q, for any trace tr, for any substitution σ, if tr executes event M σ, then there exists σ 1 such that M σ " M σ 1 and for any i, there exists j such that tr executes event M ij σ 1 .

Examples can be found in Section 5.

Equivalence

Observational equivalence of two processes P and Q models the fact that an adversary cannot distinguish between the two processes. Slightly more precisely, whenever P may emit on some channel c (interacting with an adversarial process R), then Q can emit on c as well. For readability, we summarise here the definition of exquivalence from [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF]. We write C Ó N when a configuration C " E, P with E " pN pub , N priv q can output on some channel N , i.e. if there exists outpN, M q; P P P such that fnpN q P N pub . Also, an adversarial context Cr s is a process of the form new n : bitstrings; | Q where fv pQq " H and all functional symbols in Q are public, with being a 'hole' expected to be filled by a configuration C " pN pub , N priv q, P. Therefore, and assuming that N priv X fnpQq " H, the application of one to the other is defined by : CrCs " pN 1 pub , N 1 priv q, P Y tQu with N 1

pub " pN pub Y fnpQqqztnu and N 1 priv " N priv Y tnu From this, the definition of observational equivalence follows : Definition 2. The Observational equivalence between configurations, denoted by «, is the largest symmetric relation such that C « C 1 implies :

• if C Ó N then DC 1 1 s.t. C 1 Ñ ˚C1 1 and C 1 1 Ó N ; • if C Ñ C 1 , then DC 1 1 s.t. C 1 Ñ ˚C1 1 and C 1 « C 1 1 ; • CrCs « CrC 1 s, for any adversarial context Cr s.

Formal model of the Neuchatel's voting system

We present here the main parts of our formal model. For simplicity, we present a model for elections with k " 2 choices to be made amongst n voting options. In our automated analysis, we generate the model corresponding to any given particular value k automatically, and then run ProVerif on several values of k (up to k " 4 due to ProVerif time out).

Standard primitives

The Neuchâtel protocol makes use of the standard primitives: symmetric and asymmetric encryption, signatures, hashes and concatenation. We consider the corresponding types agentId , int, ekey, epkey, skey, spkey, symkey. The constructors and the associated rewrite rules are defined as follows.

C stand " t sk e pagentId q : ekey, where all function symbols are public, except sk e and sk s that are private. The set of destructors D stand can be inferred easily. The term sk α pid q represents the private key of user id w.r.t. scheme α, where α " e stands for asymmetric encryption while α " s stands for signature. The rewrite rules are the standard ones for these primitives. For example adecpk, aencppub e pkq, m, rqq Ñ m models the fact that the plaintext of an (asymmetric) encryption can be retrieved by decrypting with the corresponding private key.

Voting device

A voter id is provided with a password pwd and codes (return codes as well as a confirmation code). When she connects to the voting server through her voting device, she first needs to retrieve her personal private key sk e pδ Id ppwd qq. The identifier id of the voter is actually derived from her password, that is id " δ Id ppwd q. This key is stored in a keystore (on the server's side), encrypted with a key that can be derived from the password: δ Key ppwd q. We therefore introduce the following theory to model the key store.

C ks " t δ Id ppassword q : agentId , δ Key ppassword q : symkey, c ekey pekeyq : any u R ks " t c any pc ekey pkqq Ñ k u

The corresponding set of destructors D ks can be inferred easily. The functions c any and c ekey are auxiliary functions that convert private keys to bitstring and conversely. We denote ksppwd q :" encpδ Key ppwd q, c ekey psk e pδ Id ppwd qqqq the encrypted value stored in the key store for voter δ Id ppwd q.

As explained in Section 2, the voting device builds a ballot as follows. It encrypts the choices j 1 , j 2 of the voters; builds pre-return codes for each choice prcpsk e , j 1 q, prcpsk e , j 2 q using the private key of the voter; and proves that the return codes correspond to the encrypted votes, through a zero-knowledge proof. This is modeled as follows.

C zk " tzkppepkey, epkey, any, int, int, int, ekeyq : any, prcpekey, intq : int u R zk " tverif zkp ppk b , pk, e, p 1 , p 2 , zkpppk b , pk, e, p 1 , p 2 , r, sk id q Ñ ok u with pk " pub e psk id q, e " aencppk b , v, rq, p 1 " prcpsk id , v 1 q, p 2 " prcpsk id , v 2 q with v " pv 1 , v 2 q. Note that here, our model abstracts some properties of the primitives. Indeed, as explained in Section 2, the two choices j 1 , j 2 of the voters are not encrypted as a list but are "compacted" in a single integer Φpj 1 , j 2 q, which is actually commutative: Φpj 1 , j 2 q " Φpj 2 , j 1 q. Similarly, the zero-knowledge proof compacts the pre-return codes. Since ProVerif cannot handle associative and commutative properties, we abstract away these properties, assuming a slightly stronger proof system. We can now provide the Device process, which is shown in Figure 5.

Voting server

When the voting server is contacted by some voter id (through her voting device), the server first needs to retrieve the personal keystore associated to id . Only valid id s, of the form id " δ Id ppwd q, are registered. The server also recovers (for later use) a signature signpsk c , sfcpgk a , id qq of the short finalization code sfcpgk a , id q that should be rebuilt and sent at the end by the server (defined in C rc below). The signing key sk c is a fixed long term key of the setup authorities and gk a is the global audit key of the server. We model this data retrieval by considering the following rewrite rule:

R retrieve " t Getpδ Id ppwd q, gk a q Ñ pksppwd q, signpsk c , sfcpgk a , id qqq u

The server needs to compute a long return code f pgk a , prc 1 q from the partial return code prc 1 sent by the voter. This long return code is too long to be human readable and is therefore associated (in a table) to a short return code. This table also provides a correspondence for long and short finalization codes. This is modeled through the following theory:

C rc " t srcpsymkey, agentId , intq : any sfcpsymkey, agentId q : any f psymkey, intq : symkey ccpagentId q : int u R rc " t read RC pf pgk a , prcpsk e pid q, jqqq Ñ srcpgk a , id , jq read FC pf pgk a , prcpsk e pid q, ccpid qqqq Ñ sfcpgk a , id q u with cc, src and sfc private function symbols. Actually, short return codes are stored encrypted using the long return code as a symmetric key. For the sake of clarity, we omit this part here but it is reflected in our ProVerif's model.

No revote. One of the main challenging tasks when modeling the voting server is the fact that it accepts at most one request from each voter. Note that the protocol is insecure otherwise. Indeed, in case revoting was allowed, a malicious voting device could first vote as queried by the voter and display the (correct) return codes and then revotes for the candidate of its choice (discarding the corresponding return codes). Therefore, it is crucial to model accurately that no voter can vote twice.

A first approach (as described in [START_REF] Galindo | Neuchâtel's Cast-as-Intended Verification Mechanism[END_REF]) is to use a table that stores whether a voter already voted or not. Then, intuitively, the code of the server is (informally) as follows: However, when it comes to modeling this lock mechanism in ProVerif, we have two options. The first option is to encode the lock mechanism directly in ProVerif, for example using private channels, that can be used as "tokens". This approach presents two drawbacks. Firstly, this encoding would necessarily be ad-hoc. And in principle there would be no assurance that the protocol is secure if the lock mechanism is implemented in another way (and of course, real lock mechanisms will never use private channels). Secondly, it is also known that ProVerif, due to its internal behavior, cannot properly handle private channels when used as tokens or, more generally, cannot handle properly events that happen "at most once".

if id R
Instead, we take a different point of view. We model a voting server that does not prevent revoting and adds blindly new ballots. Then, instead of asking ProVerif whether some property φ holds, we query a property of the form φ _ two ballots have been accepted for the same voter If ProVerif proves this query, it guarantees that for any execution trace where no 2 ballots are accepted by the server, then φ holds. It is then up to the implementation to ensure that any execution is such that no 2 ballots for the same voter are accepted by the server.

This yields a more flexible result: for any realization of the protocol that further ensures that "no two ballots from the same voters are accepted", then the realization satisfies φ, no matter how the "no revote policy" is actually implemented. We believe that this approach is of independent interest and could re-used in other contexts when modeling e.g. lock mechanisms in ProVerif.

Formally, the server simply issues events built from C BB " tInsertBB pagentId , anyq : anyu to record the fact that a ballot has been added to the box. The process corresponding to the voting server is then defined in Figure 6. These events are used later to specify security properties as just discussed.

Tally process

Once the voting process is over, the tally phase can start. The tally authorities check the validity of each ballot (same checks as the server); mix the ciphertexts containing the votes; decrypt the mixed ciphertexts and publish the election result. In our analysis, we consider that either the tally authorities are corrupted (for cast-as-intended and Devicepc 1 , c 2 , pk b q :" (* channels c 1 with Voter and c 2 with Server. *) inpc 1 , ppwd : password , j 1 : int, j 2 : intqq;

(* Get password & choices. *) outpc 2 , δ Id ppwd qq;

(* Ask for the keystore, *) inpc 2 , ks : anyq;

(* ... receive keystore, *) let sk id : ekey " c any pdecpδ Key ppwd q, ksqq in (* ... retrieve the key. *) new r : int; let e " aencppk b , pj 1 , j 2 q, rq in (* Encrypt voter's choices. *) let p " zkpppk b , pub e psk id q, e, prcpsk id , j 1 q, prcpsk id , j 2 q, r, sk id q in outpc 2 , pe, prcpsk id , j 1 q, prcpsk id , j 1 q, pub e psk id q, pqq;

(* Sends the ballot. *) inpc 2 , psrc 1 : any, src 2 : anyqq;

(* Get the short return codes *) outpc 1 , psrc (* Vote approval. *) outpc, sfc id q; outpc t , pid , b, sfc id , crf qq (* Confirms; Feeds the Tally. *)

Figure 6: The Server Process recorded-as-cast properties) or that the overall tally process is honest (for ballot privacy). As we shall see in Section 5 (security properties), we only need to consider two honest voters, as well as arbitrary many dishonest voters. Since privacy is ensured as soon as the two honest ballots are mixed, we model a tally process that mixes the two honest ballots only. The mixnet is modeled in a standard way, by sending the ballots over a private channel called mix concurrently, thus without fixing the order, and reading them back from that same channel. Formally, we define two processes: TallyH , as shown in Figure 7 for the honest voters (whose ballots are mixed); and TallyD as shown in Figure 8 for any dishonest voter (that can be executed arbitrarily). The process TallyD simply decrypts any (valid) ballot provided the corresponding id is not an honest voter, that is, is neither id a nor id b .

Security properties

The Neuchâtel protocol is designed to achieve cast-as-intended verifiability: even if the voter's device is corrupted, the ballot registered in the name of a voter corresponds to the vote intended by that voter. This offers a strong protection against attackerscontrolled personal computers and smartphones (e.g. through malware). The voting server shall be trusted for this step. Conversely, the Neuchâtel's protocol also guarantees vote privacy against a dishonest voting server. Note however that the protocol is not publicly verifiable: the content of the ballot box is not public and therefore voters cannot check that the result corresponds to the received ballots. We define next the security properties proved in ProVerif.

Verifiability properties

The protocol ensures cast-as-intended and recorded-as-cast: if a voter successfully completes the voting procedure, she is guaranteed that her ballot has been property recorded by the voting server.

Cast-as-Intended. The Neuchâtel's protocol provides Cast-as-Intended verifiability: if the server registers a ballot for some voter id then this ballot contains the votes intended by the voter. This can be formalized by the following correspondence property. Remember that the identity id of a voter is derived from her password (id " δ Id ppwd q).

eventpHasVoted ppk b , δ Id ppwd a q, eqq ñ D v 1 , v 2 , j 1 , j 2 , r, eventpconfirmed ppwd a , v 1 , v 2 qq ^e " aencppk b , pj 1 , j 2 q, rq ^ppj 1 " v 1 ^j2 " v 2 q _ pj 1 " v 2 ^j2 " v 1 qq (1)
Intuitively, the above reads as follows: if the server issues an event HasVoted ppk b , δ Id ppwd a q, eq, meaning that he accepted a ballot containing an encryption e, then the voter with password pwd a must have had cast a vote pv 1 , v 2 q that corresponds to e. Note that we cannot exclude the case where a malicious device swaps the vote (that is, casts pv 2 , v 1 q instead of pv 1 , v 2 q) and then swaps the received return codes. This is captured in the property above by allowing the two cases (the option order has no impact on the way votes are counted).

Unfortunately, ProVerif fails to prove this property. Indeed, cast-as-intended cannot be guaranteed as soon as the server may answer two requests from the same voter, as the attacker would then get two sets of return codes and could show the wrong one. This is explicitly forbidden by the Neuchâtel's protocol: the server does not answer to revote queries. However, ProVerif over-approximates the behaviors and takes into account the case where the server would answer twice (yielding "cannot be proved").

Instead, we consider the following correspondence property.

eventpHasVoted ppk b , δ Id ppwd a q, eqq ñ D v 1 , v 2 , j 1 , j 2 , j 3 , j 4 , j 5 , j 6 , r, r 1 , r 2 , eventpconfirmed ppwd a , v 1 , v 2 qq ^e " aencppk b , pj 1 , j 2 q, rq ^eventpInsertBB pδ Id ppwd a q, eqq ^eventpInsertBB pδ Id ppwd a q, aencppk b , pj 3 , j 4 q, r 1 qqq ^eventpInsertBB pδ Id ppwd a q, aencppk b , pj 5 , j 6 q, r 2 qqq ^pj

3 " v 1 _ j 4 " v 1 q ^pj 5 " v 2 _ j 6 " v 2 q (2)
This property states that if the server accepts a ballot containing an encryption e then the voter corresponding to pwd a must have cast a vote pv 1 , v 2 q such that the encryption e has been inserted in the ballot box, on behalf of δ Id ppwd a q. Moreover, there must have been two other insertions in the ballot box: one with pj 3 , j 4 q and one with pj 5 , j 6 q, such that v 1 is equal to either j 3 or j 4 and v 2 is equal to either j 5 or j 6 .

Why is this useful? Because we know that the protocol's implementation further guarantees that there is at most one insertion for each voter. Combined with Property 2, this implies j 1 " j 3 " j 5 ^j2 " j 4 " j 6 , hence the desired Property 1 (since

v 1 ‰ v 2 ).
More formally, for any trace tr of a process, if tr satisfies (2) and is such that there no distinct insertion for the same voter, that is: eventpInsertBB pδ Id ppwd a q, aencppk b , pj 3 , j 4 q, r 1 qqq P tr ^eventpInsertBB pδ Id ppwd a q, aencppk b , pj 5 , j 6 q, r 2 qqq P tr ñ pj 3 " j 5 q ^pj 4 " j 6 q ^pr 1 " r 2 q then tr satisfies (1). The proof is immediate.

The first interesting feature of this encoding is of course that it circumvents the issue that ProVerif over-approximates the no-revote policy. The second feature is that Property 1 is proved independently of the exact implementation of the no-revote policy. Assuming that the implementation guarantees that there is at most one insertion for each voter, then the protocol achieves cast-as-intended, no matter how this is implemented in practice.

Recorded-as-cast. The protocol further guarantees that if a voter completes the voting process then she is ensured that her vote has been recorded by the server. This property can be formally stated as follows. eventphappyppwd a , v 1 , v 2 qq ñ D j 1 , j 2 , r, eventpHasVoted ppk b , δ Id ppwd a q, eqq ^e " aencppk b , pj 1 , j 2 q, rq ^pj

1 " v 1 ^j2 " v 2 q _ pj 1 " v 2 ^j2 " v 1 q (3)
In our ProVerif model, we further show that the ballot registered by the server is wellformed and will therefore be accepted at the tally phase. Similarly to cast-as-intended, this property cannot be proved in ProVerif. So instead, we prove an amended property which implies the desired property as soon as the implementation guarantees that there is at most one ballot insertion per voter.

eventphappyppwd a , v 1 , v 2 qq ñ D j 1 , j 2 , j 3 , j 4 , j 5 , j 6 , r, r 1 , r 2 , eventpHasVoted ppk b , δ Id ppwd a q, eqq ^e " aencppk b , pj 1 , j 2 q, rq ^eventpInsertBB pδ Id ppwd a q, eqq ^eventpInsertBB pδ Id ppwd a q, aencppk b , pj 3 , j 4 q, r 1 qqq ^eventpInsertBB pδ Id ppwd a q, aencppk b , pj 5 , j 6 q, r 2 qqq ^pj 3 " v 1 _ j 4 " v 1 q ^pj 5 " v 2 _ j 6 " v 2 q (4)

Trust Assumptions. We prove cast-as-intended (Property 2) and recorded-as-cast (Property 4) even if the voting device and the tally process are corrupted. We assume however the voting server to be honest. Formally, we consider the following process:

Init; !Server pc, pk b , gk a , sk c , cq | !Corr | Voter pc, pwd a , v 1 , v 2 , srcpgk a , id a , v 1 q,
srcpgk a , id a , v 2 q, ccpid a q, sfcpgk a , id a qq where Init is an initialization process: it broadcasts id a " δ Id ppwd a q and pk e pid a q on some public channel c, generates the elections keys sk b , gk a and sk c , and publishes pk b " pub e psk b q, pub s psk c q, and sk b . The process !Corr models an arbitrary number of dishonest voters: each generates a password pwd i for some voter i and broadcasts all the corresponding (public and private) data. Note that we do not need to include the tally process since it is assumed to be dishonest. Instead, we simply provide the election key (sk b ) to the adversary: cast-asintended and recorded-as-cast properties are guaranteed even if the decryption key is lost.

Privacy

Intuitively, a voting protocol guarantees ballot privacy if an attacker cannot learn any information about how a voter voted. In symbolic models, this is typically formalized as follows [START_REF] Kremer | Analysis of an electronic voting protocol in the applied pi-calculus[END_REF][START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]:

V A p0q | V B p1q « V A p1q | V B p0q
An attacker should not be able to distinguish the case where Alice votes 0 and Bob votes 1 from the case where the votes are swapped. We show that the Neuchâtel's protocol ensures ballot privacy, even if the voting server and all but two voters (and their voting devices) are corrupted. Formally, we consider a set up process I similar to Init, but with two honest voters A, B with passwords pwd A , pwd B , and a corrupter Server process that leaks its private data gk a , sk c . The election key sk b (generated during the setup and distributed to election authorities) is assumed to be secret. We call V A pa, bq the process for voter A that votes for a and b.

V A pa, bq :" Devicepc A , c, pk b q | Voter pc A , pwd A , a, b, srcpgk a , id A , aq, srcpgk a , id A , bq, ccpid A q, sfcpgk a , id A qq

Then we prove (in ProVerif) that:

I | V A pa, bq | V B pc, dq | !Corr | T « I | V A pc, dq | V B pa, bq | !Corr | T (5)
with T :" TallyH pc, sk b , pk c , id A , id B q | !TallyDpc, sk b , pk c , id A , id B q

ProVerif cannot prove arbitrary equivalences. Instead, it proves diff-equivalence (a stronger notion of equivalence [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]) of pairs of processes that only differ in treatment of terms. More formally, ProVerif considers bi-processes P that may contain bi-terms choicept 1 , t 2 q instead of pure terms. Then ProVerif proves equivalence of proj 1 pP q and proj 2 pP q where proj i pP q is obtained from P by replacing any occurence of a biterm choicept 1 , t 2 q by t i . We refer the reader to [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF] for a detailed and formal definition of bi-processes and diff-equivalence.

So proving the equivalence

V A p0q | V B p1q « V A p1q | V B p0q amounts into consid- ering the process V A pchoicep0, 1qq | V B pchoicep1, 0qq
However, applying directly this tranformation to the equivalence (5) yields a process that ProVerif cannot prove. Instead, we need to further transform it by also swapping the output of the tally. This is a usual technique, as devised e.g. in [START_REF] Blanchet | Automated reasoning for equivalences in the applied pi calculus with barriers[END_REF]. Formally, we replace the outpmix, e a q | outpmix, e b q part in the TallyH process by: outpmix, choicepe a , e b qq | outpmix, choicepe b , e a qq Note that since the resulting processes are equivalent (since this study and for the sake of clarity, we have presented the Neuchâtel's protocol for the particular case of an election where k " 2 options among n options need to be selected. In our ProVerif model we have considered an arbitrary number of options n, an arbitrary number of voters m, and several values for the number of selections k. To be able to cope with an arbitrary number of selections, we would need to handle lists of arbitrary size (representing the selection of a voter). While there are some preliminary results for protocols with lists [START_REF] Chridi | Decidable analysis for a class of cryptographic group protocols with unbounded lists[END_REF][START_REF] Arnaud | Deciding security for protocols with recursive tests[END_REF][START_REF] Paiola | Verification of security protocols with lists: From length one to unbounded length[END_REF], none of them can be applied to our symbolic mocel for the Neufchâtel protocol. This is why we consider several fixed values for k.

P | Q « Q | P ),
The security properties together with corresponding the trust assumptions are summarized in Table 1 while the experiments are presented in Table 2.

Results

We run ProVerif version 1.94 on a Xeon E5-2687W v3 @ 3.10GHz. We were able to analyze cast-as-intended and individual verifiability up to k " 4 and ballot privacy up to k " 2. The detailed analysis times are reported in Table 2. The models in ProVerif can be found in [START_REF] Cortier | Proverif model for the neuchâtel e-voting protocol[END_REF]. As explained in Section 5.2, ballot privacy is expressed as an equivalence property of the form:

V A pa, bq | V B pc, dq « V A pc, dq | V B pa, bq
for k " 2, where a, b, c, d are constants. This implicity means that A and B vote for distinct options. So in the case k " 2 we further prove privacy when the two honest voters were respectively voting pa, bq, pb, cq, or pa, bq, pc, bq, or pa, bq, pb, aq, to check that no attack appears when A and B share one or two options. ProVerif proves these cases in exactly the same time than the case where the four options are pairewise distinct.

Lessons learned

Our analysis mostly confirms the security of the Neuchâtel protocol w.r.t. both privacy and verifiability properties. However, while modeling the protocol we discovered that flaws may occur in case of small but realistic deviations of the protocol. We reported these subtleties to the the company that designed the system who confirmed to be aware of them and that they have been taken care of for the actual implementation.

Exactly k choices. In case of an election where voters select k options out of n, with k ě 2, voters (and authorities) should be aware (and properly instructed) that voters should select exactly k options (and not less). Otherwise, a dishonest voting device may use the remaining "unused" choices for other unexpected voting options (and discard their return codes).

No duplicate. Still in case of an election where voters select k options out of n, voters should not be offered the possibility to vote twice for the same option (for example, the election rules may allow voters to give two choices to the same candidate). Indeed, the protocol would then be vulnerable to an attack where the intruder uses the duplicated choice (say Alice votes twice for a, that is, she votes a, a) to make her vote for a, b (and manually duplicate the return code corresponding to a, to make Alice happy).

Blank vote. It becomes particularly tricky for elections that allow voters to abstain (that is, vote "blank"). In that case, k different blank voting options must be provided to voters. Those blank voting options shall have different individual return codes, and voters shall be advised that they need to check a return code for each blank option. In other words, if Alice wishes to abstain in an election where voters can select k options out of n, then she must receive (and check) k distinct return codes, corresponding to k blank voting options. Of course, in case the election includes several questions (e.g., several sub-elections) then these blank options have to be specific to each question. This may be dificult to understand for voters.

Synchronization. As pointed before, the protocol is no longer secure w.r.t. the castas-intended property as soon as the voting server answers two different requests from the same voters. (Note that this is explicitly forbidden by the Neuchâtel protocol since revoting is not allowed). Therefore, the voting server must implement some form of thread synchronization to guarantee that two different ballots will never be accepted for the same id , even if none of them has yet been confirmed by the voter. This should be enforced even when voting servers are duplicated for efficiency reasons. In particular, the use of tables as described in [START_REF] Galindo | Neuchâtel's Cast-as-Intended Verification Mechanism[END_REF] is insufficient and further requires a proper lock mechanism.

Conclusion

We provide an automated proof of an e-voting protocol in use for politically-binding elections in the Swiss cantons of Neuchâtel and Fribourg. Our analysis confirms the security of the protocol: it ensures cast-as-intended and recorded-as-cast against a dishonest voting device (assuming an honest voting server) and it guarantees privacy against a dishonest voting server (assuming an honest voting device). Previous analysis of other e-voting protocols (eg [START_REF] Backes | Automated verification of remote electronic voting protocols in the applied pi-calculus[END_REF][START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[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] ) left several parts of the protocol undefined because they study protocols that have not been deployed for actual government elections. Our ProVerif model covers the authentication phase, voters' cryptographic keys derivation from passwords (as voters cannot be asked to copy long strings), no revote, as well as elections where voters may select several options. One particular challenging aspect of the Neuchâtel protocol is the fact that it forbids re-voting since it would be insecure otherwise. Due to ProVerif's over-approximations, we had to propose several ideas in order to still obtain automated proofs of all the desired properties.

As future work, we plan to explore how we could extend ProVerif in order to cope with protocols where some events happen only once. This is the case as soon as a protocol embeds some lock mechanisms or uses of counters.

TallyH pc t : channel , sk b : ekey, pk c : spkey, id a : agentId , id b : agentId q :" inpc t , p" id a , b a : any, sfc a : any, crf a : anyqq; inpc t , p" id b , b b : any, sfc b : any, crf b : anyqq; let pe a : any, prc 1 a : int, prc 2 a : int, " pk e pid a q, p a : anyq " b a in let pe b : any, prc 1 b : int, prc 2 b : int, " pk e pid b q, p b : anyq " b b in if verif zkp ppk b , pk e pid a q, e a , prc 1 a , prc 2 a , p a q ^verifyppk c , sfc a , crf a q ^verif zkp ppk b , pk e pid b q, e b , prc 1 b , prc 2 b , p b q ^verifyppk c , sfc b , crf b q then outpmix, e a q | outpmix, e b q | inpmix, e 1 a : anyq; inpmix, e 1 b : anyq; outpc, padecpsk b , e 1 a q, adecpsk b , e 1 b qqq; TallyDpc t : channel , sk b : ekey, pk c : spkey, id a : agentId , id b : agentId q :" inpc t , pid , b : any, sfc : any, crf : anyqq; let pe : any, prc 1 : int, prc 2 : int, " pk e pid q, p : anyq " b in if verif zkp ppk b , pk e pid q, e, prc 1 , prc 2 , pq ^verifyppk c , sfc, crf q ^id ‰ id a ^id ‰ id b then outpc, adecpsk b , eqq;

Figure 2 :

 2 Figure 2: Syntax of the core language of ProVerif.

Figure 4 :

 4 Figure 4: Transitions between configurations.

  pub e pekeyq : epkey, aencpepkey, any, intq : any, encpsymkey, anyq : any, pair pany, anyq : any, sk s pagentId q : skey, pub s pskeyq : spkey, signpskey, anyq : any u R stand " t adecpk, aencppub e pkq, m, rqq Ñ m decpk, encpk, mqq Ñ m proj 1ppair pa, bqq Ñ a proj 2ppair pa, bqq Ñ b verifyppub s pkq, m, signpk, mqq Ñ ok u

Figure 7 :

 7 Figure 7: The Tally Process -Honest version

Figure 8 :

 8 Figure 8: The Tally Process -Dishonest version

  cc id pcc id q sk id get sfc, crf id from M check if crf id valid add pid , sfc, crf id q to cb sfc if sfc " sfc id sfc

	Voter		VD		Voting Server
	pwd id , v1, v2,		pk b		pk b , gka , pkc, M,
	cc id , sfc id ,				tks id u, tables bb, cb
	tsrc id i u	pwd id , v1, v2		id
				ks id
		src1, src2	get sk id	b src1, src2	check if b valid add pid , bq to bb
	check v.s.
	src id v 1 , src id v 2
	voting success
		Figure 1: Overview of Neuchâtel Voting Protocol
	as those used in e-voting systems, make those proofs even more error-prone and thus
	harder to verify.

  t. to a set of names N pub is a process Q such that fnpQq Ă N pub and Q uses only public constructors(and destructors). In what follows, all constructors are public, unless otherwise specified. N priv q,P Y tnew a : T ; P u Ñ pN pub , N priv Y ta 1 uq, P Y tP ra 1 {asu wherea 1 R N pub Y N priv E,P Y toutpN, M q; Q, inpN, xq; P u Ñ E,P Y tQ, P rM {xsu E,P Y tlet x " D in P u Ñ E,P Y tP rM {xsu if D ó M and M ‰ fail E,P Y tif φ thenP u Ñ E,P Y tP uif φ " J E,P Y teventpM q; P u Ñ E,P Y tP u

	E,P Y t0u Ñ E,P
	E,P Y tP }Qu Ñ E,P Y tP, Qu
	E,P Y t!P u Ñ E,P Y tP, !P u
	pN pub ,

  Table then proceed and add id to Table else stop However, since the voting device may process several requests at the same time, checking whether id R Table is actually insufficient. Indeed, if two requests from the same voter reach the server at the same time, they would both pass the test id R Table and both ballots would be accepted. We therefore need a clean lock mechanism, for which there is a lot of implementation support.

  1 , src 2 qq; any, prc 1 : int, prc 2 : int, "pk e pid q, p : anyq " b in (* Parse it. *) if verif zkp ppk b , pk e pid q, e, prc 1 , prc 2 , pq then (* Checks the proof. ) let src 1 " read RC pf pgk a , prc 1 qq in (* Gets the short return codes. *) let src 2 " read RC pf pgk a , prc 2 qq in outpc, psrc 1 , src 2 qq; let sfc id : any " read FC pf pgk a , cmqq in (* Gets the finalization code. *) if verifyppk c , sfc id , crf q in (* Checks the signature.

		(* ... transmit codes.	*)
	inpc 1 , cc id : intq;	(* Get confirmation code	*)
	outpc 2 , prcpsk id , cc id qq;	(* ... transmit it.	*)
	inpc 2 , sfc id : anyq;	(* Get short finalization code *)
	outpc 1 , sfc id q.	(* ... transmit it.
		(* Recovers the keystore,	*)
	outpc, ksq;	(* ... and transmits it.	*)
	inpc, b : anyq;	(* Waits for a ballot.	*)
	let pe : (* Sends them to the Voter.	*)
	! inpc, cm : intq;	(* Waits for confirmation.	*)

*)

Figure

5

: The Device Process Server pc : channel , pk b : epkey, gk a : symkey, pk c : spkey, c t : channel q :" inpc, id : agentId q;

(* New voting requests. *) let pks : any, crf : anyq " Getpid , gk a q in *) eventpInsertBB pid , eqq;

(* Table

addition

. **) eventpHasVoted pid , eq;

Table 1 :

 1 Properties and trust assumptions. D stands for dishonest while H stands for honest.

	we still

Table 2 :

 2 Security analysis in ProVerif.

Results and lessons learnedPrevious symbol models of electronic voting protocols[START_REF] Backes | Automated verification of remote electronic voting protocols in the applied pi-calculus[END_REF][START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[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] consider a simple scenario where the voter selects one candidate among finitely many options. In

Acknowledgments

This work has been partially supported by the European Research Council (ERC) under the European Union's Horizon 2020 research (grant agreements No 645865-SPOOC).


M M S Sarr

Serge Pinto

Alain Ghio

Robert Espesser

Gilles Pouchoulin

Bernard Teston

François Viallet

A Pinto

R Ghio

G Espesser

B Pouchoulin

F Teston

Viallet

Laryngeal resistance as a marker of altered aerodynamic mechanism in parkinsonian dysarthria

BACKGROUND OBJECTIVE PATIENTS AND METHODS

RESULTS

CONCLUSIONS

Laryngeal resistance (LR) is a parameter able to further document the laryngeal activity by linking two aerodynamic dimensions (Smitheran and Hixon, 1981, J Speech Hear Disord 46, 138-146): LR is the ratio between the estimated subglottal pressure (ESGP) and the oral airflow (OAF).

Subglottal pressure and its temporal course within a sentence production is relevant for evaluating speech motor control, particularly pneumophonic coordination. If subglottal pressure is difficult to estimate non-invasively, several methods have been developed and are used to estimate indirectly this parameter (Bard et al., 1992, Ann Otol Rhinol Laryngol 101, 578-582;Jiang et al., 1999, Laryngoscope, 425-432;Jiang et al., 2006,. Laryngoscope, 89-92). We decided to measure the estimated subglottal pressure (ESGP), which is known to be equivalent to the subglottal pressure during the occlusive consonants (Laukkanen et al.. 2006. J Voice 20. 25-37), just before voicing (see figure below).

For all /pa/ syllables. ESGP and OAF measurements showed significant differences (p < 0.001) between control subjects and patients off L-dopa, patients presenting reduced values as a reflect of the disease impact.

To determine the aerodynamic relevance of laryngeal resistance in

STATISTICAL ANALYSIS

A linear mixed model (R software. version 2.6.2. http://www.r-project.org) was estimated. for group analyses integrating patient and p consonant as random terms. with a statistically significance level at p<0.05. This was not the case for the LR ratio, which displayed a striking increase specifically on the stressed syllable (second /pa/): this data is the result of a supplementary OAF decrease independent from the ESPG reduction. possibly reflecting an "active" strained glottis.

No significant difference was observed for the LR ratio concerning the latter syllables: as if the LR was progressively normalized, whereas the ESPG became stabilized thus resulting in a restored OAF.

The

  Parkinsonian dysarthria. LR, as previously reported for ESPG (Sarr et al., Revue Neurol, 2009), can thus be considered as a marker of altered aerodynamic mechanisms in PD dysarthria. It appears to be a useful, non-invasive and relevant parameter to be measured in order to assess speech motor control deficits in PD. Speech production in PD seems to benefit from various motor compensation strategies, as observed for limb movements. Vocal forcing may be one of these strategies, leading to an active control of laryngeal activity that have also to deal with PD rigidity. SPEECH PRODUCTION TASK Production of the following sentence in French «PaPa ne m'a Pas Parlé de beau-PaPa», within which measurements were made upon the 6 /p/ occlusive consonants. ESPG (hPa) = subglottal pressure during the occlusive consonant, just before voicing. Control oral airflow is at level 0. Spl (dB) = vocal intensity during the vowel following occlusive consonants. ESPG was measured at every p consonants while the OAF was measured on each vowel /a/ following the p consonant. EVA system (Ghio & Teston, 2004, International Conference on Voice Physiology and Biomecanics, Conference proceedings, 55-58) was used for data recording; analysis was performed using the Sesane environment (SQLAb, Aix-en-Provence, France; http://www.sqlab.fr/).

  of fact. it is important to consider laryngeal resistance -LR -as a means to assess globally and dynamically laryngeal rigidity in Parkinson's disease (PD).

Acknowledgments -This work was supported by grants from France Parkinson Association and PHRC 2003. Many thanks to patients and surgery teams of Marseille. Nice and Grenoble.