[en] Belenios is an online voting system that provides a strong notion of election verifiability, where no single party has to be trusted, and security holds as soon as either the voting registrar or the voting server is honest. It was formally proved to be secure, making the assump- tion that no further ballots are cast on the bulletin board after voters verified their ballots. In practice, however, revoting is allowed and voters can verify their ballots anytime. This gap between formal proofs and use in practice leaves open space for attacks, as has been shown recently. In this paper we make two simple additions to Belenios and we formally prove that the new version satisfies the expected verifiability properties. Our proofs are automatically performed with the Tamarin prover, under the assumption that voters are allowed to vote at most four times.
Disciplines :
Computer science
Author, co-author :
BALOGLU, Sevdenur ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > PI Mauw
BURSUC, Sergiu ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > PI Mauw
MAUW, Sjouke ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
PANG, Jun ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
External co-authors :
no
Language :
English
Title :
Provably Improving Election Verifiability in Belenios
Publication date :
October 2021
Event name :
6th International Joint Conference on Electronic Voting, E-Vote-ID 2021
Event date :
from 05-10-2021 to 08-10-2021
Main work title :
Electronic Voting 6th International Joint Conference, E-Vote-ID 2021 Virtual Event, October 5–8, 2021, Proceedings
Tamarin specifications for the variants of Belenios. https://github.com/sbaloglu/tamarin-codes/tree/main/belenios-zkp
Adida, B.: Helios: web-based open-audit voting. In: van Oorschot, P.C. (ed.) Proceedings of the 17th USENIX Security Symposium, San Jose, CA, USA, 28 July–1 August 2008, pp. 335–348. USENIX Association (2008). http://www.usenix.org/events/sec08/tech/full papers/adida/adida.pdf
Adida, B., De Marneffe, O., Pereira, O., Quisquater, J.J.: Electing a university president using open-audit voting: analysis of real-world use of Helios. In: 2009 Electronic Voting Technology Workshop/Workshop on Trustworthy Elections. USENIX (2009)
Arapinis, M., Cortier, V., Kremer, S.: When are three voters enough for privacy properties? In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 241–260. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45741-3 13
Baloglu, S., Bursuc, S., Mauw, S., Pang, J.: Election verifiability revisited: automated security proofs and attacks on Helios and Belenios. In: 34th IEEE Computer Security Foundations Symposium (2021). https://eprint.iacr.org/2020/982
Castéran, P., Bertot, Y.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004). https://hal.archives-ouvertes.fr/hal-00344237
Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: toward a secure voting system. In: 2008 IEEE Symposium on Security and Privacy (S&P 2008), Oakland, California, USA, 18–21 May 2008, pp. 354–368 (2008). https://doi.org/10.1109/SP.2008.32
Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 99–113. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36575-3 8
Cortier, V., Dallon, A., Delaune, S.: Bounding the number of agents, for equivalence too. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 211–232. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49635-0 11
Cortier, V., Drăgan, C.C., Dupressoir, F., Warinschi, B.: Machine-checked proofs for electronic voting: privacy and verifiability for Belenios. In: Proceedings of the 31st IEEE Computer Security Foundations Symposium, pp. 298–312. IEEE Computer Society (2018). https://doi.org/10.1109/CSF.2018.00029
Cortier, V., Filipiak, A., Lallemand, J.: BeleniosVS: secrecy and verifiability against a corrupted voting device. In: 32nd IEEE Computer Security Foundations Symposium, pp. 367–381 (2019). https://doi.org/10.1109/CSF.2019.00032
Cortier, V., Gaudry, P., Glondu, S.: Belenios: a simple private and verifiable electronic voting system. In: Guttman, J.D., Landwehr, C.E., Meseguer, J., Pavlovic, D. (eds.) Foundations of Security, Protocols, and Equational Reasoning. LNCS, vol. 11565, pp. 214–238. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-19052-1 14
Cortier, V., Smyth, B.: Attacking and fixing Helios: an analysis of ballot secrecy. J. Comput. Secur. 21(1), 89–148 (2013). https://doi.org/10.3233/JCS-2012-0458
ElGamal, T.: A public key cryptosystem and a signature scheme based on discrete logarithms. In: Blakley, G.R., Chaum, D. (eds.) CRYPTO 1984. LNCS, vol. 196, pp. 10–18. Springer, Heidelberg (1985). https://doi.org/10.1007/3-540-39568-7 2
Hirt, M., Sako, K.: Efficient receipt-free voting based on homomorphic encryption. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 539–556. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-45539-6 38
Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. In: Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, WPES, pp. 61–70 (2005). https://doi.org/10.1145/1102199.1102213
Küsters, R., Truderung, T., Vogt, A.: Verifiability, privacy, and coercion-resistance: new insights from a case study. In: 32nd IEEE Symposium on Security and Privacy, pp. 538–553. IEEE Computer Society (2011). https://doi.org/10.1109/SP.2011.21
Küsters, R., Truderung, T., Vogt, A.: Clash attacks on the verifiability of e-voting systems. In: 33rd IEEE Symposium on Security and Privacy, pp. 395–409. IEEE Computer Society (2012). https://doi.org/10.1109/SP.2012.32
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8 48
Pedersen, T.P.: Non-interactive and information-theoretic secure verifiable secret sharing. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 129–140. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-46766-1 9
Pereira, O., Wallach, D.S.: Clash attacks and the STAR-vote system. In: Krimmer, R., Volkamer, M., Braun Binder, N., Kersting, N., Pereira, O., Schürmann, C. (eds.) E-Vote-ID 2017. LNCS, vol. 10615, pp. 228–247. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68687-5 14
Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 25th IEEE Computer Security Foundations Symposium, (CSF 2012), pp. 78–94. IEEE Computer Society (2012). https://doi.org/10.1109/CSF.2012.25
