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.
翻译:在一个块链系统中, 节点定期将数据传播到其他节点。 科学文献中的理想观点是数据直接广播给所有节点, 而在实践中数据则通过反复多播传播。 由于通常只有理想环境才建立正确性和安全性, 关键是要显示这些属性会传到现实世界的落实中。 可以通过证明理想和真实行为是等效的来做到这一点。 在本文描述的工作中, 我们通过证明上述等同语的简单变体, 朝着这种证明迈出了重要的一步。 简化是, 我们只考虑一对具体的网络表象, 但它说明在任意的表象中遇到的重要现象。 为了描述数据传播系统, 我们使用一种特定域语言, 用于一般用途的计算过程。 这使我们能够在我们的证明中运用丰富的过程计算理论, 也就是用伊莎贝尔校准助理进行机检。