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
스마트 계약은 신뢰할 수 있는 제2018자 없이 조건이 충족되면 전자 계약을 포함한 거래를 자동으로 실행할 수 있는 프로토콜입니다. 대표적인 사용 사례에서는 여러 당사자가 블록체인 자산을 공정하게 거래할 때 스마트 계약이 실행됩니다. 블록체인 시스템에서 스마트 계약은 수신된 정보에 응답하고, 값을 수신 및 저장하고, 정보와 값을 외부로 보내는 시스템 참가자로 간주될 수 있습니다. 또한 스마트 계약은 자산을 일시적으로 보관하고 항상 사전 규칙에 따라 작업을 수행할 수 있습니다. 많은 암호화폐가 스마트 계약을 구현했습니다. POST2017에서 Atzei et al. 비트코인의 스마트 계약을 사용하여 오라클, 에스크로, 중간 지불, 정기 약정, 소액 지불 채널, 공정 복권 및 조건부 지불 등 XNUMX가지 공정한 교환 프로토콜을 공식화합니다. 그러나 그들은 보안에 관해 비공식적인 논의만을 제공합니다. 본 논문에서는 공식 검증 도구인 ProVerif를 사용하여 XNUMX개 프로토콜의 공정성을 검증합니다. 그 결과, 우리는 공식적으로 입증되지 않았던 XNUMX가지 프로토콜(오라클, 중개 지불, 시간 약속, 소액 지불 채널 및 공정한 복권 프로토콜)이 공정성을 충족한다는 것을 보여줍니다. 또한 두 프로토콜(에스크로 및 조건부 지불 프로토콜)의 공정성을 깨뜨리는 알려진 공격을 다시 찾아냅니다. 에스크로 프로토콜의 경우 중재인을 통한 XNUMX자 방식과 XNUMX자 방식을 공식화하였고, Atzei et al.과 같이 XNUMX자 방식은 공정성을 만족하지 못함을 보여주었다. 보여 주었다. 조건부 지불 프로토콜의 경우 비대화형 영지식 증명(NIZK)으로 프로토콜을 공식화하고 Campanelli et al.이 보여준 공격을 다시 찾습니다. 또한 CCS XNUMX에서 공격에 대한 전복 NIZK 대응책이 공식적으로 입증되지는 않았지만 제대로 작동함을 보여줍니다.
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.
부
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
부
@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},}
부
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 -