Your Blockchain Needn't Care How the Message is Spread

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 of processes that is embedded in a general-purpose process calculus. This allows us to leverage the rich theory of process calculi in our proof, which is machine-checked using the Isabelle proof assistant.