[en] The design and implementation of a trustworthy e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how the voting system works, and what requirements on the system are relevant. In this paper, we propose that the state-of-art model checker Uppaal provides a good environment for modelling and preliminary verification of voting protocols. To illustrate this, we demonstrate how to model a version of Pret-a-Voter in Uppaal, together with some natural extensions. We also show how to verify a variant of receipt-freeness, despite the severe limitations of the property specification language in the model checker.
The aim of this work is to open a new path, rather then deliver the ultimate outcome of formal analysis. A comprehensive model of Pret-a-Voter, more accurate specification of requirements, and exhaustive verification are planned for the future.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
JAMROGA, Wojciech ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > APSIA
KIM, Yan ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > APSIA
Kurpiewski, Damian
RYAN, Peter Y A ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Towards Model Checking of Voting Protocols in Uppaal
Date de publication/diffusion :
2020
Nom de la manifestation :
Fifth International Joint Conference on Electronic Voting E-VOTE-ID 2020
Date de la manifestation :
6-9 Oct 2020
Titre de l'ouvrage principal :
Proceedings of the Fifth International Joint Conference on Electronic Voting E-VOTE-ID 2020
Adida, B.: Helios: web-based open-audit voting. In: Proceedings of the 17th Conference on Security Symposium, SS 2008, USENIX Association, Berkeley, CA, USA, pp. 335–348 (2008)
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
Beckert, B., Goré, R., Schürmann, C.: Analysing vote counting algorithms via logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 135–144. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_9
Beckert, B., Kirsten, M., Klebanov, V., Schürmann., C.: Automatic margin computation for risk-limiting audits. In: Krimmer, R. et al. (eds.) Electronic Voting. Proceedings of E-Vote-ID, Lecture Notes in Computer Science, vol. 10141, pp. 18–35. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-52240-1_2
Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems: SFM-RT. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi. org/10.1007/978-3-540-30080-9_7
Bertot, Y., Casteran, P., Huet, G., Paulin-Mohring, C.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5
Boureanu, I., Kouvaros, P., Lomuscio, A.: Verifying security properties in unbounded multiagent systems. In: Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 1209–1217 (2016)
Bruni, A., Drewsen, E., Schürmann, C.: Towards a mechanized proof of selene receipt-freeness and vote-privacy. In: Krimmer, R., Volkamer, M., Braun Binder, N., Kersting, N., Pereira, O., Schürmann, C. (eds.) E-Vote-ID 2017. LNCS, vol. 10615, pp. 110–126. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68687-5_7
Burton, C., et al.: Using Prêt à Voter in Victoria state elections. In: Proceedings of EVT/WOTE. USENIX (2012)
Chaum, D., et al.: Scantegrity II: end-to-end verifiability by voters of optical scan elections through confirmation codes. IEEE Trans. Inf. Forensics Secur. 4(4), 611– 627 (2009)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_15
Cortier, V., Galindo, D., Küsters, R., Müller, J., Truderung, T.: SoK: verifiability notions for e-voting protocols. In: IEEE Symposium on Security and Privacy, pp. 779–798 (2016)
Czerwiński, W., Lasota, S., Lazić, R., Leroux, J., Mazowiecki, F.: The reachability problem for petri nets is not elementary. In: Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing STOC, pp. 24–33. Association for Computing Machinery (2019)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)
German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)
Ghale, M.K., Goré, R., Pattinson, D., Tiwari, M.: Modular formalisation and verification of STV algorithms. In: Krimmer, R., et al. (eds.) E-Vote-ID 2018. LNCS, vol. 11143, pp. 51–66. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00419-4_4
Goranko, V., Jamroga, W.: Comparing semantics of logics for multi-agent systems. Synthese 139(2), 241–280 (2004)
Haines, T., Goré, R., Tiwari, M.: Verified verifiers for verifying elections. In: Proceedings of CCS, pp. 685–702. ACM (2019)
Jakobsson, M., Juels, A., Rivest, R.L.: Making mix nets robust for electronic voting by randomized partial checking. In: USENIX Security Symposium, pp. 339–353 (2002)
Jamroga, W.: Knowledge and strategic ability for model checking: a refined approach. In: Bergmann, R., Lindemann, G., Kirn, S., Pěchouček, M. (eds.) MATES 2008. LNCS (LNAI), vol. 5244, pp. 99–110. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87805-6_10
Jamroga, W., Knapik, M., Kurpiewski, D.: Model checking the SELENE e-voting protocol in multi-agent logics. In: Krimmer, R., et al. (eds.) E-Vote-ID 2018. LNCS, vol. 11143, pp. 100–116. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00419-4_7
Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_61
Kelsey, J., Regenscheid, A., Moran, T., Chaum, D.: Attacking Paper-Based E2E Voting Systems, pp. 370–387. Springer, Heidelberg (2010). https://doi.org/10. 1007/978-3-642-12980-3_23
Lomuscio, A., Penczek, W.: LDYIS: a framework for model checking security protocols. Fundamenta Informaticae 85(1–4), 359–375 (2008)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transfer. 19(1), 9–30 (2017)
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
Meng, B.: A critical review of receipt-freeness and coercion-resistance. Inf. Technol. J. 8(7), 934–964 (2009)
Pattinson, D., Schürmann, C.: Vote counting as mathematical proof. In: Pfahringer, B., Renz, J. (eds.) AI 2015. LNCS (LNAI), vol. 9457, pp. 464–475. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26350-2_41
Ryan, P.Y.A., Schneider, S.A., Teague, V.: End-to-end verifiability in voting systems, from theory to practice. IEEE Secur. Priv. 13(3), 59–62 (2015)
Ryan, P.Y.A.: The computer ate my vote. In: Boca, P., Bowen, J., Siddiqi, J. (eds.) Formal Methods: State of the Art and New Directions, pp. 147–184. Springer, London (2010). https://doi.org/10.1007/978-1-84882-736-3_5
Ryan, P.Y.A., Rønne, P.B., Iovino, V.: Selene: voting with transparent verifiability and coercion-mitigation. In: Clark, J., et al. (eds.) Financial Cryptography and Data Security. Lecture Notes in Computer Science, vol. 9604, pp. 176–192. Springer, Heidelberg (2016)
Ryan, P.Y.A., Teague, V.: Pretty good democracy. In: Christianson, B., Malcolm, J.A., Matyáš, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol. 7028, pp. 111–130. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36213-2_15
Zollinger, M.-L., Roenne, P., Ryan, P.Y.A.: Mechanized proofs of verifiability and privacy in a paper-based e-voting scheme. In: Proceedings of 5th Workshop on Advances in Secure Electronic Voting (2020)
