Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Scaling CheckMate for Game-Theoretic Security

Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovacs, Michael Rawson

TL;DR

CheckMate addresses the need to verify game-theoretic security in decentralized protocols by modeling protocol behavior as extensive-form games and encoding security properties into SMT constraints over real arithmetic. It supports $wi$, $weri$, $cr$, and $pr$ via an iterative case-splitting solver built in C++ and interfaced with Z3, enabling extraction of strategies, counterexamples, and weakest preconditions. The tool accepts a rich JSON encoding of the EFG and honest histories, and it outputs concrete results and diagnostic artifacts that guide protocol redesign. On a benchmark suite of 15 examples, including blockchain protocols, CheckMate demonstrates scalable verification and practical insights into economic incentives and potential attack vectors.

Abstract

We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate's input format and its various components, modes, and output. CheckMate is evaluated on 15 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.

Scaling CheckMate for Game-Theoretic Security

TL;DR

CheckMate addresses the need to verify game-theoretic security in decentralized protocols by modeling protocol behavior as extensive-form games and encoding security properties into SMT constraints over real arithmetic. It supports , , , and via an iterative case-splitting solver built in C++ and interfaced with Z3, enabling extraction of strategies, counterexamples, and weakest preconditions. The tool accepts a rich JSON encoding of the EFG and honest histories, and it outputs concrete results and diagnostic artifacts that guide protocol redesign. On a benchmark suite of 15 examples, including blockchain protocols, CheckMate demonstrates scalable verification and practical insights into economic incentives and potential attack vectors.

Abstract

We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate's input format and its various components, modes, and output. CheckMate is evaluated on 15 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.
Paper Structure (16 sections, 2 equations, 4 figures, 1 table)

This paper contains 16 sections, 2 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Structure and Components
  3. Pipeline.
  4. CheckMate Input
  5. CheckMate Formulas.
  6. Example (EFG in JSON format).
  7. CheckMate Output
  8. Case Splitting in CheckMate
  9. Strategy Extraction
  10. Counterexamples
  11. Weakest Preconditions
  12. Usage
  13. Evaluation
  14. Experimental Analysis.
  15. Related Work and Conclusion
  16. ...and 1 more sections

Figures (4)

  • Figure 1: The CheckMate pipeline.
  • Figure 2: Game $G$ with $a>0$, honest history $(r_A, l_B)$.
  • Figure 3: CheckMate input encoding \ref{['fig:running-example']}.
  • Figure 4: CheckMate output for analyzing the weak immunity of the EFG of \ref{['fig:game-g-json']}, with counterexample and weakest precondition generation.