{'fraction_non_alphanumeric': 0.053161691351392835, 'fraction_numerical': 0.006695572097306423, 'mean_word_length': 4.168567178978681, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 0, 'https://': 1, 'lorem ipsum': 0, 'www.': 1, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
UC Modelling and Security Analysis of the Estonian IVXV Internet Voting System

Estonian Internet voting has been used in national-wide elections since 2005. However, the system was initially designed in a heuristic manner, with very few proven security guarantees. The Estonian Internet voting system has constantly been evolving throughout the years, with the latest version (code-named IVXV) implemented in 2018. Nevertheless, to date, no formal security analysis of the system has been given. In this work, for the first time, we provide a rigorous security modeling for the Estonian IVXV system as a ceremony, attempting to capture the effect of actual human behavior on election verifiability in the universal composability (UC) framework. Based on the voter behavior statistics collected from three actual election events in Estonia, we show that IVXV achieves end-to-end verifiability in practice despite the fact that only $4\%$ (on average) of the Estonian voters audit their ballots.


INTRODUCTION
In recent years, the advancement of remote electronic voting is gradually moving from an academic, mental exercise into practice. The first Internet voting events with legally binding results were conducted already in 2000 in Arizona [1] and the University of Osnabrück, Germany [2]. Only five years later, in 2005, the option of vote casting over the Internet was provided in the country-wide elections in Estonia for the first time in the world [3]. By 2014, the share of Internet votes in Estonia reached over 30% [4]. There have been various attempts to set up remote Internet voting in other countries, such as Switzerland [5] and Norway [6], but to date, Estonia remains the only country allowing access to Internet voting to all of its citizens.
While developing its Internet voting solution, Estonia has taken an engineering rather than theoretically well-founded approach. The initial protocol has been kept relatively simple, mimicking the conventional double-envelope postal voting and making use of the strong eID frameworks (ID-card and Mobile-ID) provided to the citizens. After its launch, the Estonian Internet voting system has been evolving towards better security guarantees. For instance, in 2011, a student presented a proof-of-concept vote manipulation malware making use of the fact that at that time, there was no vote verification mechanism implemented in the Estonian i-vote system [7]. By the next election event in 2013, the option of verifying the integrity of the votes stored on the server using a personal mobile device was introduced [8]. In contrast, the server-side of the Estonian Internet voting system was only protected using physical and organizational measures, not verifiable by the general public in an irrefutable manner. Several problems occurring as a result of such an architecture were pointed out by Springall et al. in 2014 [9]. To address these problems, the central system architecture was entirely redesigned by the 2017 parliamentary elections, introducing a mix-net procedure for vote privacy, provable decryption of votes, and independent vote commitments to ensure digital ballot box integrity [10]. The resulting system is code-named IVXV [11].
However, to date, there is no formal systematic security analysis of the IVXV system. In this work, we aim to put a foundation for abstract, model, and analyze the security of the IVXV system. In particular, we are interested in endto-end (E2E) verifiability, which has been widely accepted as a fundamental requirement for e-voting adoption. In an end-toend verifiable e-voting system, the voter can obtain a receipt after ballot casting, allowing him/her to verify that his/her vote was (i) cast as intended, (ii) recorded as cast, and (iii) tallied as recorded. Moreover, any external third-party auditor should also be able to verify that the election procedure was executed properly. Unfortunately, merely showing that a system is E2E verifiable does not imply the integrity of the election result in the real world. This is because the E2E verifiability usually relies on human participant behavior in a highly non-trivial manner. The ability of human voters to compromise overall security due to their negligence is well known in e-voting system design (cf. [12]). For instance, in terms of individual verifiability, to achieve the "cast-asintended" property, the voters are typically required/advised to perform specific auditing. This means that the voters, beyond the ballot-casting procedure, are supposed to carry out additional steps that many may find to be counterintuitive, see e.g., [13] for more discussion of this issue. This potentially leads to the defective execution of the appropriate steps that are to be carried out for verifiability to be supported; therefore, the verifiability of the election may collapse. In fact, according to the Estonian Internet voting statistics col-lected from the recent 5-year legally binding national-wide elections, only approximately 4% of voters perform the recommended ballot auditing process [14].
Is the Estonian IVXV system E2E verifiable w.r.t. the Estonian voter profile in practice? To answer this question, we study IVXV security as an e-voting ceremony. The notion, ceremony, was introduced by Ellison [15] to expand a security protocol with out-of-band channels, and the human users are considered as separate nodes of the system that should be taken into account when performing the security analysis. Later, the 'conditioned-safe ceremony' notion that encompasses forcing functions, defense-in-depth, and human tendencies was introduced in [16]. In 2015, Johansen and Jøsang [17] proposed a formal probabilistic model for verifying a security ceremony. In their work, the human agent interaction with the user interface is modeled as a nondeterministic process. In 2017, Kiayias et al. [18] analyzed the security of Helios in terms of an e-voting ceremony using property-based definitions. In this work, we, for the first time, model an e-voting ceremony in the universal composability (UC) framework [19], [20].
Our contributions. (i) For the first time, we provide a rigorous security modeling for an e-voting ceremony, attempting to capture human actions in the well-known UC (generalized UC, a.k.a. gUC) framework [19], [20]. To model verifiability, we introduce a conceptual entry, auditor AU, which cannot be corrupted. 1 The adversary is allowed to tamper with O(log λ) ballots without raising an alert, i.e., the difference between the announced tally and the true tally is logarithmically bounded w.r.t. the security parameter λ. 2 When ω(λ) ballots are tampered with, the AU will return invalid and void the entire election. In the spirit of e-voting ceremony, we distinguish the (human) voters from their voter supporting devices (VSDs), such as PC, smartphone, tablet, etc. This separation enables more refined security analysis, e.g., covering the case when a voter is honest but his/her VSD is compromised. The VSD of voter V i is modeled as an ideal functionality F Vi VSD . F Vi VSD is parameterized with a PPT Turing machine M HONEST , which is used to model the software that is running on the VSD. The functionality of M HONEST is encrypting and signing the voter's ballots. The adversary is able to compromise the F Vi VSD by sending an arbitrary M to it, and F Vi VSD will use the modified M for all its operations. Note that if the F Vi VSD is compromised, the choice of voter V i is leaked to the adversary. In addition, auditing supporting devices (ASDs) are introduced to allow the voters to have a trustworthy device to perform certain ballot auditing operations. Although each voter may have its own ASD, the corresponding operation is universal. Hence we use a single functionality F ASD to model all the ASDs in our model.
We assume that the voters as human beings are not 1. In the real world, there are in general several auditors who study the evidence presented to them independently. It is assumed that all of them should come to a coordinated decision concerning the correctness and consistency of this evidence. However, this process remains outside of the cryptographic realm, and hence we model AU as one entity here.
2. Since the number of voters n = poly(λ), such a difference can also be viewed as O(log n). This is used to model a small tally deviation that is not sufficient to swing the election results in practice. For an election with several billion voters, the deviation could remain as low as hundreds.
capable of performing complicated cryptographic operations or generating high entropy randomness. (In fact, in this work, the voters are modeled as finite state machines, but they are only required to perform string forwarding and matching tasks.) As each voter may have a different behavioral pattern in practice, we introduce a special voter emulator functionality F D V.EMU that is parameterized by a voter profile distribution D and sample a voter behavior pattern according to D as a script. The voter then runs the script during the election.
(ii) For the first time, we formally abstract the latest Estonian IVXV system as described in [11], [21] in terms of a UC protocol. More specifically, we introduce several ideal functionaries, i.e., G BB ,Ĝ CERT , {F Vi VSD } i∈[n] , F ASD , F KEYGEN , F DEC and F D V.EMU , to abstract the implementation details away from the main protocol description. We then discuss how each ideal functionality is instantiated in practice and list the implied assumptions in Sec. 5. For instance, the multisession certificate functionalityĜ CERT is introduced to abstract the Estonian PKI infrastructure. It provides a direct binding between a signature and the identity of the corresponding signer. Note that the bulletin board (BB) functionality G BB is slightly different from the conventional BB functionality required by an end-to-end verifiable voting system. Normally, a BB is publicly accessible in the sense that anyone can read the messages posted on the BB. The G BB used in the Estonian IVXV system consists of public BB and private BB, where the public BB is the same as conventional BB, but the private BB can only be accessed by the auditor(s) and ASDs. This setup can enable verifiability while still achieving a certain level of coercion resistance by preventing the adversary from seeing certain BB content 3 .
(iii) We build a real-world Estonian voter behavior profile based on the actual statistics of the voting and verification patterns observed during three recent election events in the past five years. This allows us to analyze the security of the Estonian IVXV system under the proposed UC framework w.r.t. the real Estonian voter behavior distribution. We show that the Estonian IVXV protocol UC-realizes the ideal verifiable voting functionality F n,k,t,δ VOTE , where n is the number of voters, k is the number of trustees, and t − 1 is the maximum number of corrupted trustees that the protocol can tolerate. We also study the optimal strategy for the adversary to tamper with the votes and estimate the probability of success for this strategy. For example, when the adversary tries to change 100 or 200 random votes, his probability of success is 1.687% or 0.028%, respectively.
Roadmap. In Sec. 2 we formally present notations that will be used throughout the paper. In Sec. 3 we describe the ceremony Estonian voting system under the UC framework which contains the ideal functionalities. In Sec. 4 we de- 3. In particular, the sensitive information includes the time-stamps of encrypted and signed votes. The Estonian system provides the voters with the option of re-voting in case they were forced to cast a vote against their true will. However, the efficiency of this measure relies on the coercer not being able to understand which one of the votes submitted by the voter was the latest. If the attacker is sufficiently powerful to obtain the timing information, he can request the voter to reveal her verification token and complete the coercive attack (as described e.g., in the OSCE/ODIHR report [22]). scribe the ceremony Estonian voting protocol leveraging the proposed ideal functionalities along with security analysis. Further, in Sec. 5, we discuss these ideal functionalities are instantiated in the real-world Estonian IVXV system. Finally, in Sec. 6 and Sec. 7, we discuss the related works and give a conclusion, respectively.

Threshold secret sharing
The Estonian IVXV voting system adopts Shamir secret sharing [23] for the private key distribution during the election key generation phase. In a (t, k)-threshold secret sharing scheme, the secret x is shared by a dealing algorithm (s 1 , . . . , s k ) ← Deal(x). Any group of t or more shares together can open the secret via the reconstruction algorithm x ← Reconstruct(K) for |K| ≥ t and K ⊆ {s 1 , . . . , s k }.

Re-randomizable public key encryption
A public key encryption scheme consists of a tuple of PPT algorithms PKE := (Setup, KeyGen, Enc, Dec, Rand).
• params ← Setup(1 λ ): it takes as input the security parameter λ, and outputs a public parameter params. • (PK, SK) ← KeyGen(params): it takes as input the public parameter params, and outputs a pair of public key and private key (PK, SK). • ct ← Enc(PK, m; r): it takes as input the public key PK, the message m, and the randomness r, and it outputs the ciphertext ct. • m ← Dec(SK, ct): it takes as input the private key SK and ciphertext ct, and outputs the message m. • ct ← Rand(PK, ct; r): it takes as input the public key PK, a ciphertext ct and the randomness r, and outputs a re-randomized ciphertext ct . We assume the public key encryption scheme is IND-CPA secure. In addition, given the randomness used during encryption, we want the ciphertext to be extractable such that there exists an algorithm m ← TDec(PK, ct, r), where ct = Enc(PK, m; r).

Non-interactive Zero-Knowledge Proofs
Let R be an efficiently computable binary relation. For pairs (x, w) ∈ R, we call x the statement and w the witness. Let L R be the language consisting of statements in R, i.e. L R = {x|∃w s.t. (x, w) ∈ R}. An non-interactive zero-knowledge (NIZK) proof consists of PPT algorithms (Prov, Ver, Sim, Ext), where Prov is the prover algorithm, Ver is the verification algorithm, Sim is the simulator, and Ext is the knowledge extractor. The IVXV system adopts the Verificatum mix-net, which utilises the NIZK proposed in [24] for verifiable shuffle.

Universally Composability (UC)
Following Canetti's framework [19], a protocol is represented as a set of interactive Turing machines (ITMs), each of which represents the program to be run by a participant. Let Exec Π,A,Z denote the output of the environment Z when interacting with parties running the protocol Π and realworld adversary A. Let Exec F ,S,Z denote output of Z when running protocol φ interacting with the ideal functionality F and the ideal adversary S. Definition 2.1. We say that a protocol Π UC-realizes F if for any PPT adversary A there exists an PPT adversary S such that for any environment Z that obeys the rules of interaction for UC security we have Exec Π,A,Z ≈ Exec F ,S,Z .

SECURITY MODEL
Let n, k ∈ N be poly(λ). The entities involved in IVXV are a set of voters V := {V 1 , · · · , V n }, a set of trustees T := {T 1 , · · · , T k }, the election authority EA, and the auditor AU. We consider the security of IVXV in the UC framework with static corruption. The security is based on the indistinguishability between real/hybrid world executions and ideal world executions, i.e., for any possible PPT real/hybrid world adversary A we will construct an ideal world PPT simulator S that can present an indistinguishable view to the environment Z operating the protocol. The idea world execution. In the ideal world, the election authority EA, the voters V, the trustee T and the auditor AU only communicate to an ideal functionality F n,k,t,δ VOTE during the execution, where δ ∈ N is an adjustable threshold. The ideal functionality F n,k,t,δ VOTE accepts a number of commands from EA, V, T , and AU. At the same time, it informs the adversary S of certain actions that take place and also is influenced by S to elicit certain actions. As depicted in Fig. 1, the ideal functionality F n,k,t,δ VOTE consists of four phases which are preparation, voting, tally, and audit. In the preparation phase, the trustees T := {T 1 , . . . , T k } send (START, sid) to F n,k,t,δ VOTE to indicate their presence. This is used to model their key generation participation in practice. To start an election, the EA sends the command (BEGIN, sid) to F n,k,t,δ VOTE . Note that the election will not start until all the trustees have participated in the preparation.
In the voting phase, the voter V i sends (VOTE, sid, x i ) to F n,k,t,δ VOTE . However, this action may be blocked or tampered with by the adversary A; in both cases, a flag Alert[i] is set to 1. It maintains 2 arrays -Record, Ballots. Record is only used for temporary storage to enable adversarial modification, and the final effective ballots are stored in Ballots. When the ballot is received from V i , it is temporarily saved in Record[i]; the functionality then asks the adversary S if she wants to proceed, modify, or block it. If S does not reply to the functionality, then the ballot is blocked, and it will not be copied to Ballots[i] and not counted. Note Alert[i] is initially set to 1, and it is only set to 0 when Ballots[i] := Record[i], i.e., the ballots are proceeded without tampering. If more than t trustees T j ∈ T are corrupted, i.e., |T ∩ P cor | ≥ t, F n,k,t,δ VOTE directly leaks the voter's choice x i to A. This is used to model the fact that the corrupted trustees can reconstruct the secret key and decrypt all the submitted ballots in practice. Alternatively, A can send a CORRUPT command to F n,k,t,δ VOTE to learn the voter's choice x i . This is used to model the fact that if the voter V i 's VSD is compromised, then his choice may be leaked. Note that this functionality allows the voters to re-vote an arbitrary number of times before the end of the It is parameterized with variables status, Record, Ballots, τ , J1 and J2. Let Pcor be the set of corrupted parties. Initially, set status = 0, Alert := (0, . . . , 0), Record := Ballots := τ := J1 := J2 := ∅.
-If EA ∈ Pcor, sort entries in Ballots lexicographically to Ballots * and send message (LEAK, sid, Ballots * ) to the adversary S.
• Upon receiving input (Result, sid) from any party p, if τ = ∅ ignore the input. Otherwise, return public delayed output (Result, sid, τ ) to the requestor. Audit: • Upon receiving input (AUDIT, sid) from AU, if status < 2 ignore the request; otherwise, it sends notification (AUDIT, sid) to S and then returns (AUDIT, sid, valid) to AU if HW(Alert) ≤ δ; else, it returns (AUDIT, sid, invalid) to AU, where HW is the hamming weight function.
Functionality F n,k,t,δ VOTE Figure 1: Functionality F n,k,t,δ VOTE election. The EA can end the election by sending (END, sid) command to F n,k,t,δ VOTE . In the tally phase, the trustee T j ∈ T can participate the tally by sending (Tally, sid) to F n,k,t,δ VOTE . When at least t trustees agree to tally, F n,k,t,δ VOTE computes the election result τ ← TallyAlg(Ballots) by invoking the tally algorithm TallyAlg(·) 4 . If the EA is corrupted, F n,k,t,δ VOTE leaks all the ballots Ballots to S, i.e., no voter privacy when the EA is corrupted. When the EA is honest, the adversary only learns lexicographically sorted ballots Ballots * , which is used to model the privacy level provided by the mix-net. When τ is computed, any party can query the election result by sending (Result, sid) to F n,k,t,δ VOTE . In the audit phase, the AU can send the command (AUDIT, sid) to F n,k,t,δ VOTE for auditing. HW(·) denotes the hemming weight function, and HW(Alert) = δ stands for at most δ ballots can be tampered or blocked without detection. Otherwise, F n,k,t,δ VOTE returns (AUDIT, sid, invalid) to the AU. This modeling ensures that the difference between the announced tally and the true tally is bounded by small δ w.r.t. the total number of votes. This is used to model a small tally deviation that is not sufficient to swing the election results in practice. For an election with several billion voters, the deviation could remain as low as hundreds. Remark. The above security model implies the following e-voting privacy and verifiability properties. Note that the 4. The tally algorithm TallyAlg varies among different elections and countries.
receipt-freeness property is not modeled above for readability. We refer interested readers to [25] for a UC model for receipt-freeness. Regarding privacy, in general, the protocol achieves the standard mix-net type of voter anonymity, where a voter's ballot is hidden among all the other cast ballots. When the EA is compromised, or more than t−1 trustees are compromised, voter privacy is no longer guaranteed. Otherwise, if the VSD of a voter is compromised, then this voter's ballot is leaked to the adversary. In terms of verifiability, assuming the ASD and AU cannot be compromised, the protocol achieves end-to-end verifiability against malicious EA as well as VSD's in the sense that the announced tally can only deviate O(log λ) votes from the true tally.
The real world execution. The real/hybrid world IVXV protocol Π vote utilizes a number of supporting components. Those supporting components are modeled as ideal functionalities, and later we will discuss how they are realized in practice in Sec. 5. Similar as the most End-to-End verifiable voting schemes, the IVXV protocol requires a bulletin board functionality G BB . We distinguish the voters (human) from their voting and auditing devices. Let (F V1 VSD , . . . , F Vn VSD ) and F ASD denote the voter supporting device functionalities associated with the voter V i , i ∈ [n] and audit supporting device functionality, respectively. In addition, we also abstract the threshold key generation and decryption process as F KEYGEN and F DEC . (Note that we intentionally use F KEYGEN and F DEC instead of a threshold public-key encryption functionality. This is mainly because, in Estonian e-voting, the threshold It interacts with the VSD functionalities (F V 1 VSD , . . . , F Vn VSD ), the ASD functionality F ASD , the election authority EA, the auditor AU, and the adversary A.
, verify that ssid = (V i , ssid ) for some ssid . If not, ignore the request. Otherwise, send (SIGNNOTIFY, sid, ssid, m) to the adversary A. Upon receiving (SIGNATURE, sid, ssid, m, σ) from A, verify that no entry (ssid, m, σ, 0) is recorded. If it is, then -Else, if the signer of subsession ssid is not corrupted, and no entry (ssid, m, ·, 1) is recorded, then set b = 0 and record the entry (ssid, m, σ, 0).

Figure 2:
The multi-session functionality for certificate.
The functionality interacts with the election authority EA, auditor AU, the functionalities F VSD , F ASD , F DEC , the adversary A and the set of all the other parties P. It is parameterized with variables Pub and Priv. Initially, set Pub = ∅ and Priv = ∅.
• Upon receiving (PUBPOST, sid, m) from the EA or F DEC , set Pub := Pub ∪ {m} and send notification (PUBPOST, sid, m) to the adversary A. • Upon receiving (PRIVPOST, sid, m) from the EA, then set Priv := Priv ∪ {m}. • Upon receiving (READ, sid) from a party p ∈ P ∪ {EA, F VSD , F DEC } or A, then return (READ, sid, Pub) to the requestor. • Upon receiving (READ, sid) from the AU or F ASD or F DEC , then return (READ, sid, (Pub, Priv)) to the requestor.
Functionality G BB Figure 3: Functionality G BB key generation and decryption processes are performed as ceremonies that involve human participates with different assumptions. Our modeling approach is similar to [26].) We use the certificate functionalityĜ CERT to model the Estonian PKI infrastructure. Finally, we introduce the voter emulator functionality F D V.EMU to capture the voter behavior in an evoting ceremony.
Certificate functionality. We adopt a multi-session version of the certificate functionality as modeled in [27]. The multisession certificate functionalityĜ CERT can provide a direct binding between a signature of a message and the identity of the corresponding signer. This corresponds to providing signatures accompanied by "certificates" that bind the verification process to the signers' identities. For completeness, we recapĜ CERT in Fig. 2 and refer interested readers to [27].
VSD interacts with the voter Vi ∈ V, the EA, and the adversary A. It is parameterized with a PPT Turing machine M HONEST and an internal state st. Initially, set st := ∅.
• Upon receiving (SIGNENC, sid, x) from the voter Vi, send notification (SIGNENC, sid, Vi) to the adversary A. Upon receiving (CORRUPT, sid) from  Figure 4: Fig. 3 and consists of private BB (i.e., Priv) and public BB (i.e., Pub). In practice, the functionality of the Pub can be efficiently realized from a conventional BB functionality using encryption and signature schemes. The introduction of Priv allows IVXV to enable verifiability while still achieving coercion resistance. Namely, only the honest party can access Priv. In this work, we only allow the EA to post a message on the G BB . Meanwhile, any party can read the messages posted on Pub of G BB , while only AU and F ASD can access Priv.
Voter emulator functionality. The voter emulator functionality F D V.EMU samples voter behavior according to a distribution D. Table 1 depicts the voter behaviour statistics collected from recent Estonian national-wide elections. The voter has two types of actions, (i) 'V', which stands for voting, and (ii) 'C', which stands for checking. For instance, in the RK2015 election, 93.8592% voters have action pattern 'V', which means that those voters voted their ballots without checking; whereas 3.8563% voters have action pattern 'VC', which means that those voters voted their ballots and checked; similarly, 'VVC' means that the voters voted once without checking, and he then voted the second time and checked the ballot.
Notably, as a coercion prevention measure, the voter is allowed to re-vote as many times as he wants. After every vote casting, he can check the last vote 0 or more times. For the sake of probabilistic analysis, the string of script script i is be expressed as the regular expression V (V |C) * . 5 VSD functionality. Each voter has its own unique VSD, as the Estonian national ID cards are modeled as a part of the VSD. The voter V i 's VSD is modeled as the functionality F Vi VSD , as depicted in Fig. 4. F Vi VSD is parameterized with a PPT Turning machine M HONEST , which is used to model the software running on the VSD. The functionality of M HONEST is encrypting and signing the ballots, and the details are provided later. Note that F Vi VSD can be corrupted. When it is corrupted, the voter's choice is leaked to the adversary A. Moreover, the adversary A is able to replace M HONEST with any arbitrary Turning machine M, and F Vi VSD will use M for the execution. The state st is introduced to model stateful 5. In practice, the maximal number of verifications per vote is limited to 3, but we ignore this limitation here for notation simplicity.  algorithms. After execution, F Vi VSD sends the voter V i the receipt by the command (RECEIPT, sid, z) and sends EA the ballot using the command (BALLOT, sid, y).

Modelling Voters (human).
We assume that the voters as human beings are not capable of performing complicated cryptographic operations or generating high entropy randomness. In fact, in IVXV, the voters are only required to perform string forwarding and matching. We model the voter (human) as a finite state machine (FSM), VOTE(script i , sid, x) by taking as input the script script i , session id sid, and the choice x of the voter, where the script i is an output of F D V.EMU (see Fig. 5.) The machine FSM then starts executing script i character by character, and the logic of implementing the voting and verification via the script script i is depicted in Fig. 6. The action commands corresponding to the characters are interpreted as follows. M HONEST description. As depicted in Fig. 7, the Turing machine M HONEST processes the F Vi VSD requirements from the voter V i as follows. The Turing machine M HONEST first fetch the public key PK from G BB . It samples a random r ← Z q , then encrypts and outputs c ← Enc(PK, x; r) for the voter choice x. Once obtains the ciphertext c, the Turing machine M HONEST sends the message (SIGN, sid, ssid, c) to functionalityĜ CERT and receives the feedback (SIGNATURE, sid, ssid, c, σ) fromĜ CERT . Lastly, the Turing machine M HONEST will output the triple (y, z, ∅), where y is the ciphertext and signature triple (ssid, c, σ), the receipt z is the ciphertext and random triple (ssid, c, r). The initial ∅ implies M HONEST is stateless.

Remark.
Although it is controversial whether it is a good idea to let an ideal functionality directly interact with another ideal functionality in the UC framework, technically, such type of modeling is not wrong and can be found in many UC modeling papers, e.g. [28], [29].
ASD functionality. Although each voter may have its own ASD, the corresponding operation is universal. Hence we use a single functionality F ASD to model all the ASDs. F ASD is always trusted in our setting. As depicted in Fig. 8, the voter V i ∈ V can send the command (AUDIT, sid, z) to F ASD for audit, and F ASD parses the receipt z as (ssid, c, r) The functionality interacts with a set of voters V := {V1, . . . , Vn}, the functionality G BB , and the adversary A. It is parameterized with an algorithm TDec (cf. Sec. 2).
send trustee Tj message (PRIVKEY, sid, SKj). • Upon receiving (PUBKEY, sid) from the EA, if PK is not defined yet, ignore the request. Otherwise, it sends (PUBKEY, sid, PK) to the EA.
Functionality F KEYGEN Figure 9: Functionality F KEYGEN and then verify that ssid = (V i , ssid ) for some ssid . Subsequently, the functionality F ASD fetches the corresponding record from G BB , and verify the signature by sending (Verify, sid, ssid, m, σ) toĜ CERT . Upon success, F ASD computes m ← TDec(PK, c, r) and returns (AUDITED, sid, m) to V i .
Threshold key generation functionality. F KEYGEN is aimed to provide the public key PK for voters and provide the share of secret key SK j (j ∈ [k]) via secret sharing for trustees, as depicted in Fig. 9. The trustee T j ∈ T can send the command (READY, sid) to F KEYGEN for key generation. Once all the k trustees have participated the key generation, F KEYGEN generates (PK, SK) ← KeyGen(1 λ ) and computes (SK 1 , . . . , SK k ) ← Deal(SK). Lastly, F KEYGEN returns trustee T j message (PRIVKEY, sid, SK j ) for j ∈ [k]. Furthermore, the EA can send the command (PUBKEY, sid) to the F KEYGEN for the public key PK.
Audible threshold decryption functionality. F DEC is used to model the audible threshold decryption process, as depicted in Fig. 10. The trustee T j ∈ T can send the command (KEY, sid, SK j ) to F DEC to participate the decryption. When more than t trustees participate the description, F DEC recon- The functionality interacts with trustees {T1, . . . , T k }, the EA, , the auditor AU, and the adversary A. It is parameterised with variable K, b, the decryption algorithm Dec() and the share reconstruction Reconstruct(). Initially, set K := ∅ and b = ⊥.

THE ESTONIAN IVXV I-VOTING SCHEME
On the conceptual level, the Estonian IVXV Internet voting is still mimicking double envelope postal voting as it was in 2005. The inner privacy ensuring envelope is replaced by encryption with the central system's public key, whereas the outer authentication and integrity providing envelope are replaced by the voter's digital signature [10], [14]. However, two major scheme updates have occurred since 2005. First, in 2013, it became possible to individually verify vote integrity in the digital ballot box using an independent mobile device [8]. Secondly, in 2017, server-side transparency was greatly improved by adding several independently auditable features like provable vote decryption and commitments of digital ballot box actions [10]. In the following Sec. 4.1, we will provide the UC description to the Estonian e-voting w.r.t. the documentation [11]. In Sec. 5, we show how those ideal functionalities are realized in practice.

UC Description for Estonian IVXV Voting scheme
The Estonian IVXV scheme Π vote is depicted in Fig. 11. It consists of four phases: preparation, voting, tally, and audit. The entities involved in the Π vote protocol are the election authority EA, the voters V, the trustees T , and the auditor AU. Meanwhile, the protocol also uses a number of supporting components modelled as ideal functionalities, i.e. G BB ,Ĝ CERT , {F Vi VSD } i∈[n] , F ASD , F KEYGEN , F DEC , F D V.EMU , where D is the Estonian voter behaviour statistics as depicted in Table 1.

Preparation:
• Upon receiving (START, sid) from the environment Z, the trustee Tj ∈ T sends message (READY, sid) to functionality F KEYGEN . • Upon receiving (BEGIN, sid) from the environment Z, the EA creates an empty array B := ∅. The EA then sends (PUBKEY, sid) to functionality F KEYGEN , and it receives (PUBKEY, sid, PK) from F KEYGEN . It then sends (PUBPOST, sid, PK) to G BB . Voting: • Upon receiving (VOTE, sid, x) from the environment Z, the voter Vi ∈ V sends message (EMULATE, sid) to functionality F D V.EMU and obtains (EMULATE, sid, script i ) from F D V.EMU . Execute VOTE(script i , sid, x) as described in Sec. 3, Fig. 6 to interact with F V i VSD and F ASD . • Upon receiving (BALLOT, sid, y) from the functionality F V i VSD , the EA parses y as (ssid, c, σ) where ssid = (Vi, ssid ) for some i ∈ [n]. It then sends (Verify, sid, ssid, c, σ) to functionalityĜ CERT  After that, it then sends (PRIVPOST, sid, ((c 1 , . . . , c n ), π)) to G BB . Tally: • Upon receiving (Tally, sid) from the environment Z, the trustee Tj ∈ T sends message (KEY, sid) to functionality F DEC . • Upon receiving (Result, sid) from the environment Z, any party p sends (READ, sid) to functionality G BB , and obtains (READ, sid, Pub) from G BB . p then fetches (m1, . . . , mn) from Pub. It then computes τ ← TallyAlg(m1, . . . , mn) and returns (Result, sid, τ ) to Z. Audit: • Upon receiving (AUDIT, sid) from the environment Z, the auditor AU sends (READ, sid) to functionality G BB , and obtains (READ, sid, (Pub, Priv)) from G BB . It fetches PK from Pub, and verifies: -For all the (ssid , c , σ ) in Priv, send (VERIFY, sid, ssid , c , σ ) to functionalityĜ CERT  In the preparation phase, the trustee T j ∈ T for initializing the e-voting scheme by sending the command (READY, sid) to functionality F KEYGEN for key generation. Upon receiving (BEGIN, sid), the EA fetches the generated public key PK from F KEYGEN , and then it posts PK to the G BB . Meanwhile, the EA creates B, and B[i] will be used to record the last received ballot of voter V i ∈ V, i ∈ [n].
In the voting phase, the voter V i ∈ V first queries F D V.EMU to obtains a script script i . It runs VOTE(script i , sid, x) as described in Sec. 3, Fig. 6 to interact with F Vi VSD and F ASD . Note that if the verification/checking fails w.r.t. the output of F ASD , the voter V i sends a Complain message to AU. The F Vi VSD encrypts and signs the ballot, it then sends the ballot to the EA via (BALLOT, sid, y), where y = (ssid, c, σ). The EA first checks the validity of the signature, by verifying that ssid = (V i , ssid ) and sending (Verify, sid, ssid, c, σ) to functionalityĜ CERT . The EA then posts the ballots on the G BB .
Upon receiving (END, sid), the EA picks a random permutation Π ← S n ; for i ∈ [n], it picks a random r i ← Z p and set the shuffled ciphertext c i := Rand(PK, c Π(i) ; r i ). The EA then generates the corresponding NIZK proof After that, it then posts (c 1 , . . . , c n ), π) to the G BB .
In the tally phase, the trustee T j ∈ T sends message (KEY, sid) to functionality F DEC to decrypt the ballots. When more than t trustee participated the decryption, F DEC decrypts the ballots and post the decrypted shuffled ballots (m 1 , . . . , m n ) on the G BB . After that, anyone can fetch (m 1 , . . . , m n ) from G BB and then computes the election result τ ← TallyAlg(m 1 , . . . , m n ).
In the audit phase, the auditor AU fetches all the election transcripts from the G BB and it returns valid if and only if: • All the (ssid , c , σ ) in Priv have valid signatures. • For i ∈ [n], define the last ballot c * for some * sent by voter V i as c i . • Check NIZK. Ver((c 1 , . . . , c n ), (c 1 , . . . , c n ), PK, π) = 1.
• No Complain message received from any voter V i ∈ V.

Security Analysis
We first give an intuition why the IVXV protocol is secure. Let's examine the optimal attacker strategy for IVXV. Note that the adversary also knows the voter behavior distribution as shown in Table 1, where the voter with a probability around 94% just submits one vote and never does anything else. Apparently, just manipulating the first vote gives the attacker a success probability of about 94%. But the adversary knows around 1.5% of voters who choose to vote twice and stop then according to Table 1. Thus, she has a better success probability if, in addition to the above, when she sees a revote and also manipulates that, her probability of success rises to about 95.5%. In a nutshell, for all the voter strategies of type V . . . V , the probability of the pattern V . . . V is larger than the probability of V . . . V C (with the same number of V -s). This means that in order to maximize the overall success probability, it is always rational for the adversary to manipulate the latest ballot in the sequence V . . . V . Note that by assuming this strategy, the attacker does not need to prepare a decision for any sequence where there are some Cs, since she will get caught at the corresponding verifications anyway. Thus, the overall success probability of the optimal attacker strategy is the sum of probabilities of patterns V , V V , V V V , etc. Adding them for the three different events, we see that the overall probability of these is around 96%.
From here, we can compute the attacker's success probability if she tries to implement a large-scale vote manipulation attack. E.g., the attacker wants to change k votes and remain undetected. Since the probability of not getting caught when manipulating any single vote is 0.96, the probability of remaining undetected changing k votes is 0.96 k . Consequently, the probability of being detected at least once is 1 − 0.96 k . For example, when the adversary tries to change 100 or 200 random votes, her probability of success is 1.687% or 0.028%, respectively. Theorem 4.1. Let n, k, t be in poly(λ). For any δ = O(log λ), the IVXV e-voting protocol Π vote described in Fig. 11 UC-realizes the F n,k,t,δ VOTE functionality as depicted in Fig. 1 EMU -hybrid world against static corruption if PKE is IND-CPA secure, NIZK is computationally sound and composable zero-knowledge, and there is a constant fraction 0 < c ≤ 1 of the voters who check their latest submitted ballots w.r.t. the voter behaviour distribution D (i.e. the voter behaviour pattern ends with 'C').
Proof. To prove the theorem, we first construct a simulator S such that no non-uniform PPT environment Z can distinguish with non-negligible probability between (i) the real execution Exec where the parties interact with functionality F n,k,t,δ VOTE in the G BB ,Ĝ CERT -hybrid model and corrupted parties are controlled by the simulator S. Let V cor ⊆ V and T cor ⊆ T be the set of corrupted voters and trustees, respectively.
Simulator. The simulator S internally runs A, forwarding messages to/from the environment Z. The simulator S simulates honest voters V i ∈ V \ V cor , honest trustees T j ∈ T \ T cor and functionalities {F Vi VSD } i∈[n] , F ASD , F KEYGEN , F DEC , and F D V.EMU . In addition, the S simulates the following interactions with A.
• In the preparation phase: -Upon receiving (START, sid, T j ) from the external F n,k,t,δ VOTE for an honest trustee T j ∈ T \ T cor , the simulator S acts as T j , sending message (READY, sid) to functionality F KEYGEN .
-When the simulated functionality F KEYGEN receives (READY, sid) from a corrupted trustee T j ∈ T cor , the simulator S acts as T j to send (START, sid) to the external F n,k,t,δ VOTE . -If EA is corrupted, S keeps monitoring G BB ; when PK is posted on the G BB , it acts as EA, sending (BEGIN, sid) to F n,k,t,δ VOTE . -If EA is honest, upon receiving (BEGIN, sid) from F n,k,t,δ VOTE , S acts as EA, sending (PUBKEY, sid) to the functionality F KEYGEN . When the simulated EA receives (PUBKEY, sid, PK) from F KEYGEN , S acts as EA, sending (PUBKEY, sid, PK) to G BB .
• In the voting phase: -Upon receiving (VOTE, sid, V i ) from the external F n,k,t,δ VOTE for an honest voter V i ∈ V \V cor , the simulator S acts as V i , following the protocol Π vote description as if V i receives (VOTE, sid, ⊥) from Z.
-The simulator S monitoring G BB , once a record (ssid, c, σ) is posted on the G BB , where ssid = (V i , ssid ) for some corrupted voter V i ∈ V cor , it fetches SK from the internal state of the simulated F KEYGEN and compute x ← Dec(SK, c). S then acts as V i to send (VOTE, sid, x) to F n,k,t,δ VOTE . -When the simulated F Vi VSD receives (CORRUPT, sid) from A, the simulator S sends (CORRUPT, sid, V i ) to the external F n,k,t,δ VOTE . Once S receives (LEAK, sid, It parses y as (ssid, c, σ) and extracts x * ← Dec(SK, c). S sends (PROCEED, sid, V i , x * ) to F n,k,t,δ VOTE . -If EA is honest, upon receiving (END, sid) from F n,k,t,δ VOTE , the simulator S acts as EA, following the protocol Π vote description as if EA receives (END, sid) from Z.
• In the tally phase: -Upon receiving (Tally, sid, T j ) from the external F n,k,t,δ VOTE for an honest trustee T j ∈ T \ T cor , the simulator S acts as T j , sending message (KEY, sid) to functionality F DEC .
-When the simulated functionality F DEC receives (KEY, sid) from a corrupted trustee T j ∈ T cor , the simulator S acts as T j to send (Tally, sid) to the external F n,k,t,δ VOTE . -If EA is honest: upon receiving (LEAK, sid, Ballots * ) from F n,k,t,δ VOTE , the simulator S interprets Ballots * as (m 1 , . . . , m n ) and acts as F DEC to send the command (PUBPOST, sid, (m 1 , . . . , m n )) to G BB .
• In the audit phase: -Upon receiving (AUDIT, sid) from the external F n,k,t,δ VOTE , the simulator S acts as AU, following the protocol Π vote description as if AU receives (AUDIT, sid) from Z.   . We will estimate the success probability of the adversary who is trying to manipulate the vote on the voter's device without getting caught. Assume 0 < c ≤ 1 fraction of the voters check their latest submitted ballots, the probability of not getting caught when manipulating any single vote is 1 − c. Therefore, to tamper ω(log λ) votes, the probability of being detected at least once is Therefore, with probability p, the adversary's view of H 2 is identical to the simulated view of the ideal execution Exec GBB,ĜCERT F n,k,t,δ VOTE ,S,Z . Therefore, no PPT Z can distinguish the view of the ideal execution from the view of the real execution with more than negligible probability.
Simulator. Similar as Case 1, the S internally runs A, forwarding messages to/from the environment Z. The S simulates honest voters V i ∈ V \ V cor , honest trustees T j ∈ T \ T cor and functionalities {F Vi VSD } i∈[n] , F ASD , F KEYGEN , F DEC , and F D V.EMU . In addition, the S simulates the following interactions with A.
• In the preparation phase: -The same as Case 1.
• In the voting phase: -The same as Case 1.
-When the simulated F Vi VSD receives (CORRUPT, sid) from A, the simulator S sends (CORRUPT, sid, V i ) to the external F n,k,t,δ VOTE . Once S receives (LEAK, sid, V i , x i ) from F n,k,t,δ VOTE , it acts as F Vi VSD to send (LEAK, sid, V i , x i ) to A. When the simulated F Vi VSD receives the message (TAMPER, sid, M) from A: if M = ∅, the simulator S sends (PROCEED, sid, V i , x i ) to F n,k,t,δ VOTE ; otherwise, S computes (y, z, st ) ← M(V i , st, x i ). It parses y as (ssid, c, σ) and extracts x * ← Dec(SK, c). S sends (PROCEED, sid, V i , x * ) to F n,k,t,δ VOTE . -If EA is honest, upon receiving (END, sid) from F n,k,t,δ VOTE , the simulator S acts as EA, following the protocol Π vote description as if EA receives (END, sid) from Z.
• In the tally phase: -The same as Case 1.
• In the audit phase: -The same as Case 1. Indistinguishability. The indistinguishability in this case is straightforward, as S never simulate a single message to either any corrupted parties or the external G BB . The simulator S knows all the honest voters' ballot from F n,k,t,δ VOTE when |T cor | ≥ t. Meanwhile, it also extracts the ballot of the malicious voters by using SK leaked from F KEYGEN . Hence, the simulator S can submit the extracted ballot to the external F n,k,t,δ VOTE on the malicious voters' behave. Moreover, the EA cannot tamper any ballots without being detected due to the unforgeability of the underlying signature scheme modeled byĜ CERT . Therefore, the view of Z in the ideal execution has identical distribution to the view of Z in the real execution.

REAL-WORLD INSTANTIATION
In this section, we examine how those ideal functionalities and system entities are instantiated in the real-world Estonian IVXV voting system as described in the official documentation [11]. Before that, we first provide a brief description. The Estonian i-voting process is depicted in Fig. 12, and it consists of three stages.
Pre-voting stage. Before the election, the lists of candidates and eligible voters are prepared. Also, the client software for i-voting is compiled and distributed via the main i-voting website (https://www.valimised.ee/en). This software will IVXV uses Elgamal encryption as the underlying rerandomizable public-key encryption scheme, and the election key is generated and distributed through an offline ceremony. k (human) trustees are selected from the members of national electoral committee and state electoral office. During the ceremony, the trustees are gathered on-site and witness the hardware security module (HSM) generating a public and secret key pair (PK, SK), and splitting the secret key SK into k shares using (t, k) Shamir secret sharing as (SK 1 , . . . , SK 9 ) ← Deal(SK). The shares are then stored on k smartcards, one for each trustee. SK is then deleted from the HSM. The values k = 9, t = 5 are used in recent Estonian i-voting practice.
Voting stage. The voters are authenticated by their physical eID tokens (ID chip card or Mobile-ID SIM card) combined with a knowledge-based PIN. During the voting stage, the voter first downloads the list of candidates specifies his/her choice in the i-voting software on his/her client; the client then encrypts the vote with a fresh random coin r and signs the ciphertext. It then sends the signed ciphertext to the collector. After checking the validity of the signature, the collector sends the ciphertext to the registration service who will record it and sign it together with a time stamp. The collector then generates a unique ballot ID and sends it back to the voter's client. After that, it stores the doubly-signed ciphertext (indexed by the ballot ID) in the i-ballot box. In the end, the client outputs a QR code that contains the random coin r and the ballot ID.
If the voter would like to audit the ballot, he/she can use a smartphone (with the verification app) and scan the QR code obtaining the random coin r and ballot ID 6 . As shown in Fig. 13, during the verification, the smartphone queries the collector and i-ballot box with the ballot ID, obtaining the doubly-signed ciphertext. The smartphone first checks the validity of the registration service's signature and the voter's signature. Let the ElGamal ciphertext be c := (c 1 , c 2 ) and PK := (g, h). It then computes m := TDec(PK, c, r) = c 2 ·h −r 6. The ballot can only be verified within one hour after submission. and outputs m as the candidate number to the voter for confirmation on the mobile device screen. The voter will then have to make the decision if m matches his/her true intent. Those shuffled ballots are then decrypted and counted in an offline ceremony. During the ceremony, the trustees are gathered on-site and submit their key shares via smartcards to a tallier machine. The tallier combines the private key and decrypts the ciphertexts one by one with NIZK proofs. The tally result is counted, and invalid votes are discarded. The final election result is announced on the main i-vote website, and all the NIZK proofs are kept on an offline medium, available to all the third-party auditors.
EA. The election authority EA consists of the collector, the i-ballot box, and the mixer.
G CERT . The (multi-session) certificate functionalityĜ CERT can be instantiated with the readily deployed Estonian national PKI infrastructure, i.e. ID-card, Mobile-ID and Digi-ID. Since the digital identification service is not exclusively setup for i-voting, we modelĜ CERT as a global functionality in the gUC [20] framework.
F VSD . The F VSD functionality is instantiated by the voter's client, the i-voting software, as well as the national ID card reader for signing operations.  F DEC . Similarly, the auditable decryption functionality F DEC is instantiated as a combination of cryptographic, physical, and organizational measures in the form of a voting ceremony. The subtle difference from the key generation ceremony is that it uses an untrusted tallier for decryption. Nevertheless, if the taller cheated during the decryption process, the auditors can detect it by checking the corresponding decryption NIZK proofs.

RELATED WORKS
In terms of modeling e-voting as a ceremony, in 2017, Kiayias et al. [18] analyzed the security of Helios in terms of an evoting ceremony using property-based definitions. In 2004, Groth [30] suggested evaluating voting schemes in the UC framework, and the ideal functionality corresponds closely to the well-known ballot box model used today in manual voting. In this case, security properties such as privacy, accuracy, and robustness follow as easy corollaries. In order to achieve an End-to-end auditable voting system along with the security properties such as correctness, privacy, fairness, and receipt-freeness, etc., Marneffe, Pereira, and Quisquater [31] investigated the use of techniques from the simulationbased security tradition for the analysis of these existing protocols, through a case-study on the ThreeBallot protocol. Further, Moran and Naor [32] presented a split-ballot voting scheme with the "everlasting privacy" property, and formally proven the security of the proposed protocol in the universal composability framework, based on number-theoretic assumptions. Alwen et al. [25] proposed the first construction of a UC receipt-free e-voting protocol, which implies that the first construction of an MPC protocol (for more than two parties) that is incredibly secure and universally composable. Afterward, Szepieniec and Preneel [26] presented a novel unifying framework for electronic voting in the UC model that includes universal verifiability.

CONCLUSION
To the best of our knowledge, the Estonian IVXV with endto-end verifiability may now be the only country allowing access to Internet voting to all its citizens. Although the Estonia IVXV can provide the available performance for the user, but there is no formal systematical security analysis of the current Estonian IVXV. In this paper, we analyzed the security of the Estonian IVXV with the help ceremony under the UC framework. Furthermore, we also present the details of the protocol, the results of implementation, and discuss the performance thereof according to Estonian Internet voting statistics collected from the recent 5-year legally binding national-wide elections.