@inproceedings{66,
  abstract     = {Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.},
  author       = {Chatterjee, Krishnendu and Goharshady, Amir and Ibsen-Jensen, Rasmus and Velner, Yaron},
  isbn         = {978-3-95977-087-3},
  location     = {Beijing, China},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Ergodic mean-payoff games for the analysis of attacks in crypto-currencies}},
  doi          = {10.4230/LIPIcs.CONCUR.2018.11},
  volume       = {118},
  year         = {2018},
}