Formal Analysis And Verificaiton Of Blockchain Currency Mixing Mechanism Protocol Witn Model Checking

Blockchain is a change to the traditional Internet,known as the next generation of the Internet.As a cryptographic currency in blockchain,mixed currency in blockchain has paid much attention and applied in blockchain fields.However,because of the existence of a third party in the mixed currency,it faces the same security problems as the traditional centralized system and a trusted third party may leak the connection between the mixed currency addresses,which makes the operation of the mixed currency mechanism meaningless.The protocol of mixed currency mechanism is the key method to guarantee the security and privacy of blockchain.Blockchain mixed currency mechanism protocol is an anonymous communication protocols,formal analysis anonymity of blockchain mixed currency mechanism protocol is still in the development stage.MIXCOIN protocol is a typical blockchain coin mixing mechanism protocol.Aiming at the problem that MIXCOIN protocol may leak user address correlation,as a result it does not meet the requirements of anonymity.This paper proposes a formal method based on model detection to study the anonymity security of MIXCOIN protocol.The main work of this paper is as follows:(1)Propose a formal abstract representation method of MIXCOIN protocol.Assuming that the cryptographic system used by the protocol is complete,the method first simplifies the number of entities in the MIXCOIN protocol,then reduce the expression of the encryption and decryption key string,and finally defines the bitcoin transfer function.By this method,it is difficult to use formal analysis and formal representation for MIXCOIN protocols.(2)Improve the modeling method of Dolev-Yao attackers.This method can better analyze the anonymous communication protocol by introducing the adversary control channel and extending the network communication hypothesis.The improved Dolev-Yao attacker modeling method is used to model the MIXCOIN protocol and linear temporal logic is used to describe the protocol properties.SPIN,a model detection tool,is used to verify the protocol,and an attack sequence diagram is generating to illustrate that the MIXCOIN protocol does not satisfy anonymity.(3)Improve based on the blind signature mechanism of elliptic curve and array mode,an improved method for blind signature and public key address update of MIXCOIN protocol key information.Based on the elliptic curve blind signature mechanism,this method introduces the auxiliary process channel operation,which realizes the protocol blind signature operation and the array method is using to simulate the public key address updating operation,and can better analyze and improve the protocol.MIXCOIN protocol adds blind signature operation to the message item and using array to simulate the implementation of public key address update operation,and uses adversary control channel to model the improved MIXCOIN protocol.By SPIN verification,the experiment shows that the improved MIXCOIN protocol is safe and more anonymous.The proposed MIXCOIN protocol formal abstract representation method and the improved Dolev-Yao attacker modeling method have important meaning for the formal analysis of this kind of blockchain mixed currency mechanism protocol.This paper proposes an improved method of blind signature of key protocol information by using elliptic curve blind signature mechanism and simulate the implementation of array public key address update,and introduces the auxiliary process channel to realize the blind signature operation,which proves that it can improve the anonymity of protocol sender.It is used for the design and analysis of this kind of blockchain mixed currency mechanism protocol.