{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:51:17Z","timestamp":1762102277585,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030004187"},{"type":"electronic","value":"9783030004194"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00419-4_7","type":"book-chapter","created":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T05:35:09Z","timestamp":1536125709000},"page":"100-116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Model Checking the SELENE E-Voting Protocol in Multi-agent Logics"],"prefix":"10.1007","author":[{"given":"Wojciech","family":"Jamroga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michal","family":"Knapik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damian","family":"Kurpiewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,6]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"7_CR2","unstructured":"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\u20131295. IFAAMAS (2017)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Benaloh, J., Tuinstra, D.: Receipt-free secret-ballot elections. In: Proceedings of the 26th Annual ACM Symposium on Theory of Computing, pp. 544\u2013553. ACM (1994)","DOI":"10.1145\/195058.195407"},{"key":"7_CR4","unstructured":"Boureanu, I., Kouvaros, P., Lomuscio, A.: Verifying security properties in unbounded multiagent systems. In: Proceedings of AAMAS, pp. 1209\u20131217 (2016)"},{"key":"7_CR5","unstructured":"Bulling, N., Jamroga, W.: Alternating epistemic mu-calculus. In: Proceedings of IJCAI 2011, pp. 109\u2013114 (2011)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/j.ic.2015.03.014","volume":"242","author":"S Busard","year":"2015","unstructured":"Busard, S., Pecheur, C., Qu, H., Raimondi, F.: Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Inf. Comput. 242, 128\u2013156 (2015)","journal-title":"Inf. Comput."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/CSFW.2006.8"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Dreier, J., Lafourcade, P., Lakhnech, Y.: A formal taxonomy of privacy in voting protocols. In: 2012 IEEE International Conference on Communications (ICC), pp. 6710\u20136715. IEEE (2012)","DOI":"10.1109\/ICC.2012.6364938"},{"key":"7_CR9","unstructured":"Jamroga, W., Dix, J.: Model checking ATL$$_{ir}$$ir is indeed $$\\Delta _2^P$$\u03942P-complete. In: Proceedings of EUMAS 2006. CEUR Workshop Proceedings, vol. 223. CEUR-WS.org (2006)"},{"key":"7_CR10","unstructured":"Jamroga, W., Knapik, M., Kurpiewski, D.: Fixpoint approximation of strategic abilities under imperfect information. In: Proceedings of AAMAS, pp. 1241\u20131249 (2017)"},{"key":"7_CR11","unstructured":"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\u201342 (2006)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Kusters, R., Truderung, T.: An epistemic approach to coercion-resistance for electronic voting protocols. In: Security and Privacy, pp. 251\u2013266 (2009)","DOI":"10.1109\/SP.2009.13"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, 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\u2013136. IEEE (2010)","DOI":"10.1109\/CSF.2010.16"},{"key":"7_CR14","volume-title":"Algebra","author":"S Lang","year":"1993","unstructured":"Lang, S.: Algebra. Addison-Wesley, Boston (1993)"},{"issue":"1","key":"7_CR15","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"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\u201330 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1\u20134","key":"7_CR16","doi-asserted-by":"crossref","first-page":"359","DOI":"10.3233\/FUN-2008-851-425","volume":"85","author":"A Lomuscio","year":"2008","unstructured":"Lomuscio, A., Penczek, W.: LDYIS: a framework for model checking security protocols. Fundamenta Informaticae 85(1\u20134), 359\u2013375 (2008)","journal-title":"Fundamenta Informaticae"},{"issue":"7","key":"7_CR17","doi-asserted-by":"publisher","first-page":"934","DOI":"10.3923\/itj.2009.934.964","volume":"8","author":"B Meng","year":"2009","unstructured":"Meng, B.: A critical review of receipt-freeness and coercion-resistance. Inf. Technol. J. 8(7), 934\u2013964 (2009)","journal-title":"Inf. Technol. J."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BFb0028157","volume-title":"Security Protocols","author":"T Okamoto","year":"1998","unstructured":"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\u201335. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028157"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-662-53357-4_12","volume-title":"Financial Cryptography and Data Security","author":"PYA Ryan","year":"2016","unstructured":"Ryan, P.Y.A., R\u00f8nne, 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\u2013192. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53357-4_12"},{"issue":"2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/S1571-0661(05)82604-0","volume":"85","author":"PY Schobbens","year":"2004","unstructured":"Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electron. Notes Theor. Comput. Sci. 85(2), 82\u201393 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"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\u20131:8. ACM (2016)","DOI":"10.1145\/2970030.2970039"}],"container-title":["Lecture Notes in Computer Science","Electronic Voting"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00419-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T21:29:30Z","timestamp":1751837370000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00419-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030004187","9783030004194"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00419-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}