Game Modeling of Blockchain Protocols

EasyChair Preprint 16006

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.

Keyphrases: Modeling Template, Protocol Modeling, formal models, game theory

@booklet{EasyChair:16006,
  author    = {Sophie Rain and Anja Petković Komel and Michael Rawson and Laura Kovács},
  title     = {Game Modeling of Blockchain Protocols},
  howpublished = {EasyChair Preprint 16006},
  year      = {EasyChair, 2025}}