Automating proofs of game-theoretic security properties of off-chain protocols

Abstract

Off-chain transactions are an effective approach to mitigating the issues arising as a consequence of the low scalability of blockchain technology, which are especially problematic in cryptocurrencies like Bitcoin. By conducting only few transactions on the blockchain itself and instead handling most of them in a second layer, the overall throughput of transactions - which is a crucial parameter in financial services - can be increased significantly. An example for such an off-chain protocol is the Bitcoin Lightning Network. When it comes to the security of off-chain protocols, game-theoretic approaches have been proven useful. Modeling a protocol as a game and evaluating it based on established game-theoretic properties allows for an extensive and accurate security analysis. However, creating and analyzing such a game manually is a tedious and error-prone task due to the high complexity of off-chain protocols. Therefore, we present a prototype for a framework that automates this analysis, thus facilitating the evaluation of off-chain protocols with respect to their security. To that end, we apply satisfiability modulo theories (SMT) solving for each of three established security properties to a set of constraints which is generated based on the input game and the analyzed property. We evaluate our prototype using several example games, one of which models the closing phase in the Lightning Network protocol.