Divide and Conquer: a Compositional Approach to Game-Theoretic Security

EasyChair Preprint 15785

Abstract

Game-theoretic security analysis of decentralized systems examines economic incentives behind user actions. It is particularly important to certify that deviating from the intended, honest behavior of the protocol is not beneficial: as long as users follow 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 tree as a single SMT instance does not scale to security properties with millions of interactions. We address this challenge and propose a divide-and-conquer security analysis based on compositional reasoning over game trees. 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 game trees with millions of nodes, enabling security analysis of large protocols.

Keyphrases: SMT solving, Security, automated reasoning, game theory

@booklet{EasyChair:15785,
  author    = {Ivana Bocevska and Anja Petković Komel and Laura Kovács and Sophie Rain and Michael Rawson},
  title     = {Divide and Conquer: a Compositional Approach to Game-Theoretic Security},
  howpublished = {EasyChair Preprint 15785},
  year      = {EasyChair, 2025}}