Comprehensive Formal Modeling and Automatic Vulnerability Detection for a Bitcoin-Compatible Mixing Protocol

Bao, X; Xu, X; Zhang, P; Liu, T

Comprehensive Formal Modeling and Automatic Vulnerability Detection for a Bitcoin-Compatible Mixing Protocol

Bao, X Xu, X

Zhang, P Liu, T

Permalink

Publisher:: IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
Publication Type:: Journal Article
Citation:: IEEE Access, 2022, 10, pp. 128847-128873
Issue Date:: 2022-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Published versionAdobe PDF (9.39 MB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Bao, X
dc.contributor.author	Xu, X https://orcid.org/0000-0002-3674-199X
dc.contributor.author	Zhang, P
dc.contributor.author	Liu, T
dc.date.accessioned	2023-03-21T01:02:59Z
dc.date.available	2023-03-21T01:02:59Z
dc.date.issued	2022-01-01
dc.identifier.citation	IEEE Access, 2022, 10, pp. 128847-128873
dc.identifier.issn	2169-3536
dc.identifier.issn	2169-3536
dc.identifier.uri	http://hdl.handle.net/10453/167870
dc.description.abstract	Blindcoin applies a Bitcoin-compatible mixing protocol with a blind signature scheme to improve the design of the popular Mixcoin. Given the openness of Bitcoin and the decentralization of the P2P network, it is imperative to formally analyze whether the malicious can break the security goals of the Blindcoin protocol. This work proposes a symbolic model for Blindcoin and conducts comprehensive formal verification. Fine-grained security goals of Blindcoin are formalized and subsequently encoded as model lemmas. However, it is challenging to verify the Blindcoin in a formal and automatic way. To tackle the challenges, we propose a tool-friendly symbolic model that can capture the semantics of multi-layers of Bitcoin and the features of Blindcoin. Our formal verification covers real-world security scenarios and discovers the Blindcoin vulnerabilities without human interaction. Furthermore, we offer several suggestions to fix the detected Blindcoin vulnerabilities and discuss the generalization of the proposed model.
dc.language	English
dc.publisher	IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
dc.relation.ispartof	IEEE Access
dc.relation.isbasedon	10.1109/ACCESS.2022.3228109
dc.rights	info:eu-repo/semantics/openAccess
dc.subject	08 Information and Computing Sciences, 09 Engineering, 10 Technology
dc.title	Comprehensive Formal Modeling and Automatic Vulnerability Detection for a Bitcoin-Compatible Mixing Protocol
dc.type	Journal Article
utslib.citation.volume	10
utslib.for	08 Information and Computing Sciences
utslib.for	09 Engineering
utslib.for	10 Technology
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
utslib.copyright.status	open_access	*
dc.date.updated	2023-03-21T01:02:57Z
pubs.publication-status	Published
pubs.volume	10

Abstract:

Blindcoin applies a Bitcoin-compatible mixing protocol with a blind signature scheme to improve the design of the popular Mixcoin. Given the openness of Bitcoin and the decentralization of the P2P network, it is imperative to formally analyze whether the malicious can break the security goals of the Blindcoin protocol. This work proposes a symbolic model for Blindcoin and conducts comprehensive formal verification. Fine-grained security goals of Blindcoin are formalized and subsequently encoded as model lemmas. However, it is challenging to verify the Blindcoin in a formal and automatic way. To tackle the challenges, we propose a tool-friendly symbolic model that can capture the semantics of multi-layers of Bitcoin and the features of Blindcoin. Our formal verification covers real-world security scenarios and discovers the Blindcoin vulnerabilities without human interaction. Furthermore, we offer several suggestions to fix the detected Blindcoin vulnerabilities and discuss the generalization of the proposed model.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/167870