The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Les contrats intelligents sont des protocoles qui peuvent exécuter automatiquement une transaction, y compris un contrat électronique, lorsqu'une condition est remplie sans tiers de confiance. Dans un cas d’utilisation représentatif, un contrat intelligent est exécuté lorsque plusieurs parties négocient équitablement un actif blockchain. Sur les systèmes blockchain, un contrat intelligent peut être considéré comme un participant au système, répondant aux informations reçues, recevant et stockant des valeurs, et envoyant des informations et des valeurs vers l'extérieur. De plus, un contrat intelligent peut conserver temporairement des actifs et toujours effectuer des opérations conformément aux règles antérieures. De nombreuses cryptomonnaies ont mis en place des contrats intelligents. Lors du POST2018, Atzei et al. donnent des formulations de sept protocoles d'échange équitables utilisant des contrats intelligents sur Bitcoin : oracle, séquestre, paiement intermédié, engagement chronométré, canaux de micropaiement, loteries équitables et paiement conditionnel. Cependant, ils ne donnent qu’une discussion informelle sur la sécurité. Dans cet article, nous vérifions l'équité de leurs sept protocoles en utilisant l'outil de vérification formelle ProVerif. En conséquence, nous montrons que cinq protocoles (l'oracle, le paiement intermédié, l'engagement temporisé, les canaux de micropaiement et les protocoles de loteries équitables) satisfont à l'équité, ce qui n'a pas été formellement prouvé. En outre, nous retrouvons des attaques connues visant à briser l'équité de deux protocoles (les protocoles de séquestre et de paiement conditionnel). Pour le protocole de séquestre, nous formalisons le schéma bipartite et le schéma tripartite avec un arbitre, et montrons que le schéma bipartite ne satisfait pas à l'équité comme Atzei et al. montré. Pour le protocole de paiement contingent, nous formalisons le protocole avec la preuve non interactive de connaissance nulle (NIZK), et retrouvons l'attaque montrée par Campanelli et al. au CCS 2017. Nous montrons également qu'une contre-mesure avec subversion NIZK contre l'attaque fonctionne correctement alors qu'elle n'est pas formellement prouvée.
Cheng SHI
Ibaraki University
Kazuki YONEYAMA
Ibaraki University
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
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
Copier
@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},}
Copier
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 -