Abstract
Selene is a recently proposed voting protocol that provides reasonable protection against coercion. In this paper, we make the first step towards a formalization of selected features of the protocol by means of formulae and models of multi-agent logics. We start with a very abstract view of the protocol as a public composition of a secret bijection from tracking numbers to voters and a secret mapping from voters to their choices. Then, we refine the view using multi-agent models of strategic interaction. The models define the space of strategies for the voters, the election authority, and the potential coercer. We express selected properties of the protocol using the strategic logic \(\mathbf {ATL_\mathrm {ir}}\), and conduct preliminary verification by model checking. While \(\mathbf {ATL_\mathrm {ir}}\) allows for intuitive specification of requirements like coercion-resistance, model checking of \(\mathbf {ATL_\mathrm {ir}}\) is notoriously hard. We show that some of the complexity can be avoided by using a recent approach of approximate model checking, based on fixpoint approximations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)
Belardinelli, F., Condurache, R., Dima, C., Jamroga, W., Jones, A.V.: Bisimulations for verification of strategic abilities with application to ThreeBallot voting protocol. In: Proceedings of AAMAS, pp. 1286–1295. IFAAMAS (2017)
Benaloh, J., Tuinstra, D.: Receipt-free secret-ballot elections. In: Proceedings of the 26th Annual ACM Symposium on Theory of Computing, pp. 544–553. ACM (1994)
Boureanu, I., Kouvaros, P., Lomuscio, A.: Verifying security properties in unbounded multiagent systems. In: Proceedings of AAMAS, pp. 1209–1217 (2016)
Bulling, N., Jamroga, W.: Alternating epistemic mu-calculus. In: Proceedings of IJCAI 2011, pp. 109–114 (2011)
Busard, S., Pecheur, C., Qu, H., Raimondi, F.: Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Inf. Comput. 242, 128–156 (2015)
Delaune, S., Kremer, S., Ryan, M.: Coercion-resistance and receipt-freeness in electronic voting. In: 19th IEEE Computer Security Foundations Workshop, p. 12-pp. IEEE (2006)
Dreier, J., Lafourcade, P., Lakhnech, Y.: A formal taxonomy of privacy in voting protocols. In: 2012 IEEE International Conference on Communications (ICC), pp. 6710–6715. IEEE (2012)
Jamroga, W., Dix, J.: Model checking ATL\(_{ir}\) is indeed \(\Delta _2^P\)-complete. In: Proceedings of EUMAS 2006. CEUR Workshop Proceedings, vol. 223. CEUR-WS.org (2006)
Jamroga, W., Knapik, M., Kurpiewski, D.: Fixpoint approximation of strategic abilities under imperfect information. In: Proceedings of AAMAS, pp. 1241–1249 (2017)
Jonker, H.L., Pieters, W.: Receipt-freeness as a special case of anonymity in epistemic logic. In: Proceedings of the 19th Computer Security Foundations Workshop, pp. 28–42 (2006)
Kusters, R., Truderung, T.: An epistemic approach to coercion-resistance for electronic voting protocols. In: Security and Privacy, pp. 251–266 (2009)
Küsters, R., Truderung, T., Vogt, A.: A game-based definition of coercion-resistance and its applications. In: 2010 23rd IEEE Computer Security Foundations Symposium, pp. 122–136. IEEE (2010)
Lang, S.: Algebra. Addison-Wesley, Boston (1993)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9–30 (2017)
Lomuscio, A., Penczek, W.: LDYIS: a framework for model checking security protocols. Fundamenta Informaticae 85(1–4), 359–375 (2008)
Meng, B.: A critical review of receipt-freeness and coercion-resistance. Inf. Technol. J. 8(7), 934–964 (2009)
Okamoto, T.: Receipt-free electronic voting schemes for large scale elections. In: Christianson, B., Crispo, B., Lomas, M., Roe, M. (eds.) Security Protocols 1997. LNCS, vol. 1361, pp. 25–35. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028157
Ryan, P.Y.A., Rønne, P.B., Iovino, V.: Selene: voting with transparent verifiability and coercion-mitigation. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 176–192. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53357-4_12
Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electron. Notes Theor. Comput. Sci. 85(2), 82–93 (2004)
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 PrAISe@ECAI Workshop, pp. 1:1–1:8. ACM (2016)
Acknowledgements
The authors acknowledge the support of the National Centre for Research and Development (NCBR), Poland, under the PolLux project VoteVerif (POLLUX-IV/1/2016).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Jamroga, W., Knapik, M., Kurpiewski, D. (2018). Model Checking the SELENE E-Voting Protocol in Multi-agent Logics. In: Krimmer, R., et al. Electronic Voting. E-Vote-ID 2018. Lecture Notes in Computer Science(), vol 11143. Springer, Cham. https://doi.org/10.1007/978-3-030-00419-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-00419-4_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00418-7
Online ISBN: 978-3-030-00419-4
eBook Packages: Computer ScienceComputer Science (R0)