Extending game-theoretic security of blockchain protocols with compositional reasoning and conditional actions

Abstract

Game-theoretic security analysis of blockchain technologies has proven highly valuable. Such analysis examines protocols from an economic perspective, specifically by exploring the economic incentives that drive user behavior. Thus, it ensures that deviating from the intended, honest behavior of a protocol is not financially beneficial: as long as users follow the protocol, they cannot be financially harmed, regardless of how others behave.Such an economic analysis of blockchain protocols can be encoded as an automated reasoning problem in the first-order theory of real arithmetic, thereby reducing game-theoretic reasoning to satisfiability modulo theories (SMT) solving. However, existing frameworks face significant challenges in terms of scalability and expressivity. The scalability issue arises because current approaches treat the entire game tree, potentially involving millions of interactions, as a single SMT instance. In terms of expressivity, existing frameworks fall short in modeling and analyzing games that involve external factors - such as price fluctuations or exchange rates of currencies - that depend on the current world state and lie beyond the players' control.Therefore, to address these challenges, we propose a divide-and-conquer security analysis based on compositional reasoning over game trees. In our approach, we decompose games into subgames, ensuring that changes to one subgame do not require re-analyzing the entire game, but only its ancestor nodes. We provide a sound and complete automation of this method, as well as automated compositonal extraction of strategies and counterexamples for the (dis)proved security properties. Experimental results show that compositional reasoning scales well to games with millions of nodes, enablingsecurity analysis of large real-life protocols.Additionally, we leverage compositional reasoning techniques to enhance the expressivity of the framework, enabling the modeling and analysis of protocols with actions influenced by external factors, which we refer to as games with conditional actions. To support this, we redefine key concepts such as game trees, security properties, strategies, counterexamples, honest behavior, and related notions. The analysis of games with conditional actions has also been automated and evaluated on an initial set of benchmarks involving non-trivial conditions.

Für die Sicherheitsanalyse von Blockchain-Technologien haben sich spieltheoretische Ansätze als nützlich erwiesen. Solche Ansätze untersuchen Protokolle aus einer wirtschaftlichen Perspektive, insbesondere durch die Erforschung der wirtschaftlichen Anreize, die das Nutzerverhalten steuern. Auf diese Weise wird sichergestellt, dass ein Abweichen vom ehrlichen Verhalten eines Protokolls keine finanziellen Vorteile mit sich bringt: solange sich die NutzerInnen an das Protokoll halten, kann ihnen kein finanzieller Schaden entstehen, unabhängig davon, wie sich andere verhalten.Eine solche wirtschaftliche Analyse von Blockchain-Protokollen kann als ein automatisiertes Schlussfolgerungsproblem in der Arithmetik der reellen Zahlen in der Prädikatenlogik 1. Stufe formuliert werden, wodurch das spieltheoretische Schlussfolgerungsproblem durch die Erfüllbarkeit einer Menge von Formeln, bekannt als Satisfiability Modulo Theories (SMT) Solving, gelöst wird. Diese Tools stehen jedoch vor großen Herausforderungen in Bezug auf Skalierbarkeit und Ausdruckskraft. Das Skalierbarkeitsproblem entsteht, weil aktuelle Ansätze den gesamten Spielbaum, der möglicherweise Millionen von Interaktionen umfasst, auf einmal analysieren. Dabei sind die generierten Formeln sehr groß und komplex. Hinsichtlich der Ausdruckskraft sind bestehende Frameworks nicht in der Lage, Spiele zu modellieren und zu analysieren, die externe Faktoren einbeziehen - wie etwa Preisschwankungen oder Wechselkurse, die vom aktuellen Weltzustand abhängen und außerhalb der Kontrolle der Spieler liegen.Um diesen Herausforderungen zu begegnen, schlagen wir eine auf dem Teile-und-Herrsche-Prinzip basierende Methode, welche auch die Modellierung großer Instanzen ermöglicht. Die Grundidee besteht darin, das Modell in seine Einzelteile zu zerlegen, die Sicherheitsanalyse auf diesen kleineren Teilen des Modells durchzuführen und die Ergebnisse anschließend zusammenzuführen, um das Gesamtergebnis der Analyse zu erhalten. Wir stellen eine korrekte und vollständige Automatisierung dieser Methode bereit sowie eine automatisierte Generierung von Strategien und Gegenbeispielen für die (widerlegten oder bestätigten) Sicherheitseigenschaften. Experimentelle Ergebnisse zeigen, dass diese Methode gut auf Spiele mit Millionen von Knoten skaliert und somit die Sicherheitsanalyse großer, realer Protokolle ermöglicht. Darüber hinaus nutzen wir Teile-und-Herrsche-Schlussfolgerungstechniken, um die Ausdruckskraft des Frameworks zu erweitern und die Modellierung sowie Analyse von Protokollen mit durch externe Faktoren beeinflussten Aktionen zu ermöglichen. Diese nennen wir Spiele mit bedingten Aktionen. Zu diesem Zweck definieren wir zentrale Konzepte wie Spielbäume, Sicherheitseigenschaften, Strategien, Gegenbeispiele, ehrliches Verhalten und verwandte Begriffe neu. Die Analyse von Spielen mit bedingten Aktionen wurde ebenfalls automatisiert und anhand von ersten Benchmarks mit nicht-trivialen Bedingungen evaluiert.