论文标题
比特币跟踪网络：签署时间的正式合同验证
Bitcoin Trace-Net: Formal Contract Verification at Signing Time
论文作者
论文摘要
智能合同方案有望以无信任的方式调节加密货币之间的转移。安全的智能合同实施应确保每个参与者始终将合同交易附加到区块链上，以便将合同转向安全完成。为此，我们提出了比特币跟踪网络，这是一个合同验证框架，该框架从基础合同实施中生成可执行的符号模型。痕量网络模型由培养皿网络形式主义组成，该形式富含dolev-yao样演员知识模型。显式符号演员知识模型支持对具有加密子协议的合同的验证，这在区块链上可能无法观察到。 Trace-NET足以准确地对区块链语义进行建模，例如交易广播与随后的确认之间的延迟，以及对对抗性区块链的有限深度重组，这两者都可以破坏智能合约安全性。作为实现级别框架，可以在运行时实例化跟踪网络以监视和验证智能合约协议执行。
Smart contracting protocols promise to regulate the transfer of cryptocurrency amongst participants in a trustless manner. A safe smart contract implementation should ensure that each participant can always append a contract transaction to the blockchain in order move the contract towards secure completion. To this goal, we propose Bitcoin Trace-Net, a contract verification framework which generates an executable symbolic model from the underlying contract implementation. A Trace-Net model consists of a Petri Net formalism enriched with a Dolev-Yao-like actor knowledge model. The explicit symbolic actor knowledge model supports the verification of contracts featuring cryptographic sub-protocols, which may not be observable on the blockchain. Trace-Net is sufficiently expressive to accurately model blockchain semantics such as the delay between a transaction broadcast and its subsequent confirmation, as well as adversarial blockchain reorganizations of finite depths, both of which can break smart contract safety. As an implementation level framework, Trace-Net can be instantiated at run-time to monitor and verify smart contract protocol executions.
