Formalization and Verification of Data Auction Mechanism Based on Smart Contract Using CSP

Nowadays, the utilization of online auction platforms is becoming increasingly prevalent. Online auction provides a common and practical way for global buyers to compete fairly. Nevertheless, the anonymous environment may bring collusion among entities with effects on results. Compared with traditional mechanisms which rely on third-party platforms, the data auction based on smart contract can create a decentralized environment to avoid the occurrence of collusion. Meanwhile, there exists few research on the verification of its reliability and safety which is worth investigating from the perspective of formal methods. In this paper, we apply Process Algebra CSP in modeling the data auction communicating system among five key entities. In addition, we use Process Analysis Toolkit (PAT) to realize the mechanism and verify five crucial properties, including deadlock freedom, data reachability, data correctness, anti-collusion capability and data security. The verification results indicate that the architecture of data auction based on smart contract can satisfy all the above requirements. Especially, the design of asymmetric encryption for the fundamental information ensures the non-occurrence of collusion in the auction. Additionally, the digital signature generated by private key attached to the message guarantees the safety of the interaction.