Machine-checked proofs of privacy against malicious boards for Selene & Co 1

Abstract

Privacy is a notoriously difficult property to achieve in complicated systems and especially in electronic voting schemes. Moreover, electronic voting schemes is a class of systems that require very high assurance. The literature contains a number of ballot privacy definitions along with security proofs for common systems. Some machine-checked security proofs have also appeared. We define a new ballot privacy notion that captures a larger class of voting schemes. This notion improves on the state of the art by taking into account that verification in many schemes will happen or must happen after the tally has been published, not before as in previous definitions.

As a case study we give a machine-checked proof of privacy for Selene, which is a remote electronic voting scheme which offers an attractive mix of security properties and usability. Prior to our work, the computational privacy of Selene has never been formally verified. Finally, we also prove that MiniVoting and Belenios satisfies our definition.

Keywords

Formal verification e-voting Selene privacy

Get full access to this article

View all access options for this article.

References

Barthe,

Dupressoir,

Grégoire,

Kunz,

Schmidt and

P.-Y.

Strub, EasyCrypt: A Tutorial, Springer International Publishing, Cham, 2014, pp. 146–166.

Bellare and

Rogaway, Random oracles are practical: A paradigm for designing efficient protocols, in: ACM CCS 93,

D.E.

Denning,

Pyle,

Ganesan,

R.S.

Sandhu and

Ashby, eds, ACM Press, 1993, pp. 62–73.

Bellare and

Sahai, Non-malleable encryption: Equivalence between two notions, and an indistinguishability-based characterization, in: CRYPTO’99,

M.J.

Wiener, ed., LNCS, vol. 1666, Springer, Heidelberg, 1999, pp. 519–536.

Bernhard, Zero-knowledge proofs in theory and practice, PhD thesis, University of Bristol, 2014.

Bernhard,

Cortier,

Galindo,

Pereira and

Warinschi, SoK: A comprehensive analysis of game-based ballot privacy definitions, in: 2015 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2015, pp. 499–516. doi:10.1109/SP.2015.37.

Bernhard,

Cortier,

Pereira,

Smyth and

Warinschi, Adapting helios for provable ballot privacy, in: ESORICS 2011,

Atluri and

Díaz, eds, LNCS, Vol. 6879, Springer, Heidelberg, 2011, pp. 335–354.

Bernhard,

Pereira and

Warinschi, How not to prove yourself: Pitfalls of the Fiat–Shamir heuristic and applications to Helios, in: ASIACRYPT 2012,

Wang and

Sako, eds, LNCS, Vol. 7658, Springer, Heidelberg, 2012, pp. 626–643. doi:10.1007/978-3-642-34961-4_38.

Bruni,

Drewsen and

Schürmann, Towards a mechanized proof of Selene receipt-freeness and vote-privacy, in: International Joint Conference on Electronic Voting, Springer, 2017, pp. 110–126. doi:10.1007/978-3-319-68687-5_7.

Chaidos,

Cortier,

Fuchsbauer and

Galindo, BeleniosRF: A non-interactive receipt-free electronic voting scheme, in: ACM CCS 2016,

E.R.

Weippl,

Katzenbeisser,

Kruegel,

A.C.

Myers and

Halevi, eds, ACM Press, 2016, pp. 1614–1625.

10.

Cortier,

C.C.

Dragan,

Dupressoir,

Schmidt,

P.-Y.

Strub and

Warinschi, Machine-checked proofs of privacy for electronic voting protocols, in: 2017 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2017, pp. 993–1008. doi:10.1109/SP.2017.28.

11.

Cortier,

C.C.

Dragan,

Dupressoir and

Warinschi, Machine-checked proofs for electronic voting: Privacy and verifiability for Belenios, in: CSF 2018 Computer Security Foundations Symposium,

Chong and

Delaune, eds, IEEE Computer Society Press, 2018, pp. 298–312.

12.

Cortier,

Galindo,

Glondu and

Izabachène, Election verifiability for helios under weaker trust assumptions, in: ESORICS 2014, Part II,

Kutylowski and

Vaidya, eds, LNCS, Vol. 8713, Springer, Heidelberg, 2014, pp. 327–344.

13.

Cortier,

Lallemand and

Warinschi, Fifty shades of ballot privacy: Privacy against a malicious board, in: CSF 2020 Computer Security Foundations Symposium,

Jia and

Küsters, eds, IEEE Computer Society Press, 2020, pp. 17–32.

14.

C.C.

Drăgan,

Dupressoir,

Estaji,

Gjøsteen,

Haines,

P.Y.A.

Ryan,

P.B.

Rønne and

M.R.

Solberg, Machine-checked proofs of privacy against malicious boards for Selene & Co, in: 2022 IEEE 35th Computer Security Foundations Symposium (CSF), 2022, pp. 335–347. doi:10.1109/CSF54842.2022.9919663.

15.

ElGamal, A public key cryptosystem and a signature scheme based on discrete logarithms, in: CRYPTO’84,

G.R.

Blakley and

Chaum, eds, LNCS, vol. 196, Springer, Heidelberg, 1984, pp. 10–18.

16.

Haines,

Goré and

Sharma, Did you mix me? Formally verifying verifiable mix nets in electronic voting, in: IEEE Symposium on Security and Privacy, IEEE, 2021, pp. 1748–1765.

17.

Haines,

Goré and

Tiwari, Verified verifiers for verifying elections, in: ACM CCS 2019,

Cavallaro,

Kinder,

Wang and

Katz, eds, ACM Press, 2019, pp. 685–702.

18.

Kremer and

P.B.

Rønne, To du or not to du: A security analysis of du-vote, in: 2016 IEEE European Symposium on Security and Privacy (EuroS&P), IEEE, 2016, pp. 473–486. doi:10.1109/EuroSP.2016.42.

19.

Küsters,

Müller,

Scapin and

Truderung, Select: A lightweight verifiable remote voting system, in: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), IEEE, 2016, pp. 341–354. doi:10.1109/CSF.2016.31.

20.

P.B.

Rønne,

P.Y.

Ryan and

M.-L.

Zollinger, Electryo, in-person voting with transparent voter verifiability and eligibility verifiability, 2021, arXiv preprint arXiv:2105.14783.

21.

P.Y.A.

Ryan,

P.B.

Rønne and

Iovino, Selene: Voting with transparent verifiability and coercion-mitigation, in: FC 2016 Workshops,

Clark,

Meiklejohn,

P.Y.A.

Ryan,

D.S.

Wallach,

Brenner and

Rohloff, eds, LNCS, Vol. 9604, Springer, Heidelberg, 2016, pp. 176–192.

22.

Sallal,

S.A.

Schneider,

Casey,

C.C.

Dragan,

Dupressoir,

Riley,

Treharne,

Wadsworth and

Wright, VMV: Augmenting an internet voting system with Selene verifiability, 2019, CoRR abs/1912.00288.

23.

Shoup, A proposal for an ISO standard for public key encryption, Cryptology ePrint Archive, Report 2001/112, 2001. https://eprint.iacr.org/2001/112.

24.

Shoup, Sequences of games: A tool for taming complexity in security proofs, Cryptology ePrint Archive, Report 2004/332, 2004. https://eprint.iacr.org/2004/332.

25.

M.-L.

Zollinger,

P.B.

Rønne and

P.Y.

Ryan, Short paper: Mechanized proofs of verifiability and privacy in a paper-based e-voting scheme, in: International Conference on Financial Cryptography and Data Security, Springer, 2020, pp. 310–318. doi:10.1007/978-3-030-54455-3_22.