Isabelle Infrastructure framework with blockchains, smart contracts and Inter-blockchain protocols (IBC)
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. Smart contracts control the execution and make transactions traceable and irreversible. Inter-blockchain (IBC) protocols define and control exchanges between different blockchains. The Isabelle Infrastructure framework serves security and privacy for system 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 the current development, we propose the extension of this blockchain model by smart contracts. Due to the abstractness of this model of blockchains and smart contracts in the Isabelle Infrastructure model, we can use this model to instantiate different blockchains and formalise IBC protocols.