| Bitcoin is the most popular de-centralized electronic cryptocurrency in the global market,relying on the bitcoin protocols to protect its users from attacks.However,the security guarantees declared by bitcoin are not required by the authority to give profes-sional and faithful security verification,which makes it difficult for the public to objec-tively evaluate the security of bitcoin.In order to study the security of bitcoin,its con-sensus protocol is formally analyzed by the existing works based on computational meth-ods.However,due to the difficulty of protocol modeling and formal analysis brought by computational methods,the existing works complete the manual proof and derivation of the properties of bitcoin consensus-security through over-simplified abstraction,with-out regard for the execution details of other bitcoin protocols and their combinations.But the over-simplified abstraction of protocol modeling can hide the vulnerabilities in bitcoin protocol that the malicious can leverage.So,it is necessary to carry on a more detailed and systematic security analysis of bitcoin without over-simplification.This pa-per abstracts the payment module,consensus module,cooperative mining module,and cross-chain trading module of bitcoin protocols and their entity interactions,along with the design of bitcoin adversary model and security goals,to model bitcoin protocols in symbolic approach.This paper completes the automatic verification of our fine-grained bitcoin symbolic model.The main works of this paper are as follows:1.The systematic abstraction of the bitcoin protocol modules and their entity inter-actions.In order to abstract protocol interactions within each protocol module and be-tween modules,this paper fine-grained abstract payment protocol,consensus protocol,stratum protocol,and interledger protocol along with their protocol entities.Compared to the previous work only considering consensus protocol and the node as the bitcoin entity,this paper considers five bitcoin entities and four protocol modules based on the bitcoin source codes and the related documents to allow our systematic formal analysis of the bitcoin security.The bitcoin entities and the entity interactions within each mod-ule and between modules are abstracted in detail,so both the security of each bitcoin protocol and their combination can be verified in this paper.2.Fine-grained design of bitcoin attacker model and security goals.Given that bitcoin documents do not provide an accurate definition of its attacker model,this pa-per design the bitcoin attacker abilities with proper security assumption based on the extended Dolev-Yao attacker model.For bitcoin security goals,only privacy and ac-countability are mentioned in the bitcoin white paper without clear definitions.In this paper,the security goals of bitcoin protocols are precisely defined according to the ac-tual security requirements of bitcoin protocol entities,including the security proper-ties of authentication,privacy,accountability,and balance consistency.These security properties are used to verify whether the injective agreement between protocol entities can be satisfied,whether the relationship between transaction address and real identity can be deduced,whether each malicious entity can be identified without any mistaken judgment and miss judgment,and whether the spent bitcoin can be used to forge the double-spent transactions.3.Symbolic modeling for bitcoin protocols which is suitable for automatic for-mal verification.This paper formalizes the bitcoin protocol modules and their entity interaction into a set of axioms of the symbolic model.Based on the abstraction of the bitcoin protocol module along with the design of the bitcoin attacker model and security goals,this paper formalizes the communication between bitcoin entities as model rules and bitcoin security goals as model lemmas to be proved.With the help of the formal verification tool SmartVerif,the reasoning of bitcoin model rules and the verification of bitcoin model lemmas are completed automatically with our balancing of the reasoning difficulty and our fine-grained modeling.The formal verification experiments of this paper prove the security goals that bitcoin protocols do not satisfied,and the unmet se-curity goals when considering the interactions between bitcoin protocol modules.The implementable bitcoin attacks are stated in this paper,including the hotly-discussed at-tacks and the ones that have not been formally analyzed.This paper provides temporary suggestions for bitcoin entities to prevent these attacks. |
PDF Full Text Request