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

TL;DR

This paper introduces a novel framework using ergodic mean-payoff games to model and analyze long-term attacks in crypto-currencies, addressing the need for stateful and quantitative analysis of security protocols.

Contribution

It demonstrates how ergodic games can model crypto-currency attacks, provides the first scalable implementation of algorithms for these games, and shows practical results on large models.

Findings

Framework handles thousands of states and millions of transitions.

Algorithms successfully model realistic crypto-currency attack scenarios.

Scalable approach enables long-term security analysis.

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-payoff 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.