Electronic voting promises the possibility of convenient and efficient systems for recording and tallying votes in an election. To be widely adopted, ensuring the security of the cryptographic protocols used in e-voting is of paramount importance. However, the security analysis of this type of protocol raises a number of challenges, and they are often out of reach of existing verification tools. In this paper, we study vote privacy, a central security property that should be satisfied by any e-voting system. More precisely, we propose the first formalisation of the recent BPRIV notion in the symbolic setting. To ease the formal security analysis of this notion, we propose a reduction result allowing one to bind the number of voters and ballots needed to mount an attack. We first consider the case where voters do not revote, and the ballot box is trusted. Then, we extend this reduction result, as well as our formalisation of BPRIV, to account for the case of re-voting and a dishonest ballot box. We apply our reduction results to a number of case studies including several versions of Helios, Belenios, JCJ/Civitas, and Prêt-à-Voter. For some of these protocols, thanks to our result, we are able to conduct the analysis relying on the automatic tool Proverif.
AdidaB. Helios: web-based open-audit voting. In: van Oorschot PC (ed.) Proceedings of the 17th USENIX security symposium, San Jose, CA, USA, 28 July–1 August 2008, pp.335–348. Berkeley, CA, USA: USENIX Association.
2.
BenalohJCYungM. Distributing the power of a government to enhance the privacy of voters (extended abstract). In: Halpern JY (ed.) Proceedings of the 5th annual ACM symposium on principles of distributed computing, Calgary, Alberta, Canada, 11–13 August 1986, pp.52–62. New York, NY, USA: Association for Computing Machinery.
BackesMHritcuCMaffeiM. Automated verification of remote electronic voting protocols in the applied pi calculus. In: Proceedings of the 21st IEEE computer security foundations symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23–25 June 2008, pp.195–209. Los Alamitos, CA, USA: IEEE Computer Society.
5.
CortierVSmythB. Attacking and fixing helios: an analysis of ballot secrecy. J Comput Sec2013; 21: 89–148.
6.
ArapinisMCortierVKremerS. When are three voters enough for privacy properties? In: Proceedings of the 21st European symposium on research in computer security (ESORICS’16), Heraklion, Greece, September 26-30, 2016, LNCS, vol. 9879, pp. 241--260. Cham, Switzerland: Springer.
7.
CortierVWiedlingC. A formal analysis of the Norwegian e-voting protocol. J Comput Sec2017; 25: 21–57.
8.
CortierVGalindoDTuruaniM. A formal analysis of the Neuchâtel e-voting protocol. In: 3rd IEEE European symposium on security and privacy (Euro S&P’18). London, UK, April 24-26, 2018, pp.430–442. Los Alamitos, CA, USA: IEEE Computer Society.
9.
BasinDARadomirovicSSchmidL. Alethea: a provably secure random sample voting protocol. In: 31st IEEE computer security foundations symposium, (CSF’18), Oxford, UK, July 9-12, 2018, pp. 283--297. Los Alamitos, CA, USA: IEEE Computer Society.
BernhardDCortierVGalindoD, et al.A comprehensive analysis of game-based ballot privacy definitions. In: Proceedings of the 36th IEEE symposium on security and privacy (S&P’15), San Jose, CA, USA, May 17-21, 2015, Los Alamitos, CA, USA: IEEE Computer Society.
12.
CortierVLallemandJWarinschiB. Fifty shades of ballot privacy: Privacy against a malicious board. In: 33rd IEEE computer security foundations symposium (CSF’20), June 22-26, 2020, Boston, USA, pp.17--32. Los Alamitos, CA, USA: IEEE Computer Society.
13.
DelauneSHirschiL. A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J Log Algeb Methods Program2017; 87: 127–144.
14.
MödersheimSViganòL. Alpha–beta privacy. ACM Trans Priv Secur2019; 22: 7:1–7:35, Association for Computing Machinery, New York, NY, USA.
15.
BlanchetB. An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE computer security foundations workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, 11-13 June 2001, pp.82–96. Los Alamitos, CA, USA: IEEE Computer Society.
16.
BlanchetB. Modeling and verifying security protocols with the applied pi calculus and proVerif. Found Trends Privacy Sec2016; 1: 1–135.
17.
MeierSSchmidtBCremersC, et al.The TAMARIN prover for the symbolic analysis of security protocols. In: Computer aided verification, 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13-19, LNCS, vol. 8044, 2013, pp.696–701. Cham, Switzerland: Springer.
18.
BlanchetBAbadiMFournetC. Automated verification of selected equivalences for security protocols. In: 20th IEEE symposium on logic in computer science (LICS 2005), Chicago, IL, 2005, pp.331–340. 26-29 June 2005, Los Alamitos, CA, USA: IEEE Computer Society.
19.
BasinDADreierJSasseR. Automated symbolic proofs of observational equivalence. In: Ray I, Li N and Kruegel C (eds.) Proceedings of the 22nd ACM SIGSAC conference on computer and communications security, Denver, CO, USA, 12–16 October 2015, pp.1144-1155. New York, NY, USA: Association for Computing Machinery.
20.
CortierVFilipiakALallemandJ. BeleniosVS: Secrecy and verifiability against a corrupted voting device. In: 32nd IEEE computer security foundations symposium, CSF 2019, Hoboken, NJ, USA, 25–28 June 2019. Los Alamitos, CA, USA: IEEE Computer Society.
21.
BlanchetBSmythB. Automated reasoning for equivalences in the applied pi calculus with barriers. J Comput Sec2018; 26: 367–422.
22.
Comon-LundhHCortierV. Security properties: two agents are sufficient. In: Proceedings of 12th European symposium on programming (ESOP’03), April 7-11, 2003, Warsaw, Poland, LNCS, Vol. 2618, 2003, pp.99–113. Cham, Switzerland: Springer.
23.
CortierVDallonADelauneS. Bounding the number of agents, for equivalence too. In: Proceedings of the 5th International conference on principles of security and Trust (POST’16), April 2-16, 2016, Eindhoven, the Netherlands, LNCS, pp.211–232. Cham, Switzerland: Springer.
24.
FröschleS. Leakiness is decidable for well-founded protocols? In: Proceedings of the 4th conference on principles of security and trust (POST’15), London, UK, April 11-18, LNCS, vol. 9036, pp. 176–195. Cham, Switzerland: Springer.
25.
D’OsualdoEOngLTiuA. Deciding secrecy of security protocols for an unbounded number of sessions: The case of depth-bounded processes. In Proceedings of the 30th computer security foundations symposium, (CSF’17), Santa Barbara, CA, USA, August 21-25, 2017, pp.464–480. Los Alamitos, CA, USA: IEEE Computer Society.
26.
DelauneSLallemandJ. One vote is enough for analysing privacy. In: Atluri V, Pietro RD, Jensen CD, et al. (eds) Computer security – ESORICS 2022 – 27th European symposium on research in computer security, Copenhagen, Denmark, 26–30 September 2022, proceedings, part I, lecture notes in computer science, vol. 13554, 2022, pp.173–194. Cham, Switzerland: Springer. https://doi.org/10.1007/978-3-031-17140-6_9.
27.
AbadiMFournetC. Mobile values, new names, and secure communication. In: Hankin C and Schmidt D (eds) Conference record of POPL 2001: The 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages, London, UK, 17–19 January 2001, pp.104–115. New York, NY, USA: Association for Computing Machinery.
28.
CortierVGaudryPGlonduS. Belenios: A simple private and verifiable electronic voting system. In: Foundations of security, protocols, and equational reasoning – essays dedicated to Catherine A. Meadows, LNCS, 2019, vol. 11565, pp.214–238. Cham, Switzerland: Springer.
29.
ChaidosPCortierVFuchsbauerG, et al.BeleniosRF: a non-interactive receipt-free electronic voting scheme. In: 23rd ACM conference on computer and communications security (CCS’16), Vienna, Austria, 2016, pp.1614–1625. New York, NY, USA: Association for Computing Machinery.
30.
JuelsACatalanoDJakobssonM. Coercion-resistant electronic elections. In: Chaum D, Jakobsson M, Rivest RL, et al. (eds) Towards trustworthy elections, new directions in electronic voting, LNCS, vol. 6000, 2010, pp. 37–63. Cham, Switzerland: Springer.
31.
ChaumDRyanPYASchneiderSA. A practical voter-verifiable election scheme. In: di Vimercati SDC, Syverson PF and Gollmann D (eds) Computer security – ESORICS 2005, 10th European symposium on research in computer security, Milan, Italy, 12–14 September 2005, proceedings, LNCS, vol. 3679, 2005, pp.118–139. Cham, Switzerland: Springer.
32.
RyanPYASchneiderSA. Prêt à voter with re-encryption mixes. In: Gollmann D, Meier J and Sabelfeld A (eds) Computer security – ESORICS 2006, 11th European symposium on research in computer security, Hamburg, Germany, 18–20 September 2006, proceedings, LNCS, vol. 4189, 2006, pp.313–326. Cham, Switzerland: Springer.
33.
ClarksonMRChongSMyersAC. Civitas: toward a secure voting system. In: 2008 IEEE symposium on security and privacy (S&P 2008), 18–21 May 2008, Oakland, California, USA, 2008, pp.354–368. Los Alamitos, CA, USA: IEEE Computer Society.
34.
RyanPYASchneiderSA. Prêt à voter with re-encryption mixes. In: Gollmann D, Meier J and Sabelfeld A (eds) Computer security – ESORICS 2006, 11th European symposium on research in computer security, Hamburg, Germany, 18–20 September 2006, proceedings, LNCS, vol. 4189, 2006, pp.313–326. Cham, Switzerland: Springer.
35.
ChevalVRakotonirinaI. Indistinguishability beyond diff-equivalence in proverif. In: 36th IEEE computer security foundations symposium, CSF 2023, Dubrovnik, Croatia, 10–14 July 2023, pp.184–199. Los Alamitos, CA, USA: IEEE Computer Society. https://doi.org/10.1109/CSF57540.2023.00036.
36.
DelauneSLallemandJOutreyA. One vote is enough for analysing privacy. Technical report, CNRS, 2023. https://hal.science/hal-04262499.
