Ergodic Mean-Payoff Games for the Analysis of Attacks in\n Crypto-Currencies

Abstract

Crypto-currencies are digital assets designed to work as a medium of\nexchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest\nbehavior of participants). A framework for the analysis of attacks in\ncrypto-currencies requires (a) modeling of game-theoretic aspects to analyze\nincentives for deviation from honest behavior; (b) concurrent interactions\nbetween participants; and (c) analysis of long-term monetary gains. Traditional\ngame-theoretic approaches for the analysis of security protocols consider\neither qualitative temporal properties such as safety and termination, or the\nvery special class of one-shot (stateless) games. However, to analyze general\nattacks on protocols for crypto-currencies, both stateful analysis and\nquantitative objectives are necessary. In this work our main contributions are\nas follows: (a) we show how a class of concurrent mean-payoff games, namely\nergodic games, can model various attacks that arise naturally in\ncrypto-currencies; (b) we present the first practical implementation of\nalgorithms for ergodic games that scales to model realistic problems for\ncrypto-currencies; and (c) we present experimental results showing that our\nframework can handle games with thousands of states and millions of\ntransitions.\n