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 14 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.

翻译：我们提出CheckMate工具，用于自动验证博弈论安全属性，并应用于区块链协议。CheckMate采用自动推理技术，判定博弈论协议模型是否具备博弈论安全性，即拜占庭容错与激励兼容性。我们阐述了CheckMate的输入格式、各组件、运行模式及输出。通过14个基准测试对CheckMate进行评估，涵盖去中心化协议模型、棋类游戏及博弈论示例。