Formal Verification of Fair Exchange Based on Bitcoin Smart Contracts

【Author】 Shi, Cheng; Yoneyama, Kazuki

【Source】IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES

【影响因子】0.423

【Abstract】Smart contracts are protocols that can automatically execute a transaction including an electronic contract when a condition is satisfied without a trusted third party. In a representative use-case, a smart contract is executed when multiple parties fairly trade on a blockchain asset. On blockchain systems, a smart contract can be regarded as a system participant, responding to the information received, receiving and storing values, and sending information and values outwards. Also, a smart contract can temporarily keep assets, and always perform operations in accordance with prior rules. Many cryptocurrencies have implemented smart contracts. At POST2018, Atzei et al. give formulations of seven fair exchange protocols using smart contract on Bitcoin: oracle, escrow, intermediated payment, timed commitment, micropayment channels, fair lotteries, and contingent payment. However, they only give an informal discussion on security. In this paper, we verify the fairness of their seven protocols by using the formal verification tool ProVerif. As a result, we show that five protocols (the oracle, intermediated payment, timed commitment, micropayment channels and fair lotteries protocols) satisfy fairness, which were not proved formally. Also, we re-find known attacks to break fairness of two protocols (the escrow and contingent payment protocols). For the escrow protocol, we formalize the two-party scheme and the three-party scheme with an arbitrator, and show that the two-party scheme does not satisfy fairness as Atzei et al. showed. For the contingent payment protocol, we formalize the protocol with the non-interactive zero-knowledge proof (NIZK), and re-find the attack shown by Campanelli et al. at CCS 2017. Also, we show that a countermeasure with subversion NIZK against the attack works properly while it is not formally proved.

【Keywords】formal methods; smart contracts; fairness; ProVerif

【发表时间】2022 MAR

【收录时间】2022-03-21

【文献类型】期刊

【主题类别】

区块链技术-智能合约-