论文标题
您的区块链不需要关心消息如何传播
Your Blockchain Needn't Care How the Message is Spread
论文作者
论文摘要
在区块链系统中，节点定期将数据分配给其他节点。科学文献中采取的理想观点是，数据直接向所有节点广播，而实际上数据是通过重复的多播分布的。由于通常仅针对理想的设置建立了正确性和安全性，因此至关重要的是，这些属性将这些属性延续到现实世界中的实现。这可以通过证明理想和真实行为等效来完成。 在本文中描述的工作中，我们通过证明上述等价声明的更简单变体迈出了重要的一步。简化是我们仅考虑一对网络拓扑，但它说明了使用任意拓扑遇到的重要现象。为了描述分布数据的系统，我们使用了特定于域的过程语言，该过程嵌入了通用过程计算中。这使我们能够在证明中利用丰富的过程计算理论，该理论是使用Isabelle证明助手对机器检查的。
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.
