A TLA+ Formal Proof of a Cross-Chain Swap
A TLA+ Formal Proof of a Cross-Chain Swap
复制标题
跨链交换的 TLA 正式证明
DOI：
10.1145/3491003.3491006
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
H. Fauconnier
中科院分区：
文献类型：
--
作者：
Zeinab Nehaï;François Bobot;S. Piergiovanni;C. Delporte;H. Fauconnier
区块链是一种特定类型的分布式账本，由一系列相互链接的交易数据块构成。随着时间的推移，区块链的使用越来越多，一些新的区块链正在出现。因此，增强区块链实现之间的互操作性以允许去中心化交易至关重要。实现这一目标的一种方法是使用跨链交换协议。这些协议是处理资产的关键系统。因此，必须确保系统不包含错误。本文用形式化的方法描述了跨链交换问题。我们定义了安全性和弱活动性属性，以保证在异步系统中没有正确的参与者会更糟糕。此外，我们还提供了一个正式证明的拜占庭容错协议，该协议满足交换规范。该协议对区块链进行了足够的抽象，以适应旨在执行跨链交换的各种分布式账本框架。此外，我们还说明了如何在区块链系统中实例化所描述的抽象协议。
Blockchains are a specific type of distributed ledgers structured by a sequence of blocks of transactional data linked to each other. The use of blockchains has increased over time, and several new blockchains are emerging. It is therefore essential to enhance the interoperability between blockchain implementations to allow decentralised trading. One way to achieve this is with Cross-Chain Swap protocols. These protocols are critical systems as they handle assets. Therefore, it must be sure that the system does not contain errors. In this paper, we describe the Cross-Chain Swap problem in a formal way. We define safety and weak-liveness properties that guarantee no correct participant will be worse-off in an asynchronous system. Moreover, we provide a formally proved Byzantine fault-tolerant protocol that satisfies the swap specification. The protocol abstracts the blockchain enough to suit various distributed ledger frameworks aiming to perform a cross-chain swap. In addition, we illustrate how the described abstract protocol can be instantiated in a blockchain system.