License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.11
URN: urn:nbn:de:0030-drops-134249
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13424/
Go to the corresponding OASIcs Volume Portal

Kammüller, Florian ; Nestmann, Uwe

Inter-Blockchain Protocols with the Isabelle Infrastructure Framework

pdf-format:
OASIcs-FMBC-2020-11.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{kammller_et_al:OASIcs:2020:13424,
  author =	{Florian Kamm{\"u}ller and Uwe Nestmann},
  title =	{{Inter-Blockchain Protocols with the Isabelle Infrastructure Framework}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{11:1--11:12},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bruno Bernardo and Diego Marmsoler},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13424},
  URN =		{urn:nbn:de:0030-drops-134249},
  doi =		{10.4230/OASIcs.FMBC.2020.11},
  annote =	{Keywords: Blockchain, smart contracts, interactive theorem proving, inter-blockchain protocols}
}

Keywords: Blockchain, smart contracts, interactive theorem proving, inter-blockchain protocols
Collection: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Issue Date: 2020
Date of publication: 11.12.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI