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

【Author】 Bao, Xianglin; Xu, Xiaofeng; Zhang, Ping; Liu, Tao

【Source】IEEE ACCESS

【影响因子】3.476

【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.

【Keywords】Bitcoin; Blindcoin; formal analysis; protocol vulnerabilities; symbolic model

【发表时间】2022

【收录时间】2022-12-23

【文献类型】理论模型

【主题类别】

区块链治理-技术治理-漏洞检测