{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T09:33:44Z","timestamp":1761989624767},"reference-count":39,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Fundamentals"],"published-print":{"date-parts":[[2022,3,1]]},"DOI":"10.1587\/transfun.2021cip0005","type":"journal-article","created":{"date-parts":[[2021,10,24]],"date-time":"2021-10-24T22:09:37Z","timestamp":1635113377000},"page":"242-267","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Fair Exchange Based on Bitcoin Smart Contracts"],"prefix":"10.1587","volume":"E105.A","author":[{"given":"Cheng","family":"SHI","sequence":"first","affiliation":[{"name":"Ibaraki University"}]},{"given":"Kazuki","family":"YONEYAMA","sequence":"additional","affiliation":[{"name":"Ibaraki University"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] C. Shi and K. Yoneyama, \u201cFormal verification of fair exchange based on Bitcoin smart contracts,\u201d INDOCRYPT 2020, pp.89-106, 2020. 10.1007\/978-3-030-65277-7_5","DOI":"10.1007\/978-3-030-65277-7_5"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] N. Szabo, \u201cFormalizing and securing relationships on public networks,\u201d First Monday, vol.2, no.9, Sept. 1997. 10.5210\/fm.v2i9.548","DOI":"10.5210\/fm.v2i9.548"},{"key":"3","doi-asserted-by":"crossref","unstructured":"[3] N. Atzei, M. Bartoletti, S. Lande, and R. Zunino, \u201cA formal model of Bitcoin transactions,\u201d Financial Cryptography 2018, pp.541-560, 2018. 10.1007\/978-3-662-58387-6_29","DOI":"10.1007\/978-3-662-58387-6_29"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] N. Atzei, M. Bartoletti, T. Cimoli, S. Lande, and R. Zunino, \u201cSoK: Unraveling Bitcoin smart contracts,\u201d POST 2018, pp.217-242, 2018. 10.1007\/978-3-319-89722-6_9","DOI":"10.1007\/978-3-319-89722-6_9"},{"key":"5","unstructured":"[5] B. Garbinato and I. Rickebusch, \u201cImpossibility results on fair exchange,\u201d IICS 2010, pp.507-518, 2010."},{"key":"6","unstructured":"[6] \u201cProVerif 2.00,\u201d http:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] R. Bresciani and A. Butterfield, \u201cProVerif analysis of the ZRTP protocol,\u201d International Journal for Infonomics (IJI), vol.3, no.3, pp.1060-1064, 2010. 10.20533\/iji.1742.4712.2010.0033","DOI":"10.20533\/iji.1742.4712.2010.0033"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] S. Asadi and H.S. Shahhoseini, \u201cFormal security analysis of authentication in SNMPv3 protocol by an automated tool,\u201d IST 2012, pp.306-313, 2012. 10.1109\/istel.2012.6483143","DOI":"10.1109\/ISTEL.2012.6483143"},{"key":"9","doi-asserted-by":"crossref","unstructured":"[9] K. Ammayappan, \u201cSeamless interoperation of LTE-UMTS-GSM requires flawless UMTS and GSM,\u201d International Conference on Advanced Computing, Networking and Security, pp.169-174, 2013. 10.1109\/adcons.2013.53","DOI":"10.1109\/ADCONS.2013.53"},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] N.B. Henda and K. Norrman, \u201cFormal analysis of security procedures in LTE \u2014 A feasibility study,\u201d Research in Attacks, Intrusions and Defenses 2014, pp.341-361, 2014. 10.1007\/978-3-319-11379-1_17","DOI":"10.1007\/978-3-319-11379-1_17"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] J. Lu, J. Zhang, J. Li, Z. Wan, and B. Meng, \u201cAutomatic verification of security of OpenID connect protocol with ProVerif,\u201d 3PGCIC 2016, pp.209-220, 2016. 10.1007\/978-3-319-49109-7_20","DOI":"10.1007\/978-3-319-49109-7_20"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] H. Sakurada, K. Yoneyama, Y. Hanatani, and M. Yoshida, \u201cAnalyzing and fixing the QACCE security of QUIC,\u201d SSR 2016, pp.1-31, 2016. 10.1007\/978-3-319-49100-4_1","DOI":"10.1007\/978-3-319-49100-4_1"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] K. Bhargavan, B. Blanchet, and N. Kobeissi, \u201cVerified models and reference implementations for the TLS 1.3 standard candidate,\u201d IEEE Symposium on Security and Privacy 2017, pp.483-502, 2017. 10.1109\/sp.2017.26","DOI":"10.1109\/SP.2017.26"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] N. Kobeissi, K. Bhargavan, and B. Blanchet, \u201cAutomated verification for secure messaging protocols and their implementations: A symbolic and computational approach,\u201d EuroS&P 2017, pp.435-450, 2017. 10.1109\/eurosp.2017.38","DOI":"10.1109\/EuroSP.2017.38"},{"key":"15","unstructured":"[15] C. Cremers, \u201cThe scyther tool,\u201d https:\/\/people.cispa.io\/cas.cremers\/scyther\/"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] N. Kobeissi, G. Nicolas, and M. Tiwari, \u201cVerifpal: Cryptographic protocol analysis for the real world,\u201d INDOCRYPT 2020, pp.151-202, 2020. 10.1007\/978-3-030-65277-7_8","DOI":"10.1007\/978-3-030-65277-7_8"},{"key":"17","unstructured":"[17] B. Schmidt, S. Meier, C. Cremers, and D. Basin, \u201cTamarin prover,\u201d http:\/\/tamarin-prover.github.io\/"},{"key":"18","unstructured":"[18] B. Blanchet, \u201cCryptoVerif: Cryptographic protocol verifier in the computational model,\u201d https:\/\/bblanche.gitlabpages.inria.fr\/CryptoVerif\/"},{"key":"19","doi-asserted-by":"publisher","unstructured":"[19] C. Cremers and M. Horvat, \u201cImproving the ISO\/IEC 11770 standard for key management techniques,\u201d Int. J. Inf. Sec., vol.15, no.6, pp.659-673, 2016. 10.1007\/s10207-015-0306-9","DOI":"10.1007\/s10207-015-0306-9"},{"key":"20","unstructured":"[20] \u201cISO\/IEC 11770-2:2018-IT Security techniques-Key management-Part 2: Mechanisms using symmetric techniques,\u201d https:\/\/www.iso.org\/standard\/73207.html"},{"key":"21","unstructured":"[21] \u201cISO\/IEC 11770-3:2015-Information technology-Security techniques-Key management-Part 3: Mechanisms using asymmetric techniques,\u201d https:\/\/www.iso.org\/standard\/60237.html"},{"key":"22","doi-asserted-by":"crossref","unstructured":"[22] C. Cremers, \u201cKey exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2,\u201d ESORICS 2011, pp.315-334, 2011. 10.1007\/978-3-642-23822-2_18","DOI":"10.1007\/978-3-642-23822-2_18"},{"key":"23","doi-asserted-by":"publisher","unstructured":"[23] D. Basin, C. Cremers, and S. Meier, \u201cProvably repairing the ISO\/IEC 9798 standard for entity authentication,\u201d J. Computer Security, vol.21, no.6, pp.817-846, 2013. 10.3233\/jcs-130472","DOI":"10.3233\/JCS-130472"},{"key":"24","doi-asserted-by":"crossref","unstructured":"[24] C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe, \u201cA comprehensive symbolic analysis of TLS 1.3,\u201d CCS 2017, pp.1773-1788, 2017. 10.1145\/3133956.3134063","DOI":"10.1145\/3133956.3134063"},{"key":"25","doi-asserted-by":"crossref","unstructured":"[25] C. Cremers and M. Dehnel-Wild, \u201cComponent-based formal analysis of 5G-AKA: Channel assumptions and session confusion,\u201d NDSS 2019, 2019. 10.14722\/ndss.2019.23394","DOI":"10.14722\/ndss.2019.23394"},{"key":"26","doi-asserted-by":"publisher","unstructured":"[26] C. Cremers, M. Dehnel-Wild, and K. Milner, \u201cSecure authentication in the grid: A formal analysis of DNP3: SAv5,\u201d J. Computer Security, vol.27, no.2, pp.203-232, 2019. 10.3233\/jcs-181139","DOI":"10.3233\/JCS-181139"},{"key":"27","doi-asserted-by":"crossref","unstructured":"[27] M. Backes, J. Dreier, S. Kremer, and R. K\u00fcnnemann, \u201cA novel approach for reasoning about liveness in cryptographic protocols and its application to fair exchange,\u201d EuroS&P 2017, pp.76-91, 2017. 10.1109\/eurosp.2017.12","DOI":"10.1109\/EuroSP.2017.12"},{"key":"28","unstructured":"[28] G. Maxwell, \u201cZero knowledge contingent payment,\u201d 2011."},{"key":"29","unstructured":"[29] S. Bowe, \u201cPay-to-sudoku,\u201d https:\/\/github.com\/zcash\/pay-to-sudoku, 2016."},{"key":"30","doi-asserted-by":"crossref","unstructured":"[30] M. Campanelli, R. Gennaro, S. Goldfeder, and L. Nizzardo, \u201cZero-knowledge contingent payments revisited: Attacks and payments for services,\u201d ACM Conference on Computer and Communications Security 2017, pp.229-243, 2017. 10.1145\/3133956.3134060","DOI":"10.1145\/3133956.3134060"},{"key":"31","doi-asserted-by":"crossref","unstructured":"[31] L. Luu, D.H. Chu, H. Olickel, P. Saxena, and A. Hobor, \u201cMaking smart contracts smarter,\u201d ACM Conference on Computer and Communications Security 2016, pp.254-269, 2016. 10.1145\/2976749.2978309","DOI":"10.1145\/2976749.2978309"},{"key":"32","doi-asserted-by":"crossref","unstructured":"[32] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, and S.Z. B\u00e9guelin, \u201cFormal verification of smart contracts: Short paper,\u201d PLAS@CCS 2016, pp.91-96, 2016. 10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"key":"33","doi-asserted-by":"crossref","unstructured":"[33] S. Kalra, S. Goel, M. Dhawan, and S. Sharma, \u201cZEUS: Analyzing safety of smart contracts,\u201d NDSS 2018, 2018. 10.14722\/ndss.2018.23082","DOI":"10.14722\/ndss.2018.23082"},{"key":"34","unstructured":"[34] \u201cCrowdFundDAO,\u201d https:\/\/live.ether.camp\/account\/9b37508b5f859682382d8cb6467a5c7fc5d02e9c\/contract"},{"key":"35","unstructured":"[35] \u201cDiceRoll,\u201d https:\/\/ropsten.etherscan.io\/address\/0xb95bbe8ee98a21b5ef7778ec1bb5910ea843f8f7"},{"key":"36","unstructured":"[36] \u201cStandardToken,\u201d https:\/\/git.io\/vFAlg"},{"key":"37","unstructured":"[37] \u201cWallet,\u201d https:\/\/etherscan.io\/address\/0xab7c74abc0c4d48d1bdad5dcb26153fc8780f83e"},{"key":"38","doi-asserted-by":"crossref","unstructured":"[38] M. Bellare, G. Fuchsbauer, and A. Scafuro, \u201cNIZKs with an untrusted CRS: Security in the face of parameter subversion,\u201d ASIACRYPT (2) 2016, pp.777-804, 2016. 10.1007\/978-3-662-53890-6_26","DOI":"10.1007\/978-3-662-53890-6_26"},{"key":"39","doi-asserted-by":"publisher","unstructured":"[39] O. Goldreich and Y. Oren, \u201cDefinitions and properties of zero-knowledge proof systems,\u201d J. Cryptol., vol.7, no.1, pp.1-32, 1994. 10.1007\/bf00195207","DOI":"10.1007\/BF00195207"}],"container-title":["IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transfun\/E105.A\/3\/E105.A_2021CIP0005\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,5]],"date-time":"2022-03-05T03:18:45Z","timestamp":1646450325000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transfun\/E105.A\/3\/E105.A_2021CIP0005\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,1]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022]]}},"URL":"https:\/\/doi.org\/10.1587\/transfun.2021cip0005","relation":{},"ISSN":["0916-8508","1745-1337"],"issn-type":[{"value":"0916-8508","type":"print"},{"value":"1745-1337","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,1]]},"article-number":"2021CIP0005"}}