Search Results

Documents authored by Nestmann, Uwe

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}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2017
LIPIcs, Volume 85, CONCUR'17, Complete Volume

Authors: Roland Meyer and Uwe Nestmann

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
LIPIcs, Volume 85, CONCUR'17, Complete Volume
Cite as

28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{meyer_et_al:LIPIcs.CONCUR.2017,
  title =	{{LIPIcs, Volume 85, CONCUR'17, Complete Volume}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017},
  URN =		{urn:nbn:de:0030-drops-79070},
  doi =		{10.4230/LIPIcs.CONCUR.2017},
  annote =	{Keywords: Software, Data, Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2017.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Roland Meyer and Uwe Nestmann

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.CONCUR.2017.0,
  author =	{Meyer, Roland and Nestmann, Uwe},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.0},
  URN =		{urn:nbn:de:0030-drops-77693},
  doi =		{10.4230/LIPIcs.CONCUR.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.19
Topological Self-Stabilization with Name-Passing Process Calculi

Authors: Christina Rickmann, Christoph Wagner, Uwe Nestmann, and Stefan Schmid

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Topological self-stabilization is the ability of a distributed system to have its nodes themselves establish a meaningful overlay network. Independent from the initial network topology, it converges to the desired topology via forwarding, inserting, and deleting links to neighboring nodes. We adapt a linearization algorithm, originally designed for a shared memory model, to asynchronous message-passing. We use an extended localized pi-calculus to model the algorithm and to formally prove its essential self-stabilization properties: closure and weak convergence for every arbitrary initial configuration, and strong convergence for restricted cases.
Cite as

Christina Rickmann, Christoph Wagner, Uwe Nestmann, and Stefan Schmid. Topological Self-Stabilization with Name-Passing Process Calculi. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 19:1-19:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{rickmann_et_al:LIPIcs.CONCUR.2016.19,
  author =	{Rickmann, Christina and Wagner, Christoph and Nestmann, Uwe and Schmid, Stefan},
  title =	{{Topological Self-Stabilization with Name-Passing Process Calculi}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{19:1--19:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.19},
  URN =		{urn:nbn:de:0030-drops-61761},
  doi =		{10.4230/LIPIcs.CONCUR.2016.19},
  annote =	{Keywords: Distributed Algorithms, Fault Tolerance, Topological Self-Stabilization, Linearization, Process Calculi}
}
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