{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:42:24Z","timestamp":1743147744926,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030603465"},{"type":"electronic","value":"9783030603472"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-60347-2_9","type":"book-chapter","created":{"date-parts":[[2020,9,24]],"date-time":"2020-09-24T06:02:54Z","timestamp":1600927374000},"page":"129-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Towards Model Checking of Voting Protocols in Uppaal"],"prefix":"10.1007","author":[{"given":"Wojciech","family":"Jamroga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yan","family":"Kim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damian","family":"Kurpiewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter Y. A.","family":"Ryan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,25]]},"reference":[{"key":"9_CR1","unstructured":"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\u2013348 (2008)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-45741-3_13","volume-title":"Computer Security \u2013 ESORICS 2016","author":"M Arapinis","year":"2016","unstructured":"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\u2013260. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45741-3_13"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-38574-2_9","volume-title":"Automated Deduction \u2013 CADE-24","author":"B Beckert","year":"2013","unstructured":"Beckert, B., Gor\u00e9, R., Sch\u00fcrmann, C.: Analysing vote counting algorithms via logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 135\u2013144. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_9"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Beckert, B., Kirsten, M., Klebanov, V., Sch\u00fcrmann., 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\u201335. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-52240-1_2","DOI":"10.1007\/978-3-319-52240-1_2"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems: SFM-RT","author":"G Behrmann","year":"2004","unstructured":"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\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"9_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P., Huet, G., Paulin-Mohring, C.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"9_CR7","unstructured":"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\u20131217 (2016)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-319-68687-5_7","volume-title":"Electronic Voting","author":"A Bruni","year":"2017","unstructured":"Bruni, A., Drewsen, E., Sch\u00fcrmann, 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\u00fcrmann, C. (eds.) E-Vote-ID 2017. LNCS, vol. 10615, pp. 110\u2013126. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68687-5_7"},{"key":"9_CR9","unstructured":"Burton, C., et al.: Using Pr\u00eat \u00e0 Voter in Victoria state elections. In: Proceedings of EVT\/WOTE. USENIX (2012)"},{"issue":"4","key":"9_CR10","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/TIFS.2009.2034919","volume":"4","author":"D Chaum","year":"2009","unstructured":"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\u2013627 (2009)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"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\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Cortier, V., Galindo, D., K\u00fcsters, R., M\u00fcller, J., Truderung, T.: SoK: verifiability notions for e-voting protocols. In: IEEE Symposium on Security and Privacy, pp. 779\u2013798 (2016)","DOI":"10.1109\/SP.2016.52"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Czerwi\u0144ski, W., Lasota, S., Lazi\u0107, 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\u201333. Association for Computing Machinery (2019)","DOI":"10.1145\/3313276.3316369"},{"key":"9_CR14","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"EA Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995\u20131072. Elsevier, Amsterdam (1990)"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-030-00419-4_4","volume-title":"Electronic Voting","author":"MK Ghale","year":"2018","unstructured":"Ghale, M.K., Gor\u00e9, 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\u201366. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00419-4_4"},{"issue":"2","key":"9_CR17","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1023\/B:SYNT.0000024915.66183.d1","volume":"139","author":"V Goranko","year":"2004","unstructured":"Goranko, V., Jamroga, W.: Comparing semantics of logics for multi-agent systems. Synthese 139(2), 241\u2013280 (2004)","journal-title":"Synthese"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Haines, T., Gor\u00e9, R., Tiwari, M.: Verified verifiers for verifying elections. In: Proceedings of CCS, pp. 685\u2013702. ACM (2019)","DOI":"10.1145\/3319535.3354247"},{"key":"9_CR19","doi-asserted-by":"publisher","DOI":"10.1201\/9781315371290","volume-title":"Real-World Electronic Voting: Design, Analysis and Deployment","author":"F Hao","year":"2016","unstructured":"Hao, F., Ryan, P.Y.A.: Real-World Electronic Voting: Design, Analysis and Deployment, 1st edn. Auerbach Publications, Boca Raton (2016)","edition":"1"},{"key":"9_CR20","unstructured":"Jakobsson, M., Juels, A., Rivest, R.L.: Making mix nets robust for electronic voting by randomized partial checking. In: USENIX Security Symposium, pp. 339\u2013353 (2002)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-87805-6_10","volume-title":"Multiagent System Technologies","author":"W Jamroga","year":"2008","unstructured":"Jamroga, W.: Knowledge and strategic ability for model checking: a refined approach. In: Bergmann, R., Lindemann, G., Kirn, S., P\u011bchou\u010dek, M. (eds.) MATES 2008. LNCS (LNAI), vol. 5244, pp. 99\u2013110. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87805-6_10"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-030-00419-4_7","volume-title":"Electronic Voting","author":"W Jamroga","year":"2018","unstructured":"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\u2013116. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00419-4_7"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"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\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-12980-3_23","volume-title":"Attacking Paper-Based E2E Voting Systems","author":"J Kelsey","year":"2010","unstructured":"Kelsey, J., Regenscheid, A., Moran, T., Chaum, D.: Attacking Paper-Based E2E Voting Systems, pp. 370\u2013387. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12980-3_23"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-36095-4_8","volume-title":"Topics in Cryptology \u2013 CT-RSA 2013","author":"S Khazaei","year":"2013","unstructured":"Khazaei, S., Wikstr\u00f6m, D.: Randomized partial checking revisited. In: Dawson, E. (ed.) CT-RSA 2013. LNCS, vol. 7779, pp. 115\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36095-4_8"},{"issue":"1\u20134","key":"9_CR26","first-page":"359","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":"1","key":"9_CR27","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. Transfer. 19(1), 9\u201330 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transfer."},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"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\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"issue":"7","key":"9_CR29","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":"9_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-319-26350-2_41","volume-title":"AI 2015: Advances in Artificial Intelligence","author":"D Pattinson","year":"2015","unstructured":"Pattinson, D., Sch\u00fcrmann, C.: Vote counting as mathematical proof. In: Pfahringer, B., Renz, J. (eds.) AI 2015. LNCS (LNAI), vol. 9457, pp. 464\u2013475. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26350-2_41"},{"issue":"3","key":"9_CR31","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1109\/MSP.2015.54","volume":"13","author":"PYA Ryan","year":"2015","unstructured":"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\u201362 (2015)","journal-title":"IEEE Secur. Priv."},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-1-84882-736-3_5","volume-title":"Formal Methods: State of the Art and New Directions","author":"PYA Ryan","year":"2010","unstructured":"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\u2013184. Springer, London (2010). https:\/\/doi.org\/10.1007\/978-1-84882-736-3_5"},{"key":"9_CR33","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., et al. (eds.) Financial Cryptography and Data Security. Lecture Notes in Computer Science, vol. 9604, pp. 176\u2013192. Springer, Heidelberg (2016)"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-36213-2_15","volume-title":"Security Protocols XVII","author":"PYA Ryan","year":"2013","unstructured":"Ryan, P.Y.A., Teague, V.: Pretty good democracy. In: Christianson, B., Malcolm, J.A., Maty\u00e1\u0161, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol. 7028, pp. 111\u2013130. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36213-2_15"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-030-54455-3_22"}],"container-title":["Lecture Notes in Computer Science","Electronic Voting"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-60347-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,18]],"date-time":"2022-02-18T19:27:01Z","timestamp":1645212421000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-60347-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030603465","9783030603472"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-60347-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"25 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"E-Vote-ID","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Electronic Voting","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bregenz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"evoteid2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.e-vote-id.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}