{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:20:16Z","timestamp":1768000816119,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T00:00:00Z","timestamp":1700006400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101002685"],"award-info":[{"award-number":["101002685"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["F8504"],"award-info":[{"award-number":["F8504"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004729","name":"Technische Universit\u00e4t Wien","doi-asserted-by":"publisher","award":["SecInt Doctoral College"],"award-info":[{"award-number":["SecInt Doctoral College"]}],"id":[{"id":"10.13039\/501100004729","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,15]]},"DOI":"10.1145\/3576915.3623183","type":"proceedings-article","created":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T12:35:13Z","timestamp":1700570113000},"page":"1407-1421","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["CheckMate: Automated Game-Theoretic Security Reasoning"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8770-4112","authenticated-orcid":false,"given":"Lea Salome","family":"Brugger","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7203-6641","authenticated-orcid":false,"given":"Anja","family":"Petkovic Komel","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8940-4989","authenticated-orcid":false,"given":"Sophie","family":"Rain","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Gilad Asharov and Yehuda Lindell. 2009. Utility Dependence in Correct and Fair Rational Secret Sharing. Cryptology ePrint Archive. https:\/\/eprint.iacr.org\/2009\/373","DOI":"10.1007\/978-3-642-03356-8_33"},{"key":"e_1_3_2_1_2_1","volume-title":"Handbook of Model Checking","author":"Barrett Clark","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories. In Handbook of Model Checking. Springer, UC Berkeley, 305--343."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_3"},{"key":"e_1_3_2_1_4_1","volume-title":"Sophie Rain, and Michael Rawson. EasyChair","author":"Brugger Lea Salome","year":"2023","unstructured":"Lea Salome Brugger, Laura Kov\u00e1cs, Anja Petkovi\u0107 Komel, Sophie Rain, and Michael Rawson. EasyChair, 2023. CheckMate: Automated Game-Theoretic Security Reasoning. EasyChair Preprint no. 10853."},{"key":"e_1_3_2_1_5_1","volume-title":"Probabilistic Smart Contracts: Secure Randomness on the Blockchain. In 2019 IEEE International Conference on Blockchain and Cryptocurrency (ICBC). IEEE","author":"Chatterjee Krishnendu","year":"2019","unstructured":"Krishnendu Chatterjee, Amir Goharshady, and Arash Pourdamghani. 2019. Probabilistic Smart Contracts: Secure Randomness on the Blockchain. In 2019 IEEE International Conference on Blockchain and Cryptocurrency (ICBC). IEEE, Seoul, South Korea, 403--412."},{"key":"e_1_3_2_1_6_1","volume-title":"Automata Theory and Formal Languages","author":"Collins George E","unstructured":"George E Collins. 1975. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decompostion. In Automata Theory and Formal Languages. Springer, Berlin, Heidelberg, 134--183."},{"key":"e_1_3_2_1_7_1","volume-title":"Z3: An Efficient SMT Solver","author":"Moura Leonardo De","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. Springer, Berlin, Heidelberg, 337--340."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3057268"},{"key":"e_1_3_2_1_9_1","volume-title":"A Fast Linear-Arithmetic Solver for DPLL (T)","author":"Dutertre Bruno","unstructured":"Bruno Dutertre and Leonardo De Moura. 2006. A Fast Linear-Arithmetic Solver for DPLL (T). In CAV. Springer, Berlin, Heidelberg, 81--94."},{"key":"e_1_3_2_1_10_1","volume-title":"Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories","author":"Ge Yeting","unstructured":"Yeting Ge and Leonardo De Moura. 2009. Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories. In CAV. Springer, Berlin, Heidelberg, 306--320."},{"key":"e_1_3_2_1_11_1","unstructured":"Neil Ghani Jules Hedges Viktor Winschel and Philipp Zahn. 2016. Compositional Game Theory. arxiv.org\/abs\/1603.04641"},{"key":"e_1_3_2_1_12_1","volume-title":"Theory of Cryptography","author":"Gradwohl Ronen","unstructured":"Ronen Gradwohl. 2010. Rationality in the full-information model. In Theory of Cryptography. Springer, Berlin, Heidelberg, 401--418."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2399187.2399189"},{"key":"e_1_3_2_1_14_1","first-page":"2017","article-title":"The JSON data interchange syntax","volume":"21778","author":"ISO.","year":"2017","unstructured":"ISO. 2017. The JSON data interchange syntax. ISO 21778:2017. International Organization for Standardization, Geneva, Switzerland.","journal-title":"ISO"},{"key":"e_1_3_2_1_15_1","volume-title":"Rational Secure Computation and Ideal Mechanism Design","author":"Izmalkov Sergei","unstructured":"Sergei Izmalkov, Silvio Micali, and Matt Lepinski. 2005. Rational Secure Computation and Ideal Mechanism Design. In FOCS. IEEE, Pittsburgh, 585--594."},{"key":"e_1_3_2_1_16_1","volume-title":"Solving Non-Linear Arithmetic","author":"Jovanovi\u0107 Dejan","unstructured":"Dejan Jovanovi\u0107 and Leonardo De Moura. 2012. Solving Non-Linear Arithmetic. In IJCAR. Springer, Manchester, 339--354."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3411495.3421365"},{"key":"e_1_3_2_1_18_1","volume-title":"Stochastic Game Verification with Concurrency, Equilibria and Time","author":"Kwiatkowska Marta","unstructured":"Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos. 2020. PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. In CAV. Springer International Publishing, Cham, 475--487."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00356-y"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-015-9183-0"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2909924"},{"key":"e_1_3_2_1_22_1","volume-title":"Rationality and Adversarial Behavior in Multi-Party Computation. In Annual International Cryptology Conference. Springer","author":"Lysyanskaya Anna","year":"2006","unstructured":"Anna Lysyanskaya and Nikos Triandopoulos. 2006. Rationality and Adversarial Behavior in Multi-Party Computation. In Annual International Cryptology Conference. Springer, Berlin, Heidelberg, 180--197."},{"key":"e_1_3_2_1_23_1","volume-title":"Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability. In Network and Distributed System Security Symposium. The Internet Society","author":"Malavolta Giulio","year":"2019","unstructured":"Giulio Malavolta, Pedro Moreno-Sanchez, Clara Schneidewind, Aniket Kate, and Matteo Maffei. 2019. Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability. In Network and Distributed System Security Symposium. The Internet Society, San Diego, CA, USA."},{"key":"e_1_3_2_1_24_1","unstructured":"Subhra Mazumdar Prabal Banerjee Abhinandan Sinha Sushmita Ruj and Bimal Roy. 2022. Strategic Analysis to Defend against Griefing Attack in Lightning Network. arxiv.org\/abs\/2203.10533"},{"key":"e_1_3_2_1_25_1","volume-title":"Gambit: Software Tools for Game Theory.","author":"Mckelvey Richard","year":"2005","unstructured":"Richard Mckelvey, Andrew McLennan, and Theodore Turocy. 2005. Gambit: Software Tools for Game Theory."},{"key":"e_1_3_2_1_26_1","volume-title":"The TAMARIN Prover for the Symbolic Analysis of Security Protocols","author":"Meier Simon","unstructured":"Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In CAV. Springer, Berlin, Heidelberg, 696--701."},{"key":"e_1_3_2_1_27_1","volume-title":"Bitcoin: A Peer-to-Peer Electronic Cash System.","author":"Nakamoto Satoshi","year":"2009","unstructured":"Satoshi Nakamoto. 2009. Bitcoin: A Peer-to-Peer Electronic Cash System."},{"key":"e_1_3_2_1_28_1","volume-title":"Information and Communication Technology","author":"Nguyen Van-Hau","unstructured":"Van-Hau Nguyen and Son T Mai. 2015. A New Method to Encode the At-Most-One Constraint into SAT. In Information and Communication Technology. ACM, New York, NY, USA, 46--53."},{"key":"e_1_3_2_1_29_1","volume-title":"Osborne and Ariel Rubinstein","author":"Martin","year":"1994","unstructured":"Martin J. Osborne and Ariel Rubinstein. 1994. A Course in Game Theory. The MIT Press, Cambridge, USA."},{"key":"e_1_3_2_1_30_1","unstructured":"Joseph Poon and Thaddeus Dryja. 2016. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. https:\/\/lightning.network\/lightning-network-paper.pdf."},{"key":"e_1_3_2_1_31_1","volume-title":"Towards a Game-Theoretic Security Analysis of Off-Chain Protocols","author":"Rain Sophie","unstructured":"Sophie Rain, Georgia Avarikioti, Laura Kov\u00e1cs, and Matteo Maffei. 2023. Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. In CSF. IEEE Computer Society, Los Alamitos, CA, USA, 31--46."},{"key":"e_1_3_2_1_32_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","unstructured":"Alexander Schrijver. 1999. Theory of Linear and Integer Programming. Wiley, Hoboken, New Jersey, USA."},{"key":"e_1_3_2_1_33_1","volume-title":"First-Order Logic","author":"Smullyan Raymond M","unstructured":"Raymond M Smullyan. 1995. First-Order Logic. Dover Publications, New York."},{"key":"e_1_3_2_1_34_1","volume-title":"Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain","author":"Wang Yuepeng","unstructured":"Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, and Kostas Ferles. 2019. Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. In VSTTE. Springer International Publishing, Cham, 87--106."},{"key":"e_1_3_2_1_35_1","volume-title":"Ethereum: A Secure Decentralised Generalised Transaction Ledger. https:\/\/gavwood.com\/paper.pdf","author":"Wood Gavin","year":"2014","unstructured":"Gavin Wood. 2014. Ethereum: A Secure Decentralised Generalised Transaction Ledger. https:\/\/gavwood.com\/paper.pdf"},{"key":"e_1_3_2_1_36_1","unstructured":"Paolo Zappal\u00e0 Marianna Belotti Maria Potop-Butucaru and Stefano Secci. 2021. Game Theoretical Framework for Analyzing Blockchains Robustness. 18 pages."}],"event":{"name":"CCS '23: ACM SIGSAC Conference on Computer and Communications Security","location":"Copenhagen Denmark","acronym":"CCS '23","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623183","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576915.3623183","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T01:46:20Z","timestamp":1755740780000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623183"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,15]]},"references-count":36,"alternative-id":["10.1145\/3576915.3623183","10.1145\/3576915"],"URL":"https:\/\/doi.org\/10.1145\/3576915.3623183","relation":{},"subject":[],"published":{"date-parts":[[2023,11,15]]},"assertion":[{"value":"2023-11-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}