Record link: 
http://hdl.handle.net/20.500.12708/226091
-
Title: 
Game Modeling of Blockchain Protocols
en
Citation: 
Rain, S., Petković Komel, A., Rawson, M., & Kovacs, L. (2025). Game Modeling of Blockchain Protocols. In F. Damiani & M. Farrell (Eds.), Integrated Formal Methods : 20th International Conference, iFM 2025, Paris, France, November 19–21, 2025, Proceedings (pp. 359–377). Springer. https://doi.org/10.1007/978-3-032-10794-7_18
-
Publisher DOI: 
10.1007/978-3-032-10794-7_18
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Rain, Sophie 
Petković Komel, Anja 
Rawson, Michael 
Kovacs, Laura 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies 
E056-13 - Fachbereich LogiCS 
E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems 
E056-26 - Fachbereich Automated Reasoning 
-
Published in: 
Integrated Formal Methods : 20th International Conference, iFM 2025, Paris, France, November 19–21, 2025, Proceedings 
-
ISBN: 
978-3-032-10794-7
-
Volume: 
16194
-
DOI of the book: 
10.1007/978-3-032-10794-7
-
Date (published): 
15-Nov-2025
-
Event name: 
20th International Conference on Integrated Formal Methods (iFM 2025) 
en
Event date: 
19-Nov-2025 - 21-Nov-2025
-
Event place: 
Paris, France
-
Number of Pages: 
19
-
Publisher: 
Springer, Cham
-
Peer reviewed: 
Yes
-
Keywords: 
Formal Methods; Game Theory; Modeling Template; Protocol Modeling
en
Abstract: 
Reasoning about incentives in a blockchain protocol can be captured by game-theoretic modeling. We present modeling principles sufficient to create a faithful representation of a blockchain protocol as an extensive form game. Such games are then suitable for automatically establishing game-theoretic security. We showcase the semi-automated generation of the game models for two parts of Bitcoin’s Lightning protocol: the closing of a channel and the routing of a payment along channels. Additionally, we provide a domain-specific language, which eases the implementation of the games. We believe our modeling principles and guidelines strengthen machine-supported modeling practices.
en
Project title: 
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) 
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8500 (FWF - Österr. Wissenschaftsfonds) 
Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) 
-
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 100%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

11
checked on Feb 9, 2026

Google ScholarTM

Check