Automated game-theoretic security analysis of blockchain protocols
summary
Presents an automated pipeline that reduces game-theoretic security to SMT over real arithmetic, encodes incentive-compatibility and Byzantine-tolerance as satisfiability queries, and implements it as the tool Checkmate 2.0. Uses compositional, incremental analysis (player stratification + subtree divide-and-conquer) and piecewise precomputation to avoid generating huge trees. Claims soundness and completeness and demonstrates scaling from trillions of joint strategies to handling games with >1.44 million nodes; tic-tac-toe benchmark drops from nontermination/8h to 42s and a routing protocol from ~50min to ~5min via ~10,000 tiny SMT calls.
AI-written summary · about
chapters (8)
- 0:00Game-theoretic blockchain security
- 2:49Game-theoretic security analysis
- 3:53Game-theoretic models of protocols
- 7:27Security properties in game theory
- 9:58Automating analysis with Checkmate
- 12:28Compositional reasoning for scalability
- 16:22Experimental results and improvements
- 18:55Q&A
related talks
14mDivide and Conquer: A Compositional Approach to Game-Theoretic Security
46mSecurity Games: Key Algorithmic Principles, Deployed Applications and Research Challenges(*)
52mGame-Theoretically Secure Protocols Inspired by Blockchains
26mA formal security analysis of Blockchain voting
34mProvably Secure Blockchain Protocols and Applications to Secure Computation
58mAutomating Relational Verification of Infinite-State Programs
32mSymmetric Cryptanalysis I
05mInterview