G Ch

Satie

H Ben

Ahmed Satie

A Real-Time Congestion Control Strategy in Distribution Networks

Keywords: Distributed Optimisation, Peer-to-peer, Distribution System Operator, Cost Allocation, Real-Time, Flexibility, Congestion Management

This paper proposes an algorithm for real-time congestion management in a distribution network. It sets up a peer-to-peer market allowing the distribution system operator to inject network charges. This enables him to obtain flexibility from distributed agents with heterogeneous preferences. These network charges vary in real time and are related to the network's congestion. Prosumers minimize their cost function, and find a consensus through alternating direction method of multipliers decomposition. This formulation allows the management of the large number of agents present in the distribution networks only using one price broadcast by the distribution system operator to prosumers. We illustrate with the CIGRE low voltage test case that this strategy is efficient to manage congestion and presents limited suboptimality compared to the optimal power flow.

INTRODUCTION

The deployment of Distributed Energy Resources (DERs) alters the management paradigm of distribution networks which will host 99% of new DER infrastructures [START_REF] Dutrieux | Assessing the impacts of distribution grid planning rules on the integration of renewable energy sources[END_REF]. Electrical consumption is expected to drastically rise [START_REF] Bussar | Large-scale integration of renewable energies and impact on storage demand in a European renewable power system of 2050-Sensitivity study[END_REF] because of new uses -electric mobility, heat pump -exposing it to risks of congestion and non-compliance with voltage limits [START_REF] Aziz | PV Penetration Limits in Low Voltage Networks and Voltage Variations[END_REF]. However, the violation of thermal constraints can lead to the premature aging of conductors or even to blackouts, which represent a significant additional cost for the Distribution System Operator (DSO). Currently, these constraints are managed through long-term physical network reinforcement [START_REF] Vahidinasab | Overview of Electric Energy Distribution Networks Expansion Planning[END_REF]. However, the introduction of distributed flexibilities creates a possibility of new management of the network, which is essential to achieve energy transition while limiting the costs of new infrastructures [START_REF] Morstyn | Designing decentralized markets for distribution system flexibility[END_REF]. This transition is facilitated by the widespread deployment of smart meters [START_REF] Wang | Review of Smart Meter Data Analytics: Applications, Methodologies, and Challenges[END_REF] which enables limited yet bilateral information exchange between DSO and prosumer. But currently, DSOs do not have efficient means of controlling large numbers of agents in real time.

Within the Demand Response (DR) literature, two types of approach stand out. In incentive-base DR programs, agents are offered payments in order to deliver a specific amount of load reduction. In price-based DR programs, consumers voluntarily provide load reductions by responding to economic signals [START_REF] Paterakis | An overview of Demand Response: Key-elements and international experience[END_REF]. The purpose of these programs is to match production and consumption. But fluctuating prices rarely reflect the price of using the network and to our knowledge are never used to solve the constraints associated with it.

A new market design focused on the interaction between DSO, aggregator and prosumers, opt-in for prosumers and that satisfies Pareto efficiency was proposed in [START_REF] Morstyn | Designing decentralized markets for distribution system flexibility[END_REF]. The DSO can manage network constraints by buying flexibilities from the agents, but the negotiation mechanism is not suited to real-time application. Alternatively, Steriotis [START_REF] Steriotis | A novel behavioral real time pricing scheme for the active energy consumers' participation in emerging flexibility markets[END_REF] proposed a real-time pricing scheme that offers an easily adjustable level of financial incentives to consumers, by fairly rewarding the desirable consumption changes. But prosumers have to announce their future consumption to the aggregator which can lead to privacy issues. Finally, Lu [START_REF] Lu | A Real-Time Alternating Direction Method of Multipliers Algorithm for Nonconvex Optimal Power Flow Problem[END_REF] proposed to handle constraints directly by solving an Optimal Power Flow (OPF) in a distributed manner taking advantage of the radial structure of the distribution networks to obtain an exact relaxation of the problem. Real-time resolution is made possible by warm-starting the algorithm by using the offline scheduling solution as the initial point. However, it does not directly involve prosumers in the decision making. On the other hand, peer-to-peer (P2P) markets are able to process a large number of agents with heterogeneous and private preferences (i.e. renewables, zonal) without increasing the computational complexity [START_REF] Sousa | Peer-to-peer and community-based markets: A comprehensive review[END_REF]. It is the most generic formulation because any market configuration can be expressed as a P2P market [START_REF] Baroche | Prosumer markets: A unified formulation[END_REF]. In addition, fluctuating pricing helps with involving prosumers by making them more responsible [START_REF] Albadi | Demand response in electricity markets: An overview[END_REF]. A P2P market was proposed in [START_REF] Baroche | Exogenous Cost Allocation in Peerto-Peer Electricity Markets[END_REF] to solve economic dispatch while introducing an exogenous grid price. This provides the system operator with a lever to compel market agents to comply with grid physical constraints. A consumption decrease proportional to the agents' flexibility was observed when price increases. This algorithm is a good candidate but no rule was provided to fix the network charges in advance and the algorithm requires iterative bilateral communication with the SO.

Thus, supposing that a communication network lies on top of the electric grid, we propose a real-time implementation of [START_REF] Baroche | Exogenous Cost Allocation in Peerto-Peer Electricity Markets[END_REF] allowing the DSO to manage congestion in the network using only a broadcast price reflecting the network state. Section 2 presents the P2P formalism and how it can be used to solve electricity markets in distribution networks. Simulation results are presented and discussed in section 3 using a test case relying on the CIGRE low voltage network. Section 4 contains our conclusions and perspectives for further work.

METHOD

Peer to peer market

The general formulation [START_REF] Baroche | Exogenous Cost Allocation in Peerto-Peer Electricity Markets[END_REF] of a P2P market is given in [START_REF] Dutrieux | Assessing the impacts of distribution grid planning rules on the integration of renewable energy sources[END_REF]. Where P is the matrix of power trade p nm of agent n with agent m, ω n is the set of partners of n, f n is the cost function, p n is the power exchanged, p n and p n are respectively the minimum and maximum power limits. h n is a regularization function which condense all network constrains. It is equal to 0 if they are respected and +∞ if they are violated. min

P n∈Ω f n (p n ) + h n (p n ) (1a) s.t. P = -P T (1b) p n = m∈ωn p nm n ∈ Ω (1c) p n ≤ p n ≤ p n n ∈ Ω (1d) p n ≤ p nm ≤ p n n ∈ Ω (1e)
Baroche [START_REF] Baroche | Exogenous Cost Allocation in Peerto-Peer Electricity Markets[END_REF] proposed to replace h by an exogenous terms. These exogenous term would aim not only at allocating congestion-related costs but also at controlling prosumer demand via their sensitivity to energy prices. Hence, h can be replaced by a cost allocation function defined as

h n (p n ) = γ • p n ( 2
)
where γ is the network charge fixed by the DSO which represent the network's solicitation. Problem (1) can be efficiently solved using the Alternating Direction Method of Multipliers (ADMM) [START_REF] Boyd | Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers[END_REF]. The resulting decentralized negotiation mechanism [START_REF] Baroche | Exogenous Cost Allocation in Peerto-Peer Electricity Markets[END_REF] reads :

p nm k+1 m∈ωn = argmin (pnm)m∈ω n f n (p n ) + γ • p n (3a) + m∈ωn λ k nm p k nm -p k mn 2 -p nm +(ρ/2) p k nm -p k mn 2 -p nm 2 s.t. (1c)-(1e) λ k+1 nm = λ k nm -ρ(p k+1 nm -p k+1 mn )/2 (3b)
where penalty factor ρ > 0 and λ nm is the dual variable associated to the trade p nm . According to [START_REF] Boyd | Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers[END_REF], supposing cost functions f n to be closed, proper, and convex is a sufficient condition to ensure convergence of (3).

Real time implementation using rolling iteration warm start

Convergence of trades P towards the optimal trades requires a certain number of iterations which depends on the number of agents N Ω , the cost function f n and the parameter ρ. The core element of the proposed algorithm is that at each time t 0 , agents solve their local problems and enforce their decision with an effective power exchange p t0 n . The DSO then measures the grid state, updates grid cost value and broadcast it at the next time step t 0 + ∆t. For small ∆t values, the solution should always be close to the optimal. This concept has already been studied for optimal control and Hours [START_REF] Hours | A Parametric Nonconvex Decomposition Algorithm for Real-Time and Distributed NMPC[END_REF] has shown that a well chosen ρ keeps the residuals bounded. Indeed, we can assume that between two close instants, the power p * t0 n requested by agent n at t 0 is not very different from p * t0+∆t n . Similarly, the cost function f t0 n should be close to f t0+∆t n . We can therefore find ∆t such that the solution of ( 1) is almost identical at both times. Thus, we propose the algorithm 1.

Price evolution

The DSO is in charge of maintaining the network's integrity and must ensure that it is not congested. Although the distribution network's state is generally not well known because of the small number of sensors, we will consider that it is observable in real time, for example via an estimator [START_REF] Zhou | Gradient-Based Multi-Area Distribution System State Estimation[END_REF].

The DSO determines the most constrained line or voltage

l ′ = argmax l∈L I l /C l (4)
where I l and C l are respectively the current and the maximum current admissible in l. Any technique can be chosen to determine the price the network's cost : Machine Learning, Reinforcement Learning, Kalman filter, etc. but even simple solutions can work out as illustrated section 3.

TEST CASE AND RESULTS

Test case

Simulations 1 were carried out using panda power [START_REF] Thurner | Pandapower -An Open-Source Python Tool for Convenient Modeling, Analysis, and Optimization of Electric Power Systems[END_REF] on the single-phase CIGRE European LV distribution network [START_REF] Strunz | Benchmark Systems for Network Integration of Renewable and Distributed Energy Resources[END_REF]. Fig. 1 shows the network's topology. It is composed of 44 buses, 40 prosumers including 33 with solar panels. To model the power exchanged by each agent, we used the 1 minute time step time series from [START_REF] Street | Pecan Street Dataport[END_REF]. For illustrative purpose, agent's power and lines' capacity were adapted. A quadratic function is here used for each prosumer [START_REF] Morstyn | Designing decentralized markets for distribution system flexibility[END_REF]. However, in a real implementation, each agent is encouraged to implement the cost function f t n of their choice which can be the result of an internal cost-saving optimisation [START_REF] Nguyen | Maximizing the cost-savings for time-of-use and net-metering customers using behindthe-meter energy storage systems[END_REF].

f t n (p) = -F n • p t * n • p + 0.5 • F n • p 2 (5)
where p t * n is the objective power of the agent n at time t. F n represents the agent's sensitivity to a price fluctuation γ. The larger F n is, the less sensitive the agent will be to γ, and the closer the power obtained p t n will be to p t * n . In return, the agent will pay a high price to the DSO when the network is constrained. In this paper we have chosen to use a quadratic function because (3) is efficiently solved by [START_REF] Stellato | OSQP: an operator splitting solver for quadratic programstle[END_REF].

With the aim of achieving significant price fluctuations, we fixed agents' flexibility between 25 and 200. Only p * n changes over the course of the simulation. Agents 0 represents the external grid with infinite power. It is very flexible (F 0 = 0.1) and has a zero power objective (p * 0 = 0kW ). This agent can be used to manage the coordination between TSO and DSO although this is beyond the scope of the article.

As mentioned section 2.3, any technique can be chosen to set the network charges γ t , we illustrate with a PI regulator :

γ t = max 0 ; K p + 1 T i • dt • I t l ′ C t l ′ -1 (6)
where K p is the proportional gain, T i the integration constant and γ t the fluctuating grid cost at time t.

Time series analysis

The first two panels of Fig. 2 show the evolution of the powers exchanged by agent 10 (not very flexible) and agent 5 (very flexible). Objective (b) represents the agent's objective power, i.e. the minimum of its cost function p t * . Exogenous (a), OPF (c) and OPF without line limits (d) represent respectively the power exchanged by applying the Exogenous algorithm, OPF with line limits and OPF without constraints. This legend is common to the first 3 panels. We adopt the producer convention : p n > 0 means that the power is produced by the agent n. Agent 10 being inflexible, the exchanged powers p t n are equal to p t * 10 for all t, contrary to agent 5. Before minute 100, the exchanged powers (c) and (d) are equal because no constraints are active. The exchanged powers are lower than the target because the grid agent pushes self-consumption and forces the most flexible agents to consume less. After minute 100 the curves (c) and The third panel represents the evolution of the most saturated line during the simulation for the three algorithms. Without control (d), the network exceeds the thermal constraint from minute 100 and reaches at most 155%. (c) is the strategy that implements the OPF, so it respects the constraints. (a) respects the constraint in spite of slight overruns -a qualitative analysis is made section 3.3. Finally the last panel represents the evolution of the network charges γ t given by the PI controller. It is null when constraints are inactive.

The primal (7a) and dual (7b) residual expressed as a percentage of the power exchanged during the simulation represent the degree of agreement between agents.

r t+1 = n∈ω m∈ωn (p t+1 nm + p t+1 mn ) 2 / n∈ω m∈ωn (p t+1 nm ) 2 (7a)
s t+1 = n∈ω m∈ωn (p t+1 nm -p t nm ) 2 / n∈ω m∈ωn (p t+1 nm ) 2 (7b)
Fig. 3 shows the evolution of these residues during the simulation. They never exceed 2%. This means that the evolution of p * ,t is slow enough for the algorithm to remain at a reasonable consensus level.

Statistical analysis

The histogram of the line load rating is presented Fig. 4. Over the simulation period (250 minutes), only 1.7% of the lines exceed the maximum admissible current. The biggest overflow is 28% and appeared only once. The network charges are determined by a PI controller (section 2.3). The optimal values of K p and K i cannot be known in advance because of the difficulty to characterize the system composed of the network and its agents (whose cost functions are private). We perform an exhaustive search to determine the optimal pair.

Two metrics are proposed : the undelivered power (8a) and the maximum overflow in the lines (8b). For each simulation we have N Ω (number of agents in the network) values of P not delivered and N T (number of time step) values of L overflow . We choose to represent, for each metric, the median value and the 95% quantile.

p n not delivered = t |p t n,exo -p t n,OP F | t |p t n,exo | (8a) L t overflow = max i∈L l t i,overflow (8b)
Fig. 5a shows the median undelivered power for different K i , K p pairs. (K i , K p ) = (0, 0) corresponds to the performance of the algorithm without correction. Without correction, the undelivered power exceeds 7.5% for half of the agents and drops to 4.5% with the best setting. Fig. 5b shows that without correction, the undelivered power is higher than 48% for 5% of the agents. With the best regulation, it drops to 25%. Without corrector, the most overloaded line exceeds 8% of overload half of the time (Fig. 5c). With a corrector, the network is not under stress at all for at least half of the time. Finally Fig. 5d shows that the most overloaded line exceeds 37% of overload 5% of the time. With the best controller, it is reduced to 7.5%. Fig. 6 shows the influence of flexibility on the average network's charges per MWh. The trend suggests that the more flexible an agent is, the lower the cost. For example, the cost paid by agent 5 is 1.5 times lower than that of agent 10. This trend needs to be confirmed for larger networks with more agents. Simulations were performed on one core of an Intel Core i7-9850H 2.60GHz. Results presented in table 1 are for a 250 time steps simulation, which represents 250min simulated.

CONCLUSION

In this paper, we proposed a new algorithm to manage congestion in a distribution network in real time by broadcasting, through smart meters, a variable representing the cost of network usage. At each time step t, the agents retrieve the network charges γ t . Then, they compute the optimum of their cost function f t n and propose trades p t nm to the other agents. They directly apply the result of their minimization to the network (i.e., consume the power p t n ) without worrying about the convergence of the algorithm or the possible congestion this could create. The DSO then estimates the state of the network, in particular the maximum line congestion. It infers a price γ t+∆t with the goal of resolving congestions. The algorithm being peer to peer, it is scalable and able to manage a large number of agents without increasing the computation time -minimizations are performed locally by agents.

The proposed algorithm was tested on a modified version of the CIGRE low voltage 44-bus test system. We used a simple, yet effective, PI controler to set the network charges. The algorithm not only reduces the number of overloaded lines but also the amplitude of the overload. Moreover, in our case study, less than 5% of prosumers had a significant drop in their consumption.

This exogenous approach is a good candidate for future implementation of peer-to-peer markets with low involvement of the system operator, but it needs to be tested on a more representative test case that takes into account the realistic constraints of distribution networks -hundreds of agents and buses. Designing a more complex pricing system anticipating the agents' response should improve the algorithm's performance. Other types of pricing can be considered: for example, to maintain voltage in their operating limits, to manage unbalanced three-phase networks or to encourage producers and consumers in a different way. Other questions require additional investigation, in particular : is the grid costs universal for the whole grid or it only applies for the congested area ? If it is universal, agents in the network areas without congestion are unnecessarily penalized. If it is locational, it is not fair for those agents in the weaker network areas because they always lose money due to the imposed grid cost. In conclusion, this approach should not be seen as a way to generate revenue for the DSO in order to strengthen the network. It is a new emergency way of managing the network. The matter of redistributing the profit between agents equally remains an open question.

Fig. 1 .

 1 Fig. 1. CIGRE low voltage network 44-bus, with 40 prosumers including 33 with solar panels.

Fig. 2 .

 2 Fig. 2. Evolution of the power, network charges, maximum line loading and network charges γ t during the simulation.

Fig. 3 .

 3 Fig. 3. Primal and dual residual throughout the simulation

Fig. 4 .

 4 Fig. 4. Histogram of line loading percent for the Exogenous algorithm ((K i , Kp) = (0.01, 0.01)) and the OPF without constrains. Respectively 1.7% and 4.2% of the lines exceed the maximum admissible current. Biggest overflows are 28% and 58%.

Fig. 5 .

 5 Fig. 5. Sensitivity analysis for the PI controler. Fig. (a) and (b) represent the quantile of power deference between the exogenous algorithm and the OPF with line limits expressed in %. Fig. (c) and (d) represent the quantile of maximum loading expressed in %. Each value is taken for a specific K i and Kp pair.

Fig. 6 .

 6 Fig. 6. Influence of the flexibility (arbitrary range) on network charges paid. Agents 5 and 10 whose time series are given in Fig. 2 respectively very flexible and inflexible pay different prices for the same amount of energy.

Algorithm 1 :

 1 Real time congestion control

	Result: p n , ∀n ∈ Ω
	while True do
	for n ∈ Ω do
	Get the grid cost via DSO broadcast: γ t ;
	Get trades from other agents: p t mn , ∀m ∈ ω n ; Update dual variable: λ t nm ← (3b) ; Compute new power exchange: p t+∆t n ← (3a)
	;
	end
	DSO computes network charges : γ

t+∆t ← (6); t ← t + ∆t ; end

TABLE 1

 1

			Computation time
	Algorithm Exogenous OPF	OPF without constrains
	time (s)	23	263	258


Véronique Cortier

Alexandre Debant

Pierrick Gaudry

Stéphane Glondu

Belenios with cast as intended

Introduction

Electronic voting systems aim at guaranteeing simultaneously vote privacy (no one should know what/whom I voted for) and verifiability (my vote should be properly counted). These properties come with trust and distrust assumptions on the involved parties such as the voting server, the voting devices, the decryption authorities, or external auditors. A long-standing issue is the so-called cast-asintended property: a voter should be able to control that their vote has been properly encoded and cast with their proper intention, even if their voting device tries to send a different vote.

A simple and appealing approach has been proposed by Benaloh [4] about 15 years ago. When a voter selects a vote v, their device produces a ballot b and the voter is given the choice to either cast the ballot or audit it. In the latter case, the device must produce the randomness used to form the ballot. The randomness as well as the ballot b are then sent to a second device or a third trusted party to control that b indeed encrypts v. This procedure is repeated an unpredictable number of times until the voter is convinced that their voting device behaves as expected. This approach is simple and versatile. However, user studies have shown that it is hard to use and understand in practice [START_REF] Marky | What did I really vote for? On the usability of verifiable e-voting schemes[END_REF]. As a consequence, a few voters audit in real elections. Moreover, this mechanism may even threaten privacy in case voters are not properly instructed to audit ballots that contain votes that are independent of their real intention. For the Benaloh's mechanism to be truly secure, voters need to first roll a dice to decide whether they will vote or audit, and in the latter case, roll a dice to decide which candidate to use.

Our contribution. We propose an audit mechanism that is part of the voter's journey (no need to choose) and in which the audited ballot is the one actually cast. Our approach works as follows. When a voter selects a vote v, an integer a is chosen at random (between 1 and µ, a positive integer larger than the number of possible values for v) and the voter is given v, a, and b such that b = v +a mod µ. The corresponding ballot bal is formed of the respective encryption of v, a, and b, together with a zero-knowledge proof zkp that guarantees that the three ciphertexts encrypt values x, y, z such that z = x + y mod µ. bal = enc(v), enc(a), enc(b), zkp

The voting device commits to bal on the bulletin board. Then the voter asks their device to open either the second or the third encryption (chosen at random), by revealing the randomness used to produce the ciphertext. In order to modify v, the voting device needs to modify either a or b. Hence the voter will detect a malicious device with probability 1/2. This audit mechanism does not leak any information on v since a and b (considered separately) are perfectly random.

We integrate this mechanism into the Belenios protocol [START_REF] Cortier | Election verifiability for Helios under weaker trust assumptions[END_REF], yielding Be-leniosCaI. Belenios is an evolution of Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] that additionally provides eligibility verifiability. Belenios is used each year in about 2000 elections, that include a German political party and some EU institutions [START_REF] Cortier | Features and usage of Belenios in[END_REF]. We believe that our approach could be used to add cast-as-intended to other protocols as well. Interestingly, the computation overhead remains affordable. We show that we can encode the zero-knowledge proofs of modular equality into a standard proof of set membership. Overall, the computational cost and the size of ballots are about 2-3 times bigger than their counterparts in Belenios.

We formally prove that BeleniosCaI guarantees verifiability against a compromised voting device. We also show that BeleniosCaI preserves vote secrecy (assuming an honest voting device). Specifically, we provide a formal model of BeleniosCaI using the ProVerif tool [START_REF] Blanchet | An efficient cryptographic protocol verifier based on Prolog rules[END_REF], a well established tool for analyzing the security of protocols. This required to reflect the theory of modular arithmetic in ProVerif, which is typically out of range of this tool. Fortunately, we could re-use the model developed in [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF]. Verifiability is shown by excluding traces that do not satisfy some of the properties of modular arithmetic, using restrictions, a feature recently introduced in ProVerif [START_REF] Blanchet | ProVerif with lemmas, induction, fast subsumption, and much more[END_REF]. Vote privacy is more involved since it is expressed as an equivalence property where the attacker tries to distinguish between different voting choices. Considering sufficient conditions is no longer appropriate. Instead, we show (in ProVerif) lemmas on traces that then allow us to conclude thanks to a theorem of [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF].

Related work. The idea of using a two-checksum a and b with b = v +a mod µ has been firstly developed by Neff in [START_REF] Neff | Practical high certainty intent verification for encrypted votes[END_REF] for the specific subcase µ = 2. Then, the general case has been sketched in [START_REF] Cortier | A simple alternative to Benaloh challenge for the cast-as-intended property in Helios/Belenios[END_REF] and more thoroughly introduced in [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF] in the context of on-site voting. The proposed system involves printed papers with scratch-off parts, smartcards, and local observers. We adapt this idea to Internet voting, using the Belenios protocol, with many simplifications (e.g. we no longer request a and b to be of different parity).

Many Internet voting protocols have been proposed for cast-as-intended. We refer the reader to [START_REF] Marky | Investigating usability and user experience of individually verifiable internet voting schemes[END_REF] for a nice and comprehensive survey. This survey splits existing protocols into five categories: audit-or-cast, tracking data, verification devices, code sheets, delegation. Interestingly, our approach introduced a novel category that could be called audit-and-cast. We only review here the main families. In the code sheet approach, voters obtain printed code sheets during the setup, with one code assigned to each candidate. When voting for a candidate v, the voter receives a code and checks on their sheet that it indeed corresponds to v. This is the approach followed in Switzerland with CHVote [START_REF] Haenni | CHVote system specification[END_REF], as well as the protocol developed by SwissPost [1] or previously by Scytl [START_REF] Galindo | Neuchâtel's cast-as-intended verification mechanism[END_REF]. Such systems require a heavy infrastructure (e.g. a distributed voting server) and assume a honest printer that is in charge of most of the setup. Other code-sheet based systems include Demos [START_REF] Kiayias | End-to-end verifiable elections in the standard model[END_REF] and Pretty Good Democracy [START_REF] Ryan | Pretty good democracy[END_REF].

Some systems assume a (second) verification device. This is for example the case in Estonia [START_REF] Heiberg | Verifiable internet voting in Estonia[END_REF] where voters can use a second device and the randomness of their ballot to check it is well-formed. In Australia [START_REF] Brightwell | An overview of the iVote 2015 voting system[END_REF], voters simply call a server that opens their ballot and gives the vote in clear (with associated threats on vote privacy). Intuitively, BeleniosCaI allows to simplify so much the work of the second device (checking an addition) that it can be discharged on the voter.

Tracking systems include in particular sElect [START_REF] Küsters | sElect: A lightweight verifiable remote voting system[END_REF], Selene [START_REF] Ryan | Selene: Voting with transparent verifiability and coercion-mitigation[END_REF] and its successor Hyperion [START_REF] Ryan | Hyperion: An enhanced version of the Selene end-to-end verifiable voting scheme[END_REF]. They let the voter check that their vote appears on the public bulletin board, thanks to a voting tracker. The voter may detect a misbehavior only once the election is over. In Selene and Hyperion, the validity of the tracker needs to be checked with a second device (which, in return offers some protection against vote-buying).

Protocol description

We describe a voting protocol, BeleniosCaI, where voters have to select between k 1 and k 2 candidates among a list of n candidates. A vote can be represented as a vector (v i ) 1≤i≤n , where v i = 1 if candidate i has been selected and v i = 0 otherwise; the condition v i ∈ [k 1 , k 2 ] must be satisfied. An overview of the protocol is presented in Figure 1.

Participants and setup

Voters are identified with their email addresses, that will be used for authentication by the Server. We consider two distinct roles for the Voter and their Voting device since our protocol is designed to protect against a malicious Voting device (w.r.t. verifiability).

During the setup phase, the Registrar sends a private credential cred (a signing key) to each voter. It also sends the list of corresponding public verification keys to the Server. The k Decryption authorities set up the public key of the election pk E such that a threshold t of them can decrypt any message encrypted with pk E .

We assume a Public board that can be accessed at any time by all the participants. How to realize a public board in practice is out of the scope of this paper and is discussed for example in [START_REF] Hirschi | Fixing the Achilles heel of e-voting: The bulletin board[END_REF]. We also assume that at least one honest Auditor checks the validity of the ballots and all the cryptographic material that appears on the public board.

Voting phase

Ballot. Given a vote v = (v i ) 1≤i≤n and a credential cred, a ballot bal = (M, zkp, σ) is formed of an encrypted matrix M , a zero-knowledge proof zkp and a signature σ defined as follows. First, a vector of audit codes (a i ) 1≤i≤n is chosen uniformly at random, where 0 ≤ a i < µ, that is, each a i is a small integer (smaller than a "modulus" µ than can be thought as 2 or 10).

-The encrypted matrix M =   V 1 A 1 B 1 . . . V n A n B n   contains n lines. Each line is formed of V i , A i , B i where V i = enc(v i , pk E ) encrypts the choice v i , A i = enc(a i , pk E ) encrypts the audit code a i , while B i ties V i and A i together. Namely, B i = enc(b i , pk E ) where b i = v i + a i mod µ.
-The zero-knowledge proof zkp is formed of several zero-knowledge proofs that guarantee that:

• each V i encrypts either 0 or 1;

• the V i 's encrypt values v i such that k 1 ≤ Σ n i=1 v i ≤ k 2 . • for each 1 ≤ i ≤ n, V i , A i , B i encrypt some values v i , a i , b i such that b i = v i + a i mod µ.
-Finally, σ is the signature of M and zkp with the credential cred.

Voter experience. The voter selects their vote v on their voting device, that computes a ballot bal as described above. The voting device displays the vote v and h = hash(bal) to the voter, where h will be used as a tracking number. This step is illustrated in Figure 2a. The voter confirms their vote, and then the device sends the ballot bal to the voting server. The voter waits for an email from the server, that contains a confirmation challenge chal (used for authentication) and their tracking number h. If the tracking number is correct, they enter chal to their voting device and starts the audit phase, as illustrated in Figure 2b: the voting device displays the matrix in clear

m =   v 1 + a 1 = b 1 . . . v n + a n = b n  
the voter reviews the matrix m and checks that the sums are correct (taking µ = 10 can make this step easier); for each line, they select either a i or b i , yielding a bit δ i , where δ i = 0 if a i is selected and 1 otherwise.

Voter

Voting device Voting server Public board For each i, the voting device must reveal the randomness r i used to encrypt either a i or b i according to the selection of the voter. The voting device sends to the server the selection (δ i ) 1≤i≤n as well as the corresponding randomness (r i ) 1≤i≤n . For each line i, the server decrypts A i or B i , according to δ i , thanks to the randomness r i and reveals on the public board the corresponding a i or b i . Finally, the voter checks on the public board that their tracking number h appears, as well as their selection (δ i ) 1≤i≤n and the corresponding chosen integers. External auditors check that the decryptions of audit codes are valid, as well as the zero-knowledge proofs and signatures. Intuitively, even if the voting device is malicious, it must commit to values v i , a i , b i such that b i = v i +a i mod µ. Hence if the voting device wishes to change the vote v i of the voter, it must also modify a i or b i . This will be detected with probability 1/2 by the voter since they chose to see either a i or b i at random. Therefore, while a few votes may be modified without being detected, the attacker has a probability of 1/2 k to change k votes without being detected. This does not diminish vote privacy since only a random mask (either a i or b i ) is revealed. We provide a formal security analysis in the next section.

Server. As in Belenios, the Server only accepts well-formed ballots, that is, ballots such that the zero-knowledge proofs are valid and the signature corresponds to a valid public verification key. Moreover, the Server ensures that a voter always uses the same credential (in case of a revote) and that no two voters use the same credential.

Tally phase

As in Helios and Belenios, the encrypted votes (V i ) 1≤i≤n can be combined homomorphically in order to obtain an encrypted vector that corresponds to the total number of votes per candidates. The vector is decrypted by the Decryption authorities, who also provide a zero-knowledge proof of correct decryption.

Usability considerations

In theory, the modulus µ can be as small as 2. This is enough to perfectly mask a bit. However, we do not expect typical voters to be familiar with binary arithmetic. We suggest to use µ = 10, so that voters can do a classical addition, and are instructed to consider the units digit only, e.g. if the sum is 10, then we forget the 1 and get 0. Printing the 1 in gray can help as depicted in Figure 2b.

Choosing a random mask could be difficult since we expect the voters to be bad random generators in case there are many candidates. Assuming that voters can better pick numbers at random, one option is to ask voters to enter an at least 4-digit number (or maybe longer, if there are more than 13 candidates) instead of directly selecting the mask, and convert it to a mask using a predefined deterministic function. The server must then print both the mask and the number, so that the voter can check them.

Security Analysis

We conduct a security analysis of the BeleniosCaI protocol using the tool ProVerif.

ProVerif

ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on Prolog rules[END_REF][START_REF] Blanchet | ProVerif with lemmas, induction, fast subsumption, and much more[END_REF] is a state-of-the-art, automatic verification tool to prove the security of cryptographic protocols, including industrial-scale protocols such as TLS or Signal. ProVerif proves the security of protocols thanks to a (sound) transformation into first order logic. It (often) reports an attack trace when the proof fails. We recall here its main specificities and we present an overview of our model of BeleniosCaI. The full models are available the supplementary material accompanying this HAL document. A detailed description of the syntax and semantics of ProVerif can be found in [START_REF] Blanchet | ProVerif with lemmas, induction, fast subsumption, and much more[END_REF].

Messages ProVerif is based on the notion of a Dolev-Yao attacker model [START_REF] Dolev | On the security of public key protocols[END_REF] in which messages are abstracted by terms which are either an atomic data (e.g., a key, an unguessable random number, etc) or a function symbol applied to other terms. The semantics of a message is then provided by an equational theory and/or a rewriting system. For instance, a randomized asymmetric encryption scheme is modeled by a function symbol aenc of arity 3, a symbol adec of arity 2, and a symbol pk of arity 1. The possibility to decrypt an encrypted message using the correct secret key is then modeled by the rewriting rule: adec(y, aenc(pk(y), x, r)) → x where x is the plaintext message, y the secret key corresponding to the public key pk(y), and r the randomness used for encryption. Most cryptographic primitives can be modeled similarly (e.g., signature, hash function, zero knowledge proof).

Roles The different roles of the protocol are modeled through a process algebra inspired by the applied pi-calculus which includes the commands P |Q to model that the processes P and Q execute in parallel, and !P to model that an arbitrary number of process P can be executed in parallel. Moreover, communications on a (public or private) channel c are represented by actions in(c, x) and out(c, m) which respectively model that an agent is waiting for a message x on channel c, and an agent is sending a message m on c. In addition, the process may contain event actions that are used to identify specific steps in the process and to express some security properties. Finally, there are standard actions to model fresh unguessable name generations, conditionals, declarations, etc. For sake of simplicity, ProVerif supports the syntax in(c, =m); P as a shortcut for in(c, x); if x = m then P else 0. This notation will be used in Figure 3.

All the processes are executed using an operational semantics presented in [START_REF] Blanchet | ProVerif with lemmas, induction, fast subsumption, and much more[END_REF]. For instance, it formally defines that a message u can be received through an input in(c, x) as soon as there exists an action out(c, u) to execute, or if the channel c is public and the attacker is able to deduce the message u from its knowledge. Roughly speaking, the semantics formalizes the intuitive execution of the processes that the reader might think of.

Example 1. Figure 3 presents as a concrete example the process used to model the voter role. We assume that the voter securely receives their secret signing key and knows their id and the channel they will use to communicate with their device (e.g. monitor, keyboard, mouse, etc). Finally, we assume a public channel c that will be used to communicate with the environment (i.e. the attacker).

The process then corresponds to the voter experience described in Section 2.2. First (l. 2-4), the voter sends their choice to their device. Second (l. 6-7), the voter reads on their device the ballot tracker and reviews their choice before confirming their vote. Third (l. 9-11), the voter receives an email from the server that contains a ballot tracker and a challenge. The ballot tracker must correspond to the one displayed on the reader. If this is the case, the voter enters their challenge in the device. Fourth (l. 13-18) the audit phase starts: the device displays the ballot and the corresponding audit codes, the voter checks the well-formedness of the ballot (i.e. b = x+a). The event isSum(x B , v, x A ) is executed to model the check of the sum. The voter ends this phase by randomly choosing which code will be audited. Finally, (l. [START_REF] Haenni | Improving the performance of cryptographic voting protocols[END_REF][START_REF] Heiberg | Verifiable internet voting in Estonia[END_REF][START_REF] Hirschi | Fixing the Achilles heel of e-voting: The bulletin board[END_REF][START_REF] Kiayias | End-to-end verifiable elections in the standard model[END_REF][START_REF] Küsters | sElect: A lightweight verifiable remote voting system[END_REF][START_REF] Marky | What did I really vote for? On the usability of verifiable e-voting schemes[END_REF][START_REF] Marky | Investigating usability and user experience of individually verifiable internet voting schemes[END_REF][START_REF] Neff | Practical high certainty intent verification for encrypted votes[END_REF][START_REF] Ryan | Hyperion: An enhanced version of the Selene end-to-end verifiable voting scheme[END_REF][START_REF] Ryan | Selene: Voting with transparent verifiability and coercion-mitigation[END_REF], the voter reads on the public bulletin board and look for an entry that matches their ballot tracker, and the expected audit codes. If everything is correct, then the voter is "happy" and can be sure that their vote will be counted, and that the ballot contains their intended choice.

The other roles of the protocol (i.e. voting device, server, tally) are modeled in a similar way.

Security properties ProVerif supports two main classes of security properties: trace properties and equivalence properties.

The trace properties express that specific bad states cannot be reached during the execution of the protocol. These are expressed using correspondence queries of the form i∈{1,...,n} ) else out(c_error, ERROR)

E i ⇒ i∈{1,...,

29

) else out(c, ERROR) Fig. 3: ProVerif process modeling the voter actions.

which models that whenever the events E 1 , . . ., E n are executed during an execution then there must exist i 0 ∈ {1, . . . , m} such that all the facts (i.e. events, equalities, disequalities, etc) F i0,1 , . . ., F i0,p hold too. This type of queries are used to express for instance authentication, confidentiality, or integrity. In the context of our security analysis it will be used to express verifiability properties. The equivalence properties model that two processes P and Q cannot be distinguished by an attacker interacting with them, denoted P ≈ Q. For sake of simplicity, we intentionally decide to not recall here the formal definition of the notion of equivalence that ProVerif verifies (see [START_REF] Blanchet | ProVerif with lemmas, induction, fast subsumption, and much more[END_REF] for details). In our context, this notion of equivalence properties will be useful to model vote secrecy.

How to overcome ProVerif 's limitations?

The underlying symbolic model of the ProVerif tool has two main limitations to model the BeleniosCaI protocol. First, it does not allow to model associative and commutative operators which prevents an accurate modeling of the arithmetic operations in Z/µZ. Second, it does not model probabilistic actions that would be necessary to faithfully describe the audit mechanism of BeleniosCaI. To overcome these limitations, we leverage techniques developed in [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF]. We recall here an overview of them but a detailed description and a proof of their correctness is available in the original paper.

Arithmetic operations

To model the sum in Z/µZ, we assume that an event isSum(x, a, b) is executed each time an agent verifies that x = a+b mod µ. These events records all the equalities that must hold. Based on these events, two approaches are developed in [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF] depending on the security property under study: first, for trace properties, it models the subset of properties which are relevant to make the audit mechanism secure. Specifically, it restricts the analysis to execution traces that satisfy these properties using restrictions. For example, we model that "for all a, b ∈ Z/µZ there exists a unique x ∈ Z/µZ such that x = a + b mod µ" using the restriction isSum(x, a, b) ∧ isSum(x, a, b ) ⇒ b = b . Other properties are modeled in the same way. These properties are trivially satisfied by the modular arithmetic, and actually sufficient for our verifiability properties.

Second, for equivalence properties, [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF] proposes an approach based on relation preservation between the traces of the two processes P and Q we want to prove equivalent. Note that the previous approach, based on an over-approximation of the sum relation in Z/µZ would be unsound for equivalence properties. Hence, [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF] proposes to prove equivalence of processes P and Q as follows: (1) show that for any trace tr P of P there exists an indistinguishable trace tr Q of Q, and (2) if an event isSum(x, a, b) is executed in P then the same event is executed in tr Q . The first item corresponds to the standard trace equivalence property that can be proved as usual in ProVerif, and the second item is the relation preservation property. It can be proved in ProVerif too by defining a specific lemma. An immediate consequence of item ( 2) is that, if the relation induced by the events isSum(x, a, b) models the sum in Z/µZ in tr P then it remains true in tr Q . A detailed description of this approach and its soundness is provided in [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF].

Probabilistic actions ProVerif does not handle probabilistic actions, and thus cannot faithfully model the random choice done by the voter to perform the audit. Like [START_REF] Bougon | Themis: an on-site voting system with systematic cast-as-intended verification and partial accountability[END_REF], to be able to conduct the security analysis, we decided to make the following reasoning on top of the modeling: because an attacker cannot know in advance which code the voter is about to audit, the attacker must be able to provide data that make the audits valid for both codes. Therefore, we model that the voter audits both codes for verifiability when it is necessary to avoid false attacks. Concretely, this means that, regarding Figure 3, a third case is added for audit:

1 if audit_choice = 2 then (

Security analysis and result

We proved the security of the BeleniosCaI protocol regarding vote secrecy and verifiability. Following the approach developed in [START_REF] Cortier | BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device[END_REF][START_REF] Baloglu | Election verifiability revisited: Automated security proofs and attacks on Helios and Belenios[END_REF], we consider 3 subproperties to model E2E verifiability: cast-as-intended to model that the voter can verify their ballot contains their intended vote, no clash attack to model that two voters should not agree on the same ballot, and recorded-as-cast to model that an attacker cannot create nor modify a ballot in the name of an honest voter. In this security analysis, we deliberately omit the eligibility property because it remains exactly the same as the current version of the Belenios protocol (eligibility is performed by both the registrar and the server).

To formalize these security properties, we define the following events:

-onBoard(vk, h, b, r, X) is executed each time a ballot b is added to the public bulletin board. vk is the public key associated to the signature occurring in b, h is the ballot tracker associated to b (i.e. h = hash(b)) and (r, X) is the data published to conduct the audit. -Honest(id, vk) is executed each time an honest voter id is registered with the public signing key vk. -HasInitiatedVote(id, vk) is executed when the voter id with the public signing key vk has initiated a vote. -Voted(id, vk, h) is executed when the voter id with the public signing key vk has confirmed their vote using the ballot tracker h. -HappyV(X, id, h, v) is executed when voter id has completed the audit using the ballot tracker h and intended to vote for v. X ∈ {L, R, LR} records whether the voter audited the Left, the Right, or both (for modeling) codes.

Vote secrecy. As usual in the symbolic analyses, we consider the vote secrecy definition proposed by Kremer et al. [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]: an e-voting protocol ensure vote secrecy if an attacker is not able to distinguish whether Alice voted for 0 and Bob for 1, or conversely. Formally, we note Alice(x) (resp. Bob(x)) the process modeling the role of Alice (resp. Bob) when voting x, and P the process modeling all the other roles involved in the protocol then we want to prove that:

P |Alice(0)|Bob(1) ≈ P |Alice(1)|Bob(0).

Cast-as-intended. A protocol ensures cast-as-intended if the voter is able to verify that their ballot will be counted and contains their intended vote. We consider the following correspondence property to model cast-as-intended:

HappyV(LR, id, h, v) ∧ Honest(id, vk) ⇒ onBoard(vk , b, h, r, X) ∧ (b encrypts candidate v).

No clash attack. A protocol protects against clash attacks if two voters cannot agree on the same ballot. When honest devices are used, they generate ballots with different randomness, which ensure the no-clash property. This is no longer true if the voting devices are malicious and collude: they may use the same randomness and make Alice and Bob believe they own the same ballot. Interestingly, the no-clash property still holds in BeleniosCaI thanks to the fact that voters randomly choose whether they audit the left or the right code. We therefore model the no-clash property for voters that audit differently:

HappyV(L, id, h, v) ∧ HappyV(R, id , h, v ) ⇒ false.
Note that this property is weaker than the original no-clash property, that does not need to make assumptions on voter's (audit) choices.

Recorded-as-intended. A protocol ensures recorded-as-intended if an attacker is not able to forge a ballot in the name of an honest voter. This corresponds to the following correspondence property1 : onBoard(vk, h, b, r, X) ∧ Honest(id, vk) ⇒ Voted(id , vk, h).

(1)

Unfortunately, this property is not satisfied by BeleniosCaI when the voting device and the server are compromised. Indeed, as soon as the voter initiates a vote, they reveal their credential which lets the attacker completely impersonate them. We thus define a weaker property, that says that an attacker is not able to forge a ballot in the name of an honest voter, unless the voter has started a voting session:

onBoard(vk, h, b, r, X) ∧ Honest(id, vk) ⇒ HasInitiatedVote(id , vk). (2)

Remark 1. Regarding the literature, it seems that protocols known to be verifiable assuming a compromised voting device guarantee only Property 2. This is the case, for instance, of Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] or Selene [START_REF] Ryan | Selene: Voting with transparent verifiability and coercion-mitigation[END_REF]. Still, other protocols such as the Swiss Post [1] or BeleniosVS [START_REF] Cortier | BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device[END_REF] For interested readers, Table 2 presents the detailed results of the security analysis conducted in ProVerif. The ProVerif files are available in the supplementary material accompanying this HAL document. This table details the weakest trust assumptions in which each security property is ensured by BeleniosCaI: the less trustworthy agents there are, the more secure the protocol is. For instance, line 4 shows that the strong notion of recorded-as-cast is ensured as soon as the server is honest (i.e. even if the voting device or the registrar are compromised). Indeed, if the server is honest then the attacker will not be able to learn the challenge code sent by mail to the voter, and thus will not be able to confirm a maliciously created ballot in the name of the voter.

Voter Voting device Server Registrar Dec. auth.

Cast-as-intended

No clash

Recorded-as-cast (strong)

Recorded-as-cast

Vote secrecy

= trustworthy = compromised

Table 2: Minimal trust assumptions for each security property.

Efficiency considerations

A ballot in Belenios or Helios essentially costs one ciphertext and zero-knowledge (individual) proof per candidate, plus one zero-knowledge (overall) proof that controls the number of selected candidates. BeleniosCaI requires two extra ciphertexts and a proof of modular equality for each candidate. This essentially adds a factor between 2 and 3 to compute the ballot, as we detail now.

The zero-knowledge proofs required for forming the ballots can all be expressed as statements of the form "The cleartext of this ciphertext belongs to this finite set of possible values".

-Individual proofs. Each v i belongs to {0, 1} is already in this form. This is therefore a list of 0/1 proofs. The basic approach requires 5 exponentiations. See [START_REF] Haenni | Improving the performance of cryptographic voting protocols[END_REF][START_REF] Devillez | How to verifiably encrypt many bits for an election?[END_REF] for ways to optimize them. -Overall proof. The sum of all the v i 's is between k 1 and k 2 . Due to the homomorphic property of ElGamal encryption, anyone can compute the ciphertext of this quantity, from the list of the V i 's, so that we are indeed in the claimed setting. Proving the property is then classically done as in Helios or Belenios, by rewriting it as belonging to a set of integers, with a cost that is linear in k 2 -k 1 . Techniques exist to do this at a cost in O(log(k 2 -k 1 )) [START_REF] Canard | New results for the practical use of range proofs[END_REF]. -Arithmetic proofs. The fact that V i , A i , B i encrypt some values v i , a i , b i such that b i = v i + a i mod µ can be rewritten as follows. First, by the homomorphic property, anyone can build the ciphertext that encrypts v i + a i -b i (without the modulo µ, that can not be computed homomorphically). By construction, if the ballot is correctly formed, this value must be equal to 0 or to µ. Therefore, this arithmetic proof can be rewritten as a proof of membership in a set of two elements, which is almost the same as the classical 0/1 proof. It therefore requires 5 exponentiations.

In Belenios, there is the possibility to have a special candidate representing a blank vote, and this comes with a zero-knowledge proof that either the blank vote is chosen and all the v i 's are zero, or the blank vote is not chosen, and then the sum of the v i 's is in [k 1 , k 2 ] (see [START_REF] Gaudry | Some ZK security proofs for Belenios[END_REF]). Our method supports this setting: it is enough to add an arithmetic proof for this additional encrypted bit.

We also mention that in the security analysis, there is no need to have zeroknowledge proofs of the facts that the a i 's and the b i 's are in [0, µ-1]. If, for some practical reasons, the server needs to detect early invalid ballots, these proofs can be added. They are of the same nature as the overall proof. However, they can be costly for the voting device of the voters, if there are many candidates.

To sum-up, compared to Belenios, for the voting device, the additional cost of forming a ballot is, for each candidate, to compute two ElGamal encryptions A i and B i , and to compute the arithmetic proof for them. This amounts to 9 additional exponentiations per candidate. Techniques like in [START_REF] Devillez | How to verifiably encrypt many bits for an election?[END_REF] can be used to reduce this cost. As a rule of thumb, we can say that this will multiply the running time of forming a complete ballot by a factor between 2 and 3, the exact number depending on the number of candidates and the value of k 2 -k 1 . For elections for which there are no more than a few dozens of candidates, this remains affordable with a Javascript/WebAssembly implementation running in a standard browser, and there is no need to have a native implementation (which would raise many issues, since this usually requires to install specific software).

Makes a choice vFor 1 10

 1 Fig. 1: Description of the voting phase of the BeleniosCaI protocol

Fig. 2 :

 2 Fig. 2: Two steps of the voter's journey.

2 3 event 4 )

 34 if x_ballot_tracker_bb = x_ballot_tracker && x_codes = (x_A,x_B) then ( HappyVoter(id_voter,x_ballot_tracker,v); 0 else out(c, ERROR)

  ∧ T] [VD ∧ T] [VD ∧ T] E2E verifiability (strong) (including cast-as-intended) E2E verifiability (including cast-as-intended) Vote secrecy = proved secure VD=voting device, R=registrar, S=server, T=dec. auth., = attack [.]= extra trust assumption for vote secrecy only

  m} j∈{1,...,p}

	1	Voter(id, c_device, ssk_id) =
	2	in(c, v);	(* voter's choice chosen by attacker, to consider all cases *)
	3	event HasInitiatedVote(id,v);
	4	out(c_device, (v,ssk_id));
	5
	6	in(c_device, (=v, x_ballot_tracker));
	7	out(c_device, OK);
	8
	9	in(c_mail(id), (=x_ballot_tracker, x_chal));
	10	event Voted(id,x_ballot_tracker,x_v);
	11	out(c_device, x_chal);
	12
	13	in(c_device, x_ballot_plaintext);
	14	let (=v, x_A, x_B) = x_ballot_plaintext in
	15	if x_A <> blind_code && x_B <> blind_code then
	16	event isSum(x_B,v,x_A);
	17	in(c, audit_choice);	(* audit choice chosen attacker, to consider all cases *)
	18	out(c_device, audit_choice);
	19
	20	in(cell_BB, (x_vk, x_ballot, x_ballot_tracker_bb, x_rands, x_codes));
	21	if audit_choice = 0 then (
	28
				F i,j

22 if x_ballot_tracker_bb = x_ballot_tracker && x_codes = (x_A,blind_code) then ( 23 event HappyVoter(id_voter,x_ballot_tracker,v); 0 24 ) else out(c_error, ERROR) 25 ) else if audit_choice = 1 then ( 26 if x_ballot_tracker_bb = x_ballot_tracker && x_codes = (blind_code,x_B) then ( 27 event HappyVoter(id_voter,x_ballot_tracker,v); 0

  ensure Property 1. Hence, we considered interesting to analyze the security of BeleniosCaI w.r.t. these two properties, as presented in Table1 and 2. Recorded-as-intended corresponds to Property 2 and recorded-as-intended (strong) to Property 1.Results Table1presents the main results of the security analysis: BeleniosCaI is as secure as Belenios if we assume that the voting device is honest, i.e. it requires that either the registrar or the server is honest to ensure verifiability and that the decryption authorities are honest for vote secrecy. Moreover, it still provides verifiability when considering a malicious voting device: if the server is honest then it meets the same verifiability property as Belenios (strong E2E verifiability), while if the registrar is honest, then it ensures (only) the E2E verifiability. From the vote secrecy point of view, BeleniosCaI and Belenios are both secure as soon as enough decryption authorities are honest.In summary, these results demonstrate that BeleniosCaI provides strictly better security guarantees than Belenios.

Table 1 :

 1 Security analysis of BeleniosCaI: minimal trust assumption.

This correspondence property identifies voters by their public signing key. This assumption is valid as long as the registrar is honest. Otherwise, when the server is honest, they can be identified by their id and a similar property is defined. This distinction corresponds to the approach developed in[START_REF] Cortier | BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device[END_REF].

This work received funding from the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006