{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:22:19Z","timestamp":1760059339523,"version":"build-2065373602"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","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":["10.55776\/F85"],"award-info":[{"award-number":["10.55776\/F85"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["10.47379\/ICT22007"],"award-info":[{"award-number":["10.47379\/ICT22007"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004729","name":"Technische Universit\u00e4t Wien","doi-asserted-by":"publisher","award":["Doctoral College SecInt"],"award-info":[{"award-number":["Doctoral College SecInt"]}],"id":[{"id":"10.13039\/501100004729","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>We propose a compositional approach to combine and scale automated reasoning in the static analysis of decentralized system security, such as blockchains. Our focus lies in the game-theoretic security analysis of such systems, allowing us to examine economic incentives behind user actions. In this context, it is particularly important to certify that deviating from the intended, honest behavior of the decentralized protocol is not beneficial: as long as users follow the protocol, they cannot be financially harmed, regardless of how others behave. Such an economic analysis of blockchain protocols can be encoded as an automated reasoning problem in the first-order theory of real arithmetic, reducing game-theoretic reasoning to satisfiability modulo theories (SMT). However, analyzing an entire game-theoretic model (called a game) as a single SMT instance does not scale to protocols with millions of interactions. We address this challenge and propose a divide-and-conquer  \nsecurity analysis based on compositional reasoning over games. Our compositional analysis is incremental: we divide games into subgames such that changes to one subgame do not necessitate re-analyzing the entire game, but only the ancestor nodes. Our approach is sound, complete, and effective: combining the security properties of subgames yields security of the entire game. Experimental results show that compositional reasoning discovers intra-game properties and errors while scaling to games with millions of nodes, enabling security analysis of large protocols.<\/jats:p>","DOI":"10.1145\/3763120","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1949-1973","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Divide and Conquer: A Compositional Approach to Game-Theoretic Security"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9984-995X","authenticated-orcid":false,"given":"Ivana","family":"Bocevska","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7203-6641","authenticated-orcid":false,"given":"Anja","family":"Petkovi\u0107 Komel","sequence":"additional","affiliation":[{"name":"Argot Collective, Zug, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8940-4989","authenticated-orcid":false,"given":"Sophie","family":"Rain","sequence":"additional","affiliation":[{"name":"Argot Collective, Zug, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[{"name":"University of Southampton, Southampton, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/978-3-319-10575-8_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1007\/978-3-031-65627-9_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1145\/3276514"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/978-3-319-10082-1_3"},{"key":"e_1_2_1_5_1","volume-title":"Laura Kov\u00e1cs, Sophie Rain, and Michael Rawson.","author":"Bocevska Ivana","year":"2025","unstructured":"Ivana Bocevska, Anja Petkovi\u0107 Komel, Laura Kov\u00e1cs, Sophie Rain, and Michael Rawson. 2025. Divide and Conquer: a Compositional Approach to Game-Theoretic Security. EasyChair Preprint 15785,. https:\/\/easychair.org\/publications\/preprint\/kxKK"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.5281\/zenodo.15725152"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.32408\/compositionality-5-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1145\/3576915.3623183"},{"volume-title":"A Next Generation Smart Contract & Decentralized Application Platform","author":"Buterin Vitalik","unstructured":"Vitalik Buterin. 2014. A Next Generation Smart Contract & Decentralized Application Platform. Ethereum Foundation. https:\/\/ethereum.org\/en\/whitepaper\/","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/3209108.3209165"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.4204\/eptcs.323.7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/3411495.3421365"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_2_1_14_1","volume-title":"Bitcoin: A Peer-to-Peer Electronic Cash System. https:\/\/bitcoin.org\/en\/bitcoin-paper","author":"Nakamoto Satoshi","year":"2009","unstructured":"Satoshi Nakamoto. 2009. Bitcoin: A Peer-to-Peer Electronic Cash System. https:\/\/bitcoin.org\/en\/bitcoin-paper"},{"key":"e_1_2_1_15_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. isbn:9780262650403 lccn:94008308"},{"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_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1109\/CSF57540.2023.00003"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.29007\/llnq"},{"volume-title":"First-Order Logic","author":"Smullyan Raymond M","unstructured":"Raymond M Smullyan. 1995. First-Order Logic. Dover Publications, New York.","key":"e_1_2_1_19_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1007\/978-3-030-41600-3_7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1007\/978-3-030-88806-0_21"},{"volume-title":"Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. 4, TU Wien Academic Press","author":"Wilson Amalee","unstructured":"Amalee Wilson, Andres N\u00f6tzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, and Clark W. Barrett. 2023. Partitioning Strategies for Distributed SMT Solving. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. 4, TU Wien Academic Press, Vienna, Austria. 199\u2013208. https:\/\/api.semanticscholar.org\/CorpusID:259129858","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","volume-title":"Maria Gradinariu Potop-Butucaru, and Stefano Secci","author":"Zappal\u00e0 Paolo","year":"2020","unstructured":"Paolo Zappal\u00e0, Marianna Belotti, Maria Gradinariu Potop-Butucaru, and Stefano Secci. 2020. Game theoretical framework for analyzing Blockchains Robustness. https:\/\/api.semanticscholar.org\/CorpusID:219616790"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:50:11Z","timestamp":1760032211000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763120"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":23,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763120"],"URL":"https:\/\/doi.org\/10.1145\/3763120","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}