{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:01:03Z","timestamp":1767999663899,"version":"3.49.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-10794-7_18","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:30Z","timestamp":1763189010000},"page":"359-377","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Game Modeling of\u00a0Blockchain Protocols"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8940-4989","authenticated-orcid":false,"given":"Sophie","family":"Rain","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7203-6641","authenticated-orcid":false,"given":"Anja","family":"Petkovi\u0107 Komel","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-10082-1_3","volume-title":"Foundations of Security Analysis and Design VII","author":"B Blanchet","year":"2014","unstructured":"Blanchet, B.: Automatic verification of security protocols in the symbolic model: the verifier ProVerif. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 54\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_3"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Brugger, L.S., Kov\u00e1cs, L., Petkovic\u00a0Komel, A., Rain, S., Rawson, M.: CheckMate: automated game-theoretic security reasoning. In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201923, pp. 1407\u20131421. Association for Computing Machinery, New York (2023).https:\/\/doi.org\/10.1145\/3576915.3623183","DOI":"10.1145\/3576915.3623183"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"221","DOI":"10.4204\/eptcs.372.16","volume":"372","author":"M Capucci","year":"2022","unstructured":"Capucci, M., Ghani, N., Ledent, J., Nordvall Forsberg, F.: Translating extensive form games to open games with agency. Electron. Proc. Theor. Comput. Sci. 372, 221\u2013234 (2022). https:\/\/doi.org\/10.4204\/eptcs.372.16","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"18_CR4","unstructured":"Nandi, C., Mooly\u00a0Sagiv, D.J.: Certora Technology White Paper: Unveiling the Power and Limitations of Certora\u2019s Smart Contract Verification Technology. https:\/\/www.certora.com\/blog\/white-paper"},{"key":"18_CR5","unstructured":"Cheung, Y.K., Leonardos, S., Piliouras, G., Sridhar, S.: From griefing to stability in blockchain mining economies (2021). https:\/\/arxiv.org\/abs\/2106.12332"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Dxo, Soos, M., Paraskevopoulou, Z., Lundfall, M., Brockman, M.: Hevm, a fast symbolic execution framework for evm bytecode. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 453\u2013465. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_22","DOI":"10.1007\/978-3-031-65627-9_22"},{"key":"18_CR7","unstructured":"FAssets. https:\/\/dev.flare.network\/fassets\/overview\/"},{"key":"18_CR8","unstructured":"Flare: The Blockchain for Data. https:\/\/flare.network\/"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Fooladgar, M., Manshaei, M.H., Jadliwala, M., Rahman, M.A.: On incentive compatible role-based reward distribution in algorand. In: 2020 50th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 452\u2013463 (2020). https:\/\/doi.org\/10.1109\/DSN48063.2020.00059","DOI":"10.1109\/DSN48063.2020.00059"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Ghani, N., Hedges, J., Winschel, V., Zahn, P.: Compositional game theory. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201918, pp. 472\u2013481. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3209108.3209165","DOI":"10.1145\/3209108.3209165"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Ghani, N., Kupke, C., Lambert, A., Nordvall Forsberg, F.: Compositional game theory with mixed strategies: probabilistic open games using a distributive law. Electron. Proc. Theor. Comput. Sci. 323, 95\u2013105 (2020). https:\/\/doi.org\/10.4204\/eptcs.323.7","DOI":"10.4204\/eptcs.323.7"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Holler, S., Biewer, S., Schneidewind, C.: Horstify: sound security analysis of smart contracts. In: 36th IEEE Computer Security Foundations Symposium, CSF 2023, Dubrovnik, Croatia, 10\u201314 July 2023, pp. 245\u2013260. IEEE (2023). https:\/\/doi.org\/10.1109\/CSF57540.2023.00023","DOI":"10.1109\/CSF57540.2023.00023"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Kobeissi, N., Nicolas, G., Tiwari, M.: Verifpal: cryptographic protocol analysis for the real world. In: Proceedings of the 2020 ACM SIGSAC Conference on Cloud Computing Security Workshop, CCSW\u201920, p.\u00a0159. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3411495.3421365","DOI":"10.1145\/3411495.3421365"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-53291-8_25","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Malavolta, G., Moreno-Sanchez, P., Schneidewind, C., Kate, A., Maffei, M.: Anonymous multi-hop locks for blockchain scalability and interoperability. In: Network and Distributed System Security Symposium. The Internet Society, San Diego (2019)","DOI":"10.14722\/ndss.2019.23330"},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"78100","DOI":"10.1109\/ACCESS.2018.2884764","volume":"6","author":"MH Manshaei","year":"2018","unstructured":"Manshaei, M.H., Jadliwala, M., Maiti, A., Fooladgar, M.: A game-theoretic analysis of shard-based permissionless blockchains. IEEE Access 6, 78100\u201378112 (2018). https:\/\/doi.org\/10.1109\/ACCESS.2018.2884764","journal-title":"IEEE Access"},{"issue":"2","key":"18_CR17","doi-asserted-by":"publisher","first-page":"1790","DOI":"10.1109\/tnsm.2022.3230768","volume":"20","author":"S Mazumdar","year":"2023","unstructured":"Mazumdar, S., Banerjee, P., Sinha, A., Ruj, S., Roy, B.K.: Strategic analysis of griefing attack in lightning network. IEEE Trans. Netw. Serv. Manag. 20(2), 1790\u20131803 (2023). https:\/\/doi.org\/10.1109\/tnsm.2022.3230768","journal-title":"IEEE Trans. Netw. Serv. Manag."},{"key":"18_CR18","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"},{"key":"18_CR19","unstructured":"Poon, J., Dryja, T.: The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. white paper (2016). https:\/\/lightning.network\/lightning-network-paper.pdf"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Rain, S., Avarikioti, G., Kov\u00e1cs, L., Maffei, M.: Towards a game-theoretic security analysis of off-chain protocols. In: 2023 IEEE 36th Computer Security Foundations Symposium (CSF), pp. 107\u2013122. IEEE Computer Society, Los Alamitos (2023).https:\/\/doi.org\/10.1109\/CSF57540.2023.00003","DOI":"10.1109\/CSF57540.2023.00003"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Rain, S., Brugger, L.S., Komel, A.P., Kov\u00e1cs, L., Rawson, M.: Scaling checkmate for game-theoretic security. In: Bj\u00f8rner, N., Heule, M., Voronkov, A. (eds.) Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a0100, pp. 222\u2013231. EasyChair, Stockport (2024). https:\/\/doi.org\/10.29007\/llnq","DOI":"10.29007\/llnq"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Rain, S., Komel, A.P., Rawson, M., Kov\u00e1cs, L.: Game Modeling of Blockchain Protocols \u2013 Artifact (2025). https:\/\/zenodo.org\/records\/16925288","DOI":"10.1007\/978-3-032-10794-7_18"},{"issue":"5","key":"18_CR23","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1038\/scientificamerican0599-98","volume":"280","author":"I Stewart","year":"1999","unstructured":"Stewart, I.: A puzzle for pirates. Sci. Am. 280(5), 98\u201399 (1999)","journal-title":"Sci. Am."},{"issue":"2","key":"18_CR24","doi-asserted-by":"publisher","first-page":"2708","DOI":"10.1109\/JSYST.2020.3004468","volume":"15","author":"T Wang","year":"2021","unstructured":"Wang, T., Bai, X., Wang, H., Liew, S.C., Zhang, S.: Game-theoretical analysis of mining strategy for bitcoin-ng blockchain protocol. IEEE Syst. J. 15(2), 2708\u20132719 (2021). https:\/\/doi.org\/10.1109\/JSYST.2020.3004468","journal-title":"IEEE Syst. J."},{"key":"18_CR25","unstructured":"Zappal\u00e0, P., Belotti, M., Potop-Butucaru, M.G., Secci, S.: Game theoretical framework for analyzing Blockchains Robustness. IACR Cryptol. ePrint Arch. 2020 (2020). https:\/\/api.semanticscholar.org\/CorpusID:219616790"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:30Z","timestamp":1767967170000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}