Towards Model Checking of Voting Protocols in Uppaal

[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 :

Computer science

Author, co-author :

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)

External co-authors :

yes

Language :

English

Title :

Towards Model Checking of Voting Protocols in Uppaal

Publication date :

2020

Event name :

Fifth International Joint Conference on Electronic Voting E-VOTE-ID 2020

Event date :

6-9 Oct 2020

Main work title :

Proceedings of the Fifth International Joint Conference on Electronic Voting E-VOTE-ID 2020

Publisher :

Springer

Collection name :

Lecture Notes in Computer Science, vol. 12455

Peer reviewed :

Peer reviewed

Focus Area :

Security, Reliability and Trust

Additional URL :

https://arxiv.org/abs/2007.12412

FnR Project :

FNR12685695 - Socio-technical Verification Of Information Security And Trust In Voting Systems, 2018 (01/09/2019-31/08/2022) - Peter Y. A. Ryan

Available on ORBilu :

since 24 February 2021

Statistics

Number of views

186 (23 by Unilu)

Number of downloads

168 (6 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

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)
Hao, F., Ryan, P.Y.A.: Real-World Electronic Voting: Design, Analysis and Deployment, 1st edn. Auerbach Publications, Boca Raton (2016)
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
Khazaei, S., Wikström, D.: Randomized partial checking revisited. In: Dawson, E. (ed.) CT-RSA 2013. LNCS, vol. 7779, pp. 115–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36095-4_8
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)