1 Search Results for "Kammüller, Florian"

Document
DOI: 10.4230/OASIcs.FMBC.2020.11
Inter-Blockchain Protocols with the Isabelle Infrastructure Framework

Authors: Florian Kammüller and Uwe Nestmann

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{kammuller_et_al:OASIcs.FMBC.2020.11,
  author =	{Kamm\"{u}ller, Florian and Nestmann, Uwe},
  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 =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.11},
  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}
}
  • Refine by Author
  • 1 Kammüller, Florian
  • 1 Nestmann, Uwe

  • Refine by Classification
  • 1 Networks → Peer-to-peer protocols
  • 1 Networks → Security protocols
  • 1 Software and its engineering → Software verification and validation

  • Refine by Keyword
  • 1 Blockchain
  • 1 inter-blockchain protocols
  • 1 interactive theorem proving
  • 1 smart contracts

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2020

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 Imprint Privacy Contact