Brugger, L. S., Kovács, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2023). CheckMate: Automated Game-Theoretic Security Reasoning. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 1407–1421). Association for Computing Machinery. https://doi.org/10.1145/3576915.3623183
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
CCS '23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
-
ISBN:
979-8-4007-0050-7
-
Date (published):
21-Nov-2023
-
Event name:
2023 ACM SIGSAC Conference on Computer and Communications Security
-
Event date:
26-Nov-2023 - 30-Nov-2023
-
Event place:
Copenhagen, Denmark
-
Number of Pages:
15
-
Publisher:
Association for Computing Machinery, New York
-
Keywords:
Automated Reasoning; Decentralized Protocols; Game Theory; Secure Protocols; Security Analysis
en
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.
en
Project title:
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 85 (FWF - Österr. Wissenschaftsfonds)
-
Project (external):
European Union (ERC)
-
Project ID:
101002685
-
Research Areas:
Logic and Computation: 40% Mathematical and Algorithmic Foundations: 30% Computer Science Foundations: 30%
CC BY 4.0
