Advertisement

Blockchains as Kripke Models: An Analysis of Atomic Cross-Chain Swap

  • Yoichi HiraiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11247)

Abstract

There is a protocol called “atomic cross-chain swap” that spans across multiple blockchains, but is it really atomic? We analyze the protocol using a modal logic for asynchronous communication. The modal logic allows us to identify some assumptions required for the “atomic” property as logical formulas. We first demonstrate that the atomicity fails without some temporal-epistemic assumptions. We further construct a proof that the atomicity holds with strong enough temporal-epistemic assumptions. In both analyses, we use Kripke models of the modal logic. This is the first analysis of multiple blockchains’ interaction using a modal logic.

Keywords

Modal logic Epistemic logic Asynchronous computation Blockchains 

References

  1. 1.
    Atzei, N., Bartoletti, M., Cimoli, T., Lande, S., Zunino, R.: SoK: unraveling bitcoin smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 217–242. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_9CrossRefGoogle Scholar
  2. 2.
    Bitcoin Wiki: Script (2010–2018). https://en.bitcoin.it/wiki/Script. Accessed 13 Mar 2018
  3. 3.
    Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Chandy, K.M., Misra, J.: How processes learn. Distrib. Comput. 1(1), 40–52 (1986)CrossRefGoogle Scholar
  5. 5.
    van Dalen, D.: Logic and Structure. Springer, Heidelberg (1994).  https://doi.org/10.1007/978-3-662-02962-6CrossRefzbMATHGoogle Scholar
  6. 6.
    van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic, 1st edn. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-1-4020-5839-4CrossRefzbMATHGoogle Scholar
  7. 7.
    Emerson, E., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)CrossRefGoogle Scholar
  8. 8.
    Fagin, R., Halpern, J.Y., Vardi, M.Y., Moses, Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  9. 9.
    Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Gencer, A.E., van Renesse, R., Sirer, E.G.: Short paper: service-oriented sharding for blockchains. In: Kiayias, A. (ed.) FC 2017. LNCS, vol. 10322, pp. 393–401. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70972-7_22CrossRefGoogle Scholar
  11. 11.
    von Gleissenthall, K., Rybalchenko, A.: An epistemic perspective on consistency of concurrent computations. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 212–226. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40184-8_16CrossRefGoogle Scholar
  12. 12.
    Halpern, J.Y., Pass, R.: A knowledge-based analysis of the blockchain protocol. In: TARK 2017. EPTCS, vol. 251, pp. 324–335 (2017)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Hirai, Y.: An intuitionistic epistemic logic for asynchronous communication. Master’s thesis, the University of Tokyo (2010)Google Scholar
  14. 14.
    Hirai, Y.: An intuitionistic epistemic logic for sequential consistency on shared memory. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 272–289. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17511-4_16CrossRefzbMATHGoogle Scholar
  15. 15.
    Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133–169 (1998)CrossRefGoogle Scholar
  16. 16.
    Lundeberg, M.B.: Advisory: secret size attack on cross-chain hash lock smart contracts (2018). https://gist.github.com/markblundeberg/7a932c98179de2190049f5823907c016. Accessed 07 Mar 2018
  17. 17.
    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS 2016, pp. 254–269. ACM (2016)Google Scholar
  18. 18.
    Luu, L., Narayanan, V., Zheng, C., Baweja, K., Gilbert, S., Saxena, P.: A secure sharding protocol for open blockchains. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 17–30. CCS 2016. ACM (2016)Google Scholar
  19. 19.
    Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org/bitcoin.pdf. Accessed 20 Mar 2018
  20. 20.
    Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. ArXiv e-prints (2018)Google Scholar
  21. 21.
    Nolan, T.: Re: Alt chains and atomic transfers (2013). https://bitcointalk.org/index.php?topic=193281.msg2224949#msg2224949. Accessed 12 Mar 2018
  22. 22.
    Poon, J., Buterin, V.: Plasma: scalable autonomous smart contracts (2017). https://plasma.io/plasma.pdf. Accessed 07 Mar 2018
  23. 23.
    Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 478–493. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_30CrossRefGoogle Scholar
  24. 24.
    Troelstra, A.S., Van Dalen, D.: Constructivism in Mathematics: An Introduction, vol. 1. Elsevier, Amsterdam (1988)zbMATHGoogle Scholar
  25. 25.
    Wood, G.: Polkadot: vision for a heterogeneous multi-chain framework (2016). https://github.com/w3f/polkadot-white-paper/blob/master/PolkaDotPaper.pdf. Accessed 07 Mar 2018

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.BerlinGermany

Personalised recommendations