B. Adida, Helios: Web-based open-audit voting, 17th USENIX Security Symposium (Usenix'08), pp.335-348, 2008.

B. Adida, O. Olivier-de-marneffe, J. Pereira, and . Quisquater, Electing a university president using open-audit voting: Analysis of real-world use of helios, International Conference on Electronic Voting Technology/Workshop on Trustworthy Elections, 2009.

J. C. Benaloh and M. Yung, Distributing the power of a government to enhance the privacy of voters, 5th ACM Symposium on Principles of Distributed Computing, (PODC'86, pp.52-62, 1986.

D. Bernhard, V. Cortier, D. Galindo, O. Pereira, and B. Warinschi, A comprehensive analysis of game-based ballot privacy definitions, 36th IEEE Symposium on Security and Privacy (S&P'15), pp.499-516, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01206289

D. Bernhard and B. Smyth, Ballot secrecy with malicious bulletin boards, Cryptology ePrint Archive, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102306

S. Bursuc, S. Constantin-c?t?lin-dr?gan, and . Kremer, Private votes on untrusted platforms: models, attacks and provable scheme, 4th IEEE European Symposium on Security and Privacy (EuroS&P'19), 2019.
URL : https://hal.archives-ouvertes.fr/hal-02099434

N. Chondros, B. Zhang, and T. Zacharias, Ddemos: A distributed, end-to-end verifiable, internet voting system, Panos Diamantopoulos, Stathis Maneas, Christos Patsonakis, Alex Delis, Aggelos Kiayias, and Mema Roussopoulos, pp.711-720, 2016.

M. R. Clarkson, S. Chong, and A. C. Myers, Civitas: Toward a secure voting system, IEEE Symposium on Security and Privacy (S&P'08), pp.354-368, 2008.

V. Cortier, D. Galindo, S. Glondu, and M. Izabachene, Election verifiability for Helios under weaker trust assumptions, 19th European Symposium on Research in Computer Security (ESORICS'14), vol.8713, pp.327-344
URL : https://hal.archives-ouvertes.fr/hal-01080292

. Springer, , 2014.

V. Cortier, P. Gaudry, and S. Glondu, Belenios: A Simple Private and Verifiable Electronic Voting System, pp.214-238, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02066930

V. Cortier and J. Lallemand, Voting: You can't have privacy without individual verifiability, 25th ACM Conference on Computer and Communications Security (CCS'18), pp.53-66, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01858034

C. Culnane and S. Schneider, A peered bulletin board for robust use in verifiable voting systems, 27th IEEE Computer Security Foundations Symposium (CSF 2014), pp.169-183, 2014.

J. Groth, Evaluating security of oting schemes in the universal composability framework, International Conference on Applied Cryptography and Network Securtiy, pp.46-60, 2004.

A. Kiayias, A. Kuldmaa, H. Lipmaa, J. Siim, and T. Zacharias, On the security properties of e-voting bulletin boards, 11th International Conference on Security and Cryptography for Networks (SCN 2018), pp.505-523, 2018.

O. Pereira, Real-World Electronic Voting: Design, Analysis and Deployment, chapter Internet Voting with Helios, 2016.

P. Roenne, Private communication. 1. No honest votes are modified by mod sk,U (?): ?i. ?(id, v)

, U (?)[i] = (id, v). Hence LL [j] = (id, v) for some j. Thus, by construction of LL , (id, v) is an element of LL cast , which means that BB[k] = (p, b) for some k, p, b such that (p, b) does not occur in BB 1 , extract id (p, U) / ? H, and extract(sk

, = [mod sk,U (?)(j)|?v. L[mod sk,U (?)(j)] = (id, v)], that is, since the non-? elements in LL and LL are in the same order, ?id ? H check, the same order: ?id ? H check

;. Let-id-?-h-check and . Id, = LL id succeeds: in that case, we have LL = LL, and it is sufficient to show that

, ? or this test fails, and LL = [1 . . . |BB 1 |] LL cast

, |?, issue.1

, No votes from voters in H check are modified by mod sk,U (?): ?i. ?(id, v). mod sk,U (?)[i] = (id, v) =? id ? D ? H check

, Hence LL[j] = (id, v) for some j. Thus, by construction of LL, id ? S. Since S ? D ? H check by definition, we have id ? D ? H check . 2. mod sk,U (?) keeps the votes of all voters who check: ?i. ?id ? H check . ?v. L[i] = (id, v) =? ?j. mod sk,U (?)(j) = i, that is

, Let id ? H check , i, b such that BB 1 [i] = (id, (id, b)). We distinguish two cases: ? either ?p

?. Bb, in that case, by definition of LL , i ? LL . Hence, since LL is a sublist of LL , i ? LL and the claim holds

, ? or there exists j such that BB[j] = (p , b) for some p . In that case, by construction of LL, we have LL[j] = i, and thus LL