Your Blockchain Needn't Care How the Message is Spread
Wolfgang Jeltsch, Javier D\'iaz

TL;DR
This paper proves that the security and correctness properties of data distribution in blockchain systems hold true in real-world multicast scenarios by establishing an equivalence with ideal broadcast models, using formal methods.
Contribution
It introduces a formal framework and proof technique, via process calculus and Isabelle, to show the equivalence between ideal broadcast and multicast data distribution in blockchain networks.
Findings
Proved equivalence between ideal broadcast and multicast data distribution.
Demonstrated the approach on specific network topologies.
Leveraged formal methods for machine-checked proofs.
Abstract
In a blockchain system, nodes regularly distribute data to other nodes. The ideal perspective taken in the scientific literature is that data is broadcast to all nodes directly, while in practice data is distributed by repeated multicast. Since correctness and security typically have been established for the ideal setting only, it is vital to show that these properties carry over to real-world implementations. This can be done by proving that the ideal and the real behavior are equivalent. In the work described in this paper, we take an important step towards such a proof by proving a simpler variant of the above equivalence statement. The simplification is that we consider only a concrete pair of network topologies, which nevertheless illustrates important phenomena encountered with arbitrary topologies. For describing systems that distribute data, we use a domain-specific language…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsService-Oriented Architecture and Web Services · Business Process Modeling and Analysis · Distributed systems and fault tolerance
