Divide and Conquer - A Compositional Approach to Game-Theoretic Security

Explore a compositional approach to game-theoretic security analysis for decentralized systems like blockchains in this 14-minute conference presentation from OOPSLA 2025. Learn how researchers from TU Wien, Argot Collective, and University of Southampton tackle the scalability challenges of automated reasoning in static security analysis by proposing a divide-and-conquer methodology that breaks down complex game-theoretic models into manageable subgames. Discover how this approach addresses the critical need to certify that deviating from honest protocol behavior is not financially beneficial for users, ensuring economic security in decentralized protocols. Understand how game-theoretic security analysis can be encoded as automated reasoning problems in first-order real arithmetic theory, reducing complex game-theoretic reasoning to satisfiability modulo theories (SMT) problems. Examine the limitations of analyzing entire game-theoretic models as single SMT instances when dealing with protocols involving millions of interactions, and see how compositional reasoning provides a scalable solution. Gain insights into the incremental nature of this analysis, where changes to individual subgames only require re-analyzing ancestor nodes rather than the entire system, making it both sound and complete while maintaining effectiveness. Review experimental results demonstrating how this compositional approach successfully discovers intra-game properties and errors while scaling to games with millions of nodes, enabling comprehensive security analysis of large-scale protocols.