Advertisement

Modeling Bitcoin Contracts by Timed Automata

  • Marcin Andrychowicz
  • Stefan Dziembowski
  • Daniel Malinowski
  • Łukasz Mazurek
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8711)

Abstract

Bitcoin is a peer-to-peer cryptographic currency system. Since its introduction in 2008, Bitcoin has gained noticeable popularity, mostly due to its following properties: (1) the transaction fees are very low, and (2) it is not controlled by any central authority, which in particular means that nobody can “print” the money to generate inflation. Moreover, the transaction syntax allows to create the so-called contracts, where a number of mutually-distrusting parties engage in a protocol to jointly perform some financial task, and the fairness of this process is guaranteed by the properties of Bitcoin. Although the Bitcoin contracts have several potential applications in the digital economy, so far they have not been widely used in real life. This is partly due to the fact that they are cumbersome to create and analyze, and hence risky to use.

In this paper we propose to remedy this problem by using the methods originally developed for the computer-aided analysis for hardware and software systems, in particular those based on the timed automata. More concretely, we propose a framework for modeling the Bitcoin contracts using the timed automata in the Uppaal model checker. Our method is general and can be used to model several contracts. As a proof-of-concept we use this framework to model some of the Bitcoin contracts from our recent previous work. We then automatically verify their security in Uppaal, finding (and correcting) some subtle errors that were difficult to spot by the manual analysis. We hope that our work can draw the attention of the researchers working on formal modeling to the problem of the Bitcoin contract verification, and spark off more research on this topic.

Keywords

Commitment Scheme Time Automaton Honest Party Cryptology ePrint Archive Digital Currency 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science (1994)Google Scholar
  3. 3.
    Alur, R., Henzinger, T.A.: A really temporal logic. Journal of the ACM (1994)Google Scholar
  4. 4.
    Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES - A tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 460. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Andreessen, M.: Why Bitcoin Matters. The New York Times (January 2013), http://dealbook.nytimes.com/2014/01/21/why-bitcoin-matters/ (accessed on January 26, 2014)
  6. 6.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, Ł.: Fair two-party computations via the bitcoin deposits. Cryptology ePrint Archive, Report 2013/837 (2013), http://eprint.iacr.org/2013/837, accepted to the 1st Workshop on Bitcoin Research
  7. 7.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, Ł.: How to deal with malleability of Bitcoin transactions. ArXiv e-prints (December 2013)Google Scholar
  8. 8.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, Ł.: Secure Multiparty Computations on Bitcoin. Cryptology ePrint Archive (2013), http://eprint.iacr.org/2013/784, accepted to the 35th IEEE Symposium on Security and Privacy, Oakland (2014)
  9. 9.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal 4.0 (2006)Google Scholar
  10. 10.
    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Softw. Eng. 17(3), 259–273 (1991)CrossRefMathSciNetGoogle Scholar
  11. 11.
  12. 12.
    Delfs, H., Knebl, H.: Introduction to Cryptography: Principles and Applications. Information Security and Cryptography. Springer (2007)Google Scholar
  13. 13.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Theory (1983)Google Scholar
  14. 14.
    Dwork, C., Naor, M.: Pricing via processing or combatting junk mail. In: Brickell, E.F. (ed.) CRYPTO 1992. LNCS, vol. 740, pp. 139–147. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  15. 15.
    The Economist. The Economist explains: How does Bitcoin work? (April 2013), http://www.economist.com/blogs/economist-explains/2013/04/economist-explains-how-does-bitcoin-work (accessed on January 26, 2014)
  16. 16.
    Ateniese, G., et al.: Certified bitcoins. Cryptology ePrint Archive, Report 2014/076Google Scholar
  17. 17.
    Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)Google Scholar
  18. 18.
    Barber, S., Boyen, X., Shi, E., Uzun, E.: Bitter to better — how to make bitcoin a better currency. In: Keromytis, A.D. (ed.) FC 2012. LNCS, vol. 7397, pp. 399–414. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  19. 19.
    Katz, J., Lindell, Y.: Introduction to Modern Cryptography. Chapman & Hall/Crc Cryptography and Network Security Series. Chapman & Hall/CRC (2007)Google Scholar
  20. 20.
    Lee, T.B.: Here’s how Bitcoin charmed Washington, http://www.washingtonpost.com/blogs/the-switch/wp/2013/11/21/heres-how-bitcoin-charmed-washington (accessed on January 26, 2014)
  21. 21.
    Morris, D.Z.: Bitcoin is not just digital currency. It’s Napster for finance. CNN Money (January 2014), http://finance.fortune.cnn.com/2014/01/21/bitcoin-platform (accessed on January 26, 2014)
  22. 22.
    Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2008)Google Scholar
  23. 23.
    Nicollin, X., Sifakis, J.: The algebra of timed processes, atp: Theory and application. Inf. Comput. 114(1), 131–178 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  24. 24.
    Cohen, R.: Global Bitcoin Computing Power Now 256 Times Faster Than Top 500 Supercomputers, Combined! Forbes, http://www.forbes.com/sites/reuvencohen/2013/11/28/global-bitcoin-computing-power-now-256-times-faster-than-top-500-supercomputers-combined/
  25. 25.
    Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theor. Comput. Sci. 58(1-3), 249–261 (1988)CrossRefzbMATHMathSciNetGoogle Scholar
  26. 26.
    Bitcoin wiki. Contracts, http://en.bitcoin.it/wiki/Contracts (accessed on January 26, 2014)
  27. 27.
    Bitcoin wiki. Script, https://en.bitcoin.it/wiki/Script (accessed on January 26, 2014)
  28. 28.
    Yi, W.: CCS + time = an interleaving model for real time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  29. 29.
    Yovine, S.: Kronos: a verification tool for real-time systems. Journal on Software Tools for Technology Transfer 1 (October 1997)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Marcin Andrychowicz
    • 1
  • Stefan Dziembowski
    • 1
  • Daniel Malinowski
    • 1
  • Łukasz Mazurek
    • 1
  1. 1.Cryptology and Data Security GroupUniversity of WarsawPoland

Personalised recommendations