Divide and Conquer: A Compositional Approach to Game-Theoretic Security
summary
Compositional pipeline reduces game-theoretic blockchain security checks to many small SMT queries instead of one huge one, encoding incentives in first-order real arithmetic and automating strategy/counterexample extraction. Prototype Checkmate 2.0 is sound and complete, splits games into 1,400 subtrees and performs >10,000 compact SMT calls, scales to millions of nodes, cuts tic‑tac‑toe from timeout to 42 seconds and a Lightning routing counterexample extraction from 50 minutes to 5.
AI-written summary · about
chapters (12)
- 0:00Game-theoretic security intro
- 1:04Game-theoretic models
- 2:49Security properties analysis
- 3:52Scalability challenges
- 4:13Compositional approach with Checkmate 2.0
- 5:18Divide and conquer subtrees
- 6:44Player-wise iteration
- 7:28Benchmark results
- 8:32Subgame and supergame reasoning
- 9:57Four-player routing protocol
- 10:58Scalability improvements summary
- 11:40Q&A
related talks
24mAutomated game-theoretic security analysis of blockchain protocols
46mSecurity Games: Key Algorithmic Principles, Deployed Applications and Research Challenges(*)
52mGame-Theoretically Secure Protocols Inspired by Blockchains
27mUniversally Composable Security for Program Partitioning
16mDesigning Holistic Security Programs
44mModular Approach to Cloud Security
31mSequential Composition of Rational Proofs
34mProvably Secure Blockchain Protocols and Applications to Secure Computation