S. Heiberg, P. Laud, and J. Willemson, The application of I-Voting for Estonian parliamentary elections of 2011, VoteID 2011, ser. LNCS, vol.7187, pp.208-223, 2012.

, iVote system -NSW Electoral Commission

R. Haenni, R. E. Koenig, P. Locher, and E. Dubuis, CHVote system specification, 2017.

V. Cortier and B. Smyth, Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security, vol.21, issue.1, pp.89-148, 2013.
URL : https://hal.archives-ouvertes.fr/inria-00638556

R. Küsters, T. Truderung, and A. Vogt, Clash Attacks on the Verifiability of E-Voting Systems, 33rd IEEE Symposium on Security and Privacy (S&P'12), pp.395-409, 2012.

S. Wolchok, E. Wustrow, D. Isabel, and J. A. Halderman, Internet voting system, Financial Cryptography and Data Security (FC'12), 2012.

D. Springall, T. Finkenauer, Z. Durumeric, J. Kitcat, H. Hursti et al., Security Analysis of the Estonian Internet Voting System, ACM Conference on Computer and Communications Security (CCS'14), pp.703-715, 2014.

O. De-marneffe, O. Pereira, and J. Quisquater, Electing a university president using open-audit voting: Analysis of real-world use of Helios, 2009 Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, EVT/WOTE '09, 2009.

A. T. Sherman, R. A. Fink, R. Carback, and D. Chaum, Scantegrity III: automatic trustworthy receipts, highlighting over/under votes, and full voter verifiability, 2011 Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, EVT/WOTE '11, 2011.

P. Ryan, Prêt à Voter with Paillier encryption, Mathematical and Computer Modelling, vol.48, issue.9, pp.1646-1662, 2008.

S. Bell, J. Benaloh, M. D. Byrne, D. Debeauvoir, B. Eakin et al., STAR-Vote: A secure, transparent, auditable, and reliable voting system, Electronic Voting Technology Workshop/Workshop on Trustworthy Elections (EVT/WOTE'13), 2013.

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.

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

R. Küsters, J. Müller, E. Scapin, and T. Truderung, sElect: A lightweight verifiable remote voting system, IEEE Computer Security Foundations Symposium (CSF'16), pp.341-354, 2016.

P. Y. Ryan, P. B. Roenne, and V. Iovino, Selene: Voting with transparent verifiability and coercion-mitigation, 1st Workshop on Secure Voting Systems (VOTING'16), pp.176-192, 2016.
DOI : 10.1007/978-3-662-53357-4_12

URL : https://hal.archives-ouvertes.fr/hal-01242690

D. Galindo, S. Guasch, and J. Puiggali, Neuchâtel's cast-asintended verification mechanism, 5th International Conference on E-Voting and Identity, pp.3-18, 2015.
DOI : 10.1007/978-3-319-22270-7_1

D. A. Basin, S. Radomirovic, and L. Schmid, Alethea: A provably secure random sample voting protocol, 31st IEEE Computer Security Foundations Symposium (CSF'18), pp.283-297, 2018.

N. Chondros, B. Zhang, T. Zacharias, P. Diamantopoulos, S. Maneas et al., D-DEMOS: A distributed, end-to-end verifiable, internet voting system, 36th IEEE International Conference on Distributed Computing Systems, ICDCS 2016, pp.711-720, 2016.

A. Kiayias, T. Zacharias, and B. Zhang, DEMOS-2: Scalable E2E verifiable elections without random oracles, ACM Conference on Computer and Communications Security (CCS'15), 2015.

D. Chaum, Surevote: Technical overview, Workshop on Trustworthy Elections (WOTE '01), 2001.

P. Chaidos, V. Cortier, G. Fuchsbauer, and D. Galindo, BeleniosRF: A non-interactive receipt-free electronic voting scheme, 23rd ACM Conference on Computer and Communications Security (CCS'16)
URL : https://hal.archives-ouvertes.fr/hal-01377917

O. Blazy, G. Fuchsbauer, D. Pointcheval, and D. Vergnaud, Signatures on randomizable ciphertexts, 14th International Conference on Practice and Theory in Public Key Cryptography, pp.403-422, 2011.
DOI : 10.1007/978-3-642-19379-8_25

URL : https://hal.archives-ouvertes.fr/inria-00542643

B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423760

K. Bhargavan, R. Corin, C. Fournet, and E. Zalinescu, Cryptographically Verified Implementations for TLS, 15th ACM Conference on Computer and Communications Security (CCS'08), pp.459-468, 2008.
DOI : 10.1145/1455770.1455828

V. Cortier and C. Wiedling, A formal analysis of the Norwegian E-voting protocol, Journal of Computer Security, vol.25, issue.15777, pp.21-57, 2017.
URL : https://hal.archives-ouvertes.fr/inria-00636115

B. Blanchet, Symbolic and computational mechanized verification of the ARINC823 avionic protocols, 30th IEEE Computer Security Foundations Symposium (CSF'17, pp.68-82, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575861

V. Cortier, F. Eigner, S. Kremer, M. Maffei, and C. Wiedling, Typebased verification of electronic voting protocols, 4th Conference on Principles of Security and Trust (POST'15), ser. LNCS, vol.9036, pp.303-323, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01103545

V. Cortier, D. Galindo, S. Glondu, and M. Izabachene, Distributed ElGamal à la Pedersen -application to Helios, Workshop on Privacy in the Electronic Society (WPES 2013), 2013.
DOI : 10.1145/2517840.2517852

URL : https://hal.archives-ouvertes.fr/hal-00881076

R. Focardi, F. L. Luccio, and H. A. Wahsheh, Usable cryptographic qr codes, IEEE International Conference on Industrial Technology (ICIT 2018), 2018.
DOI : 10.1109/icit.2018.8352431

S. Delaune, S. Kremer, and M. D. Ryan, Verifying privacy-type properties of electronic voting protocols: A taster, Towards Trustworthy Elections -New Directions in Electronic Voting, ser. LNCS, vol.6000, pp.289-309, 2010.

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), ser. LNCS, vol.8713, pp.327-344, 2014.
DOI : 10.1007/978-3-319-11212-1_19

URL : https://hal.archives-ouvertes.fr/hal-01011294

V. Cortier, D. Galindo, and M. Turuani, A formal analysis of the Neuchâtel e-voting protocol, 3rd IEEE European Symposium on Security and Privacy (EuroSP'18), 2018.

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

B. Schmidt, S. Meier, C. Cremers, and D. Basin, Automated analysis of Diffie-Hellman protocols and advanced security properties, 25th IEEE Computer Security Foundations Symposium, CSF 2012, pp.78-94, 2012.

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

, new c vs : channel; new c vd : channel

, Registrar(id, c vs ) | VoterAudit A (id, c vs

|. Vd,

|. Vs,

|. ,

, new c vs : channel; new c vd : channel

, Registrar(id, c vs ) | VoterAudit B (id, c vs

|. Vd,

|. Vs,

|. ,

, V CHV (t)(v) = |{id ? CHV(t)|Voted(id, v) ? t}| ? |{id ? CHV(t)|?id , cred, b, l. Voted(id, v) ? t ? Voter

, Thus for all id ? CHV(t) such that Voter(id, cred, l) ? t for some cred, l, we know that l = H. Hence, by the recorded-as-intended property on credentials, V CHV (t)(v) ? |{id ? CHV(t)|?id , cred, b, l. Voter(id, cred, l) ? t ? Going-to-tally(id , cred, b) ? t ? valid(b) ? v = open(b)}| ? |{cred|?id ? CHV(t), By assumption, each voter is only registered once and CHV(t) ? HV(t)