Formal Verification of Fair Exchange Based on Bitcoin Smart Contracts

Cheng SHI; Kazuki YONEYAMA

doi:10.1587/transfun.2021CIP0005

IEICE TRANSACTIONS on Fundamentals

Formal Verification of Fair Exchange Based on Bitcoin Smart Contracts

Cheng SHI, Kazuki YONEYAMA

Full Text Views

0

Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E105-A No.3 pp.242-267

Publication Date: 2022/03/01

Publicized: 2021/10/25

Online ISSN: 1745-1337

DOI: 10.1587/transfun.2021CIP0005

Type of Manuscript: Special Section PAPER (Special Section on Cryptography and Information Security)

Category

Authors

Cheng SHI
Ibaraki University
Kazuki YONEYAMA
Ibaraki University

Keyword

formal methods, smart contracts, fairness, ProVerif

Cite this

Copy

Cheng SHI, Kazuki YONEYAMA, "Formal Verification of Fair Exchange Based on Bitcoin Smart Contracts" in IEICE TRANSACTIONS on Fundamentals, vol. E105-A, no. 3, pp. 242-267, March 2022, doi: 10.1587/transfun.2021CIP0005.
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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.2021CIP0005/_p

Copy

@ARTICLE{e105-a_3_242,
author={Cheng SHI, Kazuki YONEYAMA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Formal Verification of Fair Exchange Based on Bitcoin Smart Contracts},
year={2022},
volume={E105-A},
number={3},
pages={242-267},
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={},
doi={10.1587/transfun.2021CIP0005},
ISSN={1745-1337},
month={March},}

Copy

TY - JOUR
TI - Formal Verification of Fair Exchange Based on Bitcoin Smart Contracts
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 242
EP - 267
AU - Cheng SHI
AU - Kazuki YONEYAMA
PY - 2022
DO - 10.1587/transfun.2021CIP0005
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E105-A
IS - 3
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - March 2022
AB - 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.
ER -

IEICE TRANSACTIONS on Fundamentals