文章基本信息

标题：Inter-Blockchain Protocols with the Isabelle Infrastructure Framework
本地全文：下载
作者：Kammüller, Florian ; Uwe Nestmann
期刊名称：OASIcs : OpenAccess Series in Informatics
电子版ISSN：2190-6807
出版年度：2020
卷号：84
页码：1-12
DOI：10.4230/OASIcs.FMBC.2020.11
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Blockchain; smart contracts; interactive theorem proving; inter-blockchain protocols