DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2021.25

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks

Authors: Andreas Lochbihler

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract

Aharoni et al. [Ron Aharoni et al., 2010] proved the max-flow min-cut theorem for countable networks, namely that in every countable network with finite edge capacities, there exists a flow and a cut such that the flow saturates all outgoing edges of the cut and is zero on all incoming edges. In this paper, we formalize their proof in Isabelle/HOL and thereby identify and fix several problems with their proof. We also provide a simpler proof for networks where the total outgoing capacity of all vertices other than the source is finite. This proof is based on the max-flow min-cut theorem for finite networks.

Cite as

Andreas Lochbihler. A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{lochbihler:LIPIcs.ITP.2021.25,
  author =	{Lochbihler, Andreas},
  title =	{{A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.25},
  URN =		{urn:nbn:de:0030-drops-139204},
  doi =		{10.4230/LIPIcs.ITP.2021.25},
  annote =	{Keywords: flow network, optimization, infinite graph, Isabelle/HOL}
}

Document

DOI: 10.4230/OASIcs.FMBC.2020.6

Authenticated Data Structures as Functors in Isabelle/HOL

Authors: Andreas Lochbihler and Ognjen Marić

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

Abstract

Merkle trees are ubiquitous in blockchains and other distributed ledger technologies (DLTs). They guarantee that the involved systems are referring to the same binary tree, even if each of them knows only the cryptographic hash of the root. Inclusion proofs allow knowledgeable systems to share subtrees with other systems and the latter can verify the subtrees' authenticity. Often, blockchains and DLTs use data structures more complicated than binary trees; authenticated data structures generalize Merkle trees to such structures. We show how to formally define and reason about authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL. The construction lives in the symbolic model, i.e., we assume that no hash collisions occur. Our approach is modular and allows us to construct complicated trees from reusable building blocks, which we call Merkle functors. Merkle functors include sums, products, and function spaces and are closed under composition and least fixpoints. As a practical application, we model the hierarchical transactions of Canton, a practical interoperability protocol for distributed ledgers, as authenticated data structures. This is a first step towards formalizing the Canton protocol and verifying its integrity and security guarantees.

Cite as

Andreas Lochbihler and Ognjen Marić. Authenticated Data Structures as Functors in Isabelle/HOL. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lochbihler_et_al:OASIcs.FMBC.2020.6,
  author =	{Lochbihler, Andreas and Mari\'{c}, Ognjen},
  title =	{{Authenticated Data Structures as Functors in Isabelle/HOL}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{6:1--6:15},
  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.6},
  URN =		{urn:nbn:de:0030-drops-134196},
  doi =		{10.4230/OASIcs.FMBC.2020.6},
  annote =	{Keywords: Merkle tree, functor, distributed ledger, datatypes, higher-order logic}
}

Search Results

Documents authored by Lochbihler, Andreas

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks

Abstract

Cite as

Authenticated Data Structures as Functors in Isabelle/HOL

Abstract

Cite as

Thanks for your feedback!

Could not send message