Document Open Access Logo

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

Authors Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Yaron Velner

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.11.pdf
  • Filesize: 1.02 MB
  • 17 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
  • IST Austria (Institute of Science and Technology Austria), Klosterneuburg, Austria
Amir Kafshdar Goharshady
  • IST Austria (Institute of Science and Technology Austria), Klosterneuburg, Austria
Rasmus Ibsen-Jensen
  • IST Austria (Institute of Science and Technology Austria), Klosterneuburg, Austria
Yaron Velner
  • Hebrew University of Jerusalem, Jerusalem, Israel

Cite As Get BibTex

Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.11

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Crypto-currency
  • Quantitative Verification
  • Mean-payoff Games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. M. Abadi and P. Rogaway. Reconciling two views of cryptography. In Proceedings of the IFIP International Conference on Theoretical Computer Science, pages 3-22. Springer, 2000. Google Scholar
  2. C. Baier, C. Dubslaff, J. Klein, S. Klüppelholz, and S Wunderlich. Probabilistic model checking for energy-utility analysis. In Horizons of the Mind. A Tribute to Prakash Panangaden - Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, pages 96-123, 2014. Google Scholar
  3. C. Baier, S. Klüppelholz, H. de Meer, F. Niedermeier, and S. Wunderlich. Greener bits: Formal analysis of demand response. In ATVA, pages 323-339, 2016. Google Scholar
  4. Bitcoin Wiki. Comparison of mining pools, 2017. URL: http://en.bitcoin.it/Comparison_of_mining_pools.
  5. D. Blackwell and T. Ferguson. The big match. The Annals of Mathematical Statistics, 39(1):159-163, 1968. Google Scholar
  6. blockcypher.com. Confidence factor, 2017. URL: http://dev.blockcypher.com/#confidence-factor.
  7. R. Bloem, K. Chatterjee, T.A. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. In CAV, pages 140-156, 2009. Google Scholar
  8. J. Bonneau, A. Miller, J. Clark, A. Narayanan, J.A. Kroll, and E.W. Felten. Sok: Research perspectives and challenges for bitcoin and cryptocurrencies. In IEEE Symposium on Security and Privacy, pages 104-121. IEEE, 2015. Google Scholar
  9. P. Cerný, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, and R. Singh. Quantitative synthesis for concurrent programs. In CAV, pages 243-259, 2011. Google Scholar
  10. K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, and Y. Velner. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. arXiv, 2018. URL: http://arxiv.org/abs/1806.03108.
  11. K. Chatterjee, A.K. Goharshady, and Y. Velner. Quantitative analysis of smart contracts. In ESOP, pages 739-767, 2018. Google Scholar
  12. K. Chatterjee, T.A. Henzinger, and M. Jurdzinski. Games with secure equilibria. In LICS, pages 160-169, 2004. Google Scholar
  13. K. Chatterjee and R. Ibsen-Jensen. The complexity of ergodic mean-payoff games. In ICALP II, pages 122-133, 2014. Google Scholar
  14. K. Chatterjee, R. Majumdar, and T. A. Henzinger. Stochastic limit-average games are in EXPTIME. Int. J. Game Theory, 37(2):219-234, 2008. Google Scholar
  15. K. Chatterjee, A. Pavlogiannis, and Y. Velner. Quantitative interprocedural analysis. In POPL, pages 539-551, 2015. Google Scholar
  16. K. Chatterjee and V. Raman. Assume-guarantee synthesis for digital contract signing. Formal Asp. Comput., 26(4):825-859, 2014. Google Scholar
  17. CNN Money. Bitcoin’s uncertain future as currency, 2011. URL: http://money.cnn.com/video/technology/2011/07/18/t_bitcoin_currency.cnnmoney/.
  18. coinmarketcap.com. Crypto-currency market capitalizations, 2017. URL: http://coinmarketcap.com/.
  19. I. Eyal. The miner’s dilemma. In IEEE Symposium on Security and Privacy, pages 89-103. IEEE, 2015. Google Scholar
  20. I. Eyal and E.G. Sirer. Majority is not enough: Bitcoin mining is vulnerable. In Financial Cryptography and Data Security, 2014. Google Scholar
  21. V. Forejt, M. Z. Kwiatkowska, and D. Parker. Pareto curves for probabilistic model checking. In ATVA, pages 317-332, 2012. Google Scholar
  22. D. Gillette. Stochastic games with zero stop probabilitites. In CTG, pages 179-188. Princeton University Press, 1957. Google Scholar
  23. K. A. Hansen, M. Koucký, N. Lauritzen, P. B. Miltersen, and E. P. Tsigaridas. Exact algorithms for solving stochastic games: extended abstract. In STOC, pages 205-214, 2011. Google Scholar
  24. A.J. Hoffman and R.M. Karp. On nonterminating stochastic games. Management Sciences, 12(5):359-370, 1966. Google Scholar
  25. G. Karame, E. Androulaki, and S. Capkun. Two bitcoins at the price of one? double-spending attacks on fast payments in bitcoin. IACR Cryptology ePrint Archive, 2012:248, 2012. Google Scholar
  26. S. Kremer and J.F. Raskin. A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security, 2003. Google Scholar
  27. Marta Z. Kwiatkowska, David Parker, and Aistis Simaitis. Strategic analysis of trust models for user-centric networks. In SR, pages 53-59, 2013. Google Scholar
  28. J. Kwon. Tendermint: Consensus without mining, 2015. URL: https://blog.ethereum.org/2015/08/01/introducing-casper-friendly-ghost/.
  29. A. Laszka, B. Johnson, and J. Grossklags. When bitcoin mining pools run dry. In International Conference on Financial Cryptography and Data Security, pages 63-77. Springer, 2015. Google Scholar
  30. J.F. Mertens and A. Neyman. Stochastic games. IJGT, 10:53-66, 1981. Google Scholar
  31. S. Nakamoto. Bitcoin: A peer-to-peer electronic cash system, 2008. Google Scholar
  32. NxtCommunity. Nxt whitepaper, 2014. URL: http://bravenewcoin.com/assets/Whitepapers/NxtWhitepaper-v122-rev4.pdf.
  33. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, pages 179-190. ACM Press, 1989. Google Scholar
  34. P.J.G. Ramadge and W.M. Wonham. The control of discrete event systems. IEEE Transactions on Control Theory, 77:81-98, 1989. Google Scholar
  35. Meni Rosenfeld. Analysis of bitcoin pooled mining reward systems. arXiv preprint arXiv:1112.4980, 2011. Google Scholar
  36. A. Sapirshtein, Y. Sompolinsky, and A. Zohar. Optimal selfish mining strategies in bitcoin. arXiv preprint arXiv:1507.06183, 2015. Google Scholar
  37. L.S. Shapley. Stochastic games. PNAS, 39:1095-1100, 1953. Google Scholar
  38. Y. Sompolinsky and A. Zohar. Bitcoin’s security model revisited. CoRR, abs/1605.09193, 2016. Google Scholar
  39. M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state systems. In FOCS, pages 327-338. IEEE, 1985. Google Scholar
  40. V. Zamfir. Introducing casper, the friendly ghost, 2015. URL: https://blog.ethereum.org/2015/08/01/introducing-casper-friendly-ghost/.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact