CheckMate: Automated Game-Theoretic Security Reasoning

EasyChair Preprint 10853

Abstract

We present the CheckMate framework for full automation of game-theoretic security analysis, with particular focus on blockchain technologies. CheckMate analyzes protocols modeled as games for their game-theoretic security — that is, for incentive compatibility and Byzantine fault-tolerance. The framework either proves the protocols secure by providing defense strategies or yields all possible attack vectors. For protocols that are not secure, CheckMate can also provide weakest preconditions under which the protocol becomes secure, if they exist. CheckMate implements a sound and complete encoding of game-theoretic security in first-order linear real arithmetic, thereby reducing security analysis to satisfiability solving. CheckMate further automates efficient handling of case splitting on arithmetic terms. Experiments show CheckMate scales, analyzing games with trillions of strategies that model phases of Bitcoin’s Lightning Network.
This work is the extended version of our CCS 2023 paper “CheckMate: Automated Game-Theoretic Security Reasoning"

Keyphrases: Decentralized Protocols, Secure Protocols, automated reasoning, game theory, security analysis

@booklet{EasyChair:10853,
  author    = {Lea Salome Brugger and Laura Kovács and Anja Petković Komel and Sophie Rain and Michael Rawson},
  title     = {CheckMate: Automated Game-Theoretic Security Reasoning},
  howpublished = {EasyChair Preprint 10853},
  year      = {EasyChair, 2023}}