[en] Voting procedures are designed and implemented by people, for people, and with significant human involvement. Thus, one should take into account the human factors in order to comprehensively analyze properties of an election and detect threats. In particular, it is essential to assess how actions and strategies of the involved agents (voters, municipal office employees, mail clerks) can influence the outcome of other agents’ actions as well as the overall outcome of the election. In this paper, we present our first attempt to capture those aspects in a formal multi-agent model of the Polish presidential election 2020. The election marked the first time when postal vote was universally available in Poland. Unfortunately, the voting scheme was prepared under time pressure and political pressure, and without the involvement of experts. This might have opened up possibilities for various kinds of ballot fraud, in-house coercion, etc. We propose a preliminary scalable model of the procedure in the form of a Multi-Agent Graph, and formalize selected integrity and security properties by formulas of agent logics. Then, we transform the models and formulas so that they can be input to the state-of-art model checker Uppaal. The first series of experiments demonstrates that verification scales rather badly due to the state-space explosion. However, we show that a recently developed technique of user-friendly model reduction by variable abstraction allows us to verify more complex scenarios.
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002). https://doi.org/10.1145/585265.585270
Andrzej Rzepliński, M.S.: Statement on election irregularities [polish: Oświadczenia w sprawie nieprawidłowości dotyczących wyborów]. https://ow.org.pl/2020/08/05/oswiadczenia-w-sprawie-nieprawidlowosci-dotyczacych-wyborow/
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
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Basin, D., Gersbach, H., Mamageishvili, A., Schmid, L., Tejada, O.: Election security and economics: it’s all about eve. In: Krimmer, R., Volkamer, M., Braun Binder, N., Kersting, N., Pereira, O., Schürmann, C. (eds.) E-Vote-ID 2017. LNCS, vol. 10615, pp. 1–20. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68687-5_1
Basin, D.A., Radomirovic, S., Schmid, L.: Modeling human errors in security protocols. In: Computer Security Foundations Symposium, CSF, pp. 325–340. IEEE Computer Society (2016). https://doi.org/10.1109/CSF.2016.30
Beckert, B., Beuster, G.: A method for formalizing, analyzing, and verifying secure user interfaces. In: International Conference on Formal Engineering Methods, pp. 55–73. Springer, Cham (2006)
Behrmann, G., David, A., Larsen, K.: A tutorial on uppaal. In: Formal Methods for the Design of Real-Time Systems: SFM-RT. LNCS, pp. 200–236, vol. 3185. Springer, Cham (2004)
Bella, G., Curzon, P., Giustolisi, R., Lenzini, G.: A socio-technical methodology for the security and privacy analysis of services. In: COMPSAC Workshops, pp. 401–406. IEEE Computer Society (2014). https://doi.org/10.1109/COMPSACW.2014.69
Bella, G., Curzon, P., Lenzini, G.: Service security and privacy as a socio-technical problem. J. Comput. Secur. 23(5), 563–585 (2015). https://doi.org/10.3233/JCS-150536
Bella, G., Giustolisi, R., Schürmann, C.: Modelling human threats in security ceremonies. J. Comput. Secur. (Preprint) 1–23 (2022)
Benaloh, J., Ryan, P.Y., Teague, V.: Verifiable postal voting. In: Cambridge International Workshop on Security Protocols, pp. 54–65. Springer, Cham (2013)
Blanchet, B., et al.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends® Privacy Secur. 1(1-2), 1–135 (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
Bruni, A., Carbone, M., Giustolisi, R., Mödersheim, S., Schürmann, C.: Security protocols as choreographies. In: Dougherty, D., Meseguer, J., Mödersheim, S.A., Rowe, P. (eds.) Protocols, Strands, and Logic. LNCS, vol. 13066, pp. 98–111. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-91631-2_5
Buldas, A., Mägi, T.: Practical security analysis of e-voting systems. In: Proceedings of IWSEC. LNCS, vol. 4752, pp. 320–335. Springer, Cham (2007)
Carlos, M.C., Martina, J.E., Price, G., Custódio, R.F.: A proposed framework for analysing security ceremonies. In: SECRYPT, pp. 440–445. SciTePress (2012)
Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R., et al.: Handbook of model checking, vol. 10. Springer, Cham (2018)
Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Cortier, V., Filipiak, A., Lallemand, J.: Beleniosvs: secrecy and verifiability against a corrupted voting device. In: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pp. 367–36714. IEEE (2019)
Cortier, V., Galindo, D., Turuani, M.: A formal analysis of the neuchâtel e-voting protocol. In: 2018 IEEE European Symposium on Security and Privacy (EuroS &P), pp. 430–442. IEEE (2018)
Dastani, M., Hindriks, K., Meyer, J. (eds.): Specification and Verification of Multi-Agent Systems. Springer, Cham (2010)
Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier (1990)
Fakt.pl: Ballot papers without stamp were delivered. Will the votes be invalid? [Polish: Dostali karty do głosowania bez pieczęci. Czy głosy będą nieważne?]. https://www.fakt.pl/wydarzenia/polityka/dostali-karty-do-glosowania-bez-pieczeci-czy-glosy-beda-niewazne/6cwhzg4
Haines, T., Goré, R., Tiwari, M.: Verified verifiers for verifying elections. In: Proceedings of CCS, pp. 685–702. ACM (2019). https://doi.org/10.1145/3319535.3354247
Haines, T., Goré, R., Sharma, B.: Did you mix me? Formally verifying verifiable mix nets in electronic voting. In: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24–27 May 2021, pp. 1748–1765. IEEE (2021). https://doi.org/10.1109/SP40001.2021.00033
Jamroga, W., Knapik, M., Kurpiewski, D.: Model checking the SELENE e-voting protocol in multi-agent logics. In: Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID). LNCS, vol. 11143, pp. 100–116. Springer, Cham (2018)
Jamroga, W., Tabatabaei, M.: Preventing coercion in e-voting: be open and commit. In: Krimmer, R., et al. (eds.) E-Vote-ID 2016. LNCS, vol. 10141, pp. 1–17. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52240-1_1
Jamroga, W., Kim, Y.: Practical abstraction for model checking of multi-agent systems (2022). https://doi.org/10.48550/ARXIV.2202.12016
Jamroga, W., Kim, Y., Kurpiewski, D., Ryan, P.Y.A.: Towards model checking of voting protocols in Uppaal. In: Krimmer, R., et al. (eds.) E-Vote-ID 2020. LNCS, vol. 12455, pp. 129–146. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-60347-2_9
Jamroga, W., Kurpiewski, D., Malvone, V.: Natural strategic abilities in voting protocols. In: Proceedings of STAST 2020 (2021, to appear)
Jamroga, W., Mestel, D., Roenne, P.B., Ryan, P.Y.A., Skrobot, M.: A survey of requirements for COVID-19 mitigation strategies. Bull. Polish Acad. Sci. Tech. Sci. 69(4), e137724 (2021). https://doi.org/10.24425/bpasts.2021.137724
Killer, C., Stiller, B.: The swiss postal voting process and its system and security analysis. In: International Joint Conference on Electronic Voting, pp. 134–149. Springer, Cham (2019)
Kurpiewski, D., Jamroga, W., Knapik, M.L.: STV: model checking for strategies under imperfect information. In: Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2019, pp. 2372–2374. IFAAMAS (2019)
Kurpiewski, D., Pazderski, W., Jamroga, W., Kim, Y.: STV+Reductions: towards practical verification of strategic ability using model reductions. In: Proceedings of AAMAS, pp. 1770–1772. ACM (2021)
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). https://doi.org/10.1007/s10009-015-0378-x
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)
Martimiano, T., Santos, E.D., Olembo, M., Martina, J.: Ceremony analysis meets verifiable voting: individual verifiability in Helios. In: SECURWARE (2015)
McMillan, K.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers (1993)
McMillan, K.: Applying SAT methods in unbounded symbolic model checking. In: Proceedings of Computer Aided Verification (CAV). LNCS, vol. 2404, pp. 250–264 (2002)
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The tamarin prover for the symbolic analysis of security protocols. In: International Conference on Computer Aided Verification, pp. 696–701. Springer, Cham (2013)
Meng, B.: A critical review of receipt-freeness and coercion-resistance. Inf. Technol. J. 8(7), 934–964 (2009)
National Electoral Commission [Polish: Państwowa Komisja Wyborcza]: Presidential election 2020. [Polish: Wybory Prezydenta Rzeczypospolitej Polskiej 2020 r] (2020). https://prezydent20200628.pkw.gov.pl/prezydent20200628/pl
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
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56922-7_34
of the Republic of Poland, S.: Internet Legal Acts System [Polish: Internetowy System Aktów Prawnych] (2022). https://isap.sejm.gov.pl/isap.nsf/search.xsp?status=O&kw=wybory
Sempreboni, D., Vigano, L.: X-men: a mutation-based approach for the formal analysis of security ceremonies. In: 2020 IEEE European Symposium on Security and Privacy (EuroS &P), pp. 87–104. IEEE (2020)
Shoham, Y., Leyton-Brown, K.: Multiagent Systems - Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press (2009)
Skubiszewski, M.: Electoral Observatory to the President of the NEC: Incorrectly printed ballots abroad - need to address the problem [Polish: Obserwatorium Wyborcze do Przewodniczącego PKW: Nieprawidłowo wydrukowane karty do głosowania za granicą - konieczność rozwiązania problemu]. https://monitorkonstytucyjny.eu/archiwa/14355
Spotted-Lublin: Election 2020 ballot papers without red DEC seal [Polish: Wybory 2020. Karty do głosowania bez czerwonej pieczęci obwodowej komisji wyborczej]. https://spottedlublin.pl/wybory-2020-karty-do-glosowania-bez-czerwonej-pieczeci-obwodowej-komisji-wyborczej/
Tabatabaei, M., Jamroga, W., Ryan, P.Y.A.: Expressing receipt-freeness and coercion-resistance in logics of strategic ability: Preliminary attempt. In: Proceedings of the 1st International Workshop on AI for Privacy and Security, PrAISe@ECAI 2016, pp. 1:1–1:8. ACM (2016). https://doi.org/10.1145/2970030.2970039
