Document Open Access Logo

Inter-Blockchain Protocols with the Isabelle Infrastructure Framework

Authors Florian Kammüller , Uwe Nestmann

PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.11.pdf
  • Filesize: 0.58 MB
  • 12 pages

Document Identifiers

Author Details

Florian Kammüller
  • Middlesex University London, UK
  • Technische Universität Berlin, Germany
Uwe Nestmann
  • Technische Universität Berlin, Germany

Funding

  • Kammüller, Florian: Research for this paper has been supported by CHIST-ERA grant 101112, SUCCESS.

Cite As Get BibTex

Florian Kammüller and Uwe Nestmann. Inter-Blockchain Protocols with the Isabelle Infrastructure Framework. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.FMBC.2020.11

Abstract

The main incentives of blockchain technology are distribution and distributed change, consistency, and consensus. Beyond just being a distributed ledger for digital currency, smart contracts add transaction protocols to blockchains to execute terms of a contract in a blockchain network. Inter-blockchain (IBC) protocols define and control exchanges between different blockchains.
The Isabelle Infrastructure framework {has been designed to} serve security and privacy for IoT architectures by formal specification and stepwise attack analysis and refinement. A major case study of this framework is a distributed health care scenario for data consistency for GDPR compliance. This application led to the development of an abstract system specification of blockchains for IoT infrastructures.
In this paper, we first give a summary of the concept of IBC. We then introduce an instantiation of the Isabelle Infrastructure framework to model blockchains. Based on this we extend this model to instantiate different blockchains and formalize IBC protocols. We prove the concept by defining the generic property of global consistency and prove it in Isabelle.

Subject Classification

ACM Subject Classification
  • Networks → Peer-to-peer protocols
  • Networks → Security protocols
  • Software and its engineering → Software verification and validation
Keywords
  • Blockchain
  • smart contracts
  • interactive theorem proving
  • inter-blockchain protocols

Metrics

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

References

  1. S. Amani, M. Bégel, M. Bortin, and M. Staples. Towards verifying ethereum smart contract bytecode in isabelle/hol. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 66-77. ACM, 2018. Google Scholar
  2. N. Catano, D. Marmsoler, and B. Bernardo, editors. Pre-proceedings of the First Workshop on Formal Methods for Blockchains, FMBC, 2019. Selected papers to appear in Springer LNCS. URL: https://sites.google.com/view/fmbc.
  3. CHIST-ERA. Success: Secure accessibility for the internet of things, 2016. http://www.chistera.eu/projects/success. Google Scholar
  4. Sylvain Conchon, Alexandrina Korneva1, and Fatiha Zaidi. Verifying smart contracts with cubicle, 2019. Selected papers to appear in Springer LNCS. URL: https://sites.google.com/view/fmbc.
  5. Cosmos. Cosmos hub, 2020. accessed 23.1.2020. URL: https://hub.cosmos.network/master/hub-overview/overview.html.
  6. I. Grishchenko, M. Maffei, and C. Schneidewind. A semantic framework for the security analysis of ethereum smart contracts. In L. Bauer and R. Ksters, editors, Principles of Security and Trust, Lecture Notes in Computer Science, pages 243-269. Springer, 2017. Google Scholar
  7. Y. Hirai. Defining the ethereum virtual machine for interactive theorem provers. In M. Brenner, K. Rohloff, J. Bonneau, A. Miller, P. Y. Ryan, V. Teague, A. Braccialiand M. Sala, F. Pintore, and M. Jakobsson, editors, Financial Cryptography and Data Security, Lecture Notes in Computer Science, pages 520-535. Springer, 2017. Google Scholar
  8. F. Kammüller. Formal modeling and analysis of data protection for gdpr compliance of iot healthcare systems. In IEEE Systems, Man and Cybernetics, SMC2018. IEEE, 2018. Google Scholar
  9. F. Kammüller. Attack trees in isabelle extended with probabilities for quantum cryptography. Computer & Security, 87, 2019. URL: https://doi.org/10.1016/j.cose.2019.101572.
  10. F. Kammüller. Combining secure system design with risk assessment for iot healthcare systems. In Workshop on Security, Privacy, and Trust in the IoT, SPTIoT’19, colocated with IEEE PerCom. IEEE, 2019. Google Scholar
  11. F. Kammüller. Qkd in isabelle – bayesian calculation. arXiv, cs.CR, 2019. URL: https://arxiv.org/abs/1905.00325.
  12. F. Kammüller. Isabelle infrastructure framework for ibc, 2020. Isabelle sources for IBC formalisation. URL: https://github.com/flokam/IsabelleSC.
  13. F. Kammüller, M. Kerber, and C.W. Probst. Towards formal analysis of insider threats for auctions. In 8th ACM CCS International Workshop on Managing Insider Security Threats, MIST’16. ACM, 2016. Google Scholar
  14. F. Kammüller, M. Wenzel, and L. C. Paulson. Locales - a sectioning concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, volume 1690 of LNCS. Springer, 1999. Google Scholar
  15. Florian Kammüller. A formal development cycle for security engineering in isabelle, 2020. URL: http://arxiv.org/abs/2001.08983.
  16. Mikhail Mandrykin1, Jake O'Shannessy, Jacob Payne, and Ilya Shchepetkov. Formal specification of a security framework for smart contracts, 2019. Selected papers to appear in Springer LNCS. URL: https://sites.google.com/view/fmbc.
  17. A. C. Myers and B. Liskov. Complete, safe information flow with decentralized labels. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 1999. Google Scholar
  18. J. Botsch Nielsen and B. Spitters. Smart contract interactions in coq, 2019. Selected papers to appear in Springer LNCS. URL: https://sites.google.com/view/fmbc.
  19. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002. Google Scholar
  20. Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, and Grigore Roundefinedu. A formal verification tool for ethereum vm bytecode. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, pages 912-915, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3236024.3264591.
  21. Lawrence Paulson and Jasmin Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. Proceedings of the 8th International Workshop on the Implementation of Logics, February 2015. URL: https://doi.org/10.29007/tnfd.
  22. Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1-2):85-128, 1998. URL: http://iospress.metapress.com/content/5wlu8p2am1du051d/.
  23. Grigore Rosu. Specifying languages and verifying programs with k. 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 28-31, 2013. Google Scholar
  24. The IBC Specification Team. The interblockchain communication protocol, 2020. 4th May 2020 — 1.0.0-rc5. URL: https://github.com/cosmos/ics/blob/master/spec.pdf.
  25. Duy Minh Vo. Verification of Smart Contracts using the K-framework. PhD thesis, Technische Universität Berlin, 2018. Google Scholar
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