Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness

To enhance the efficiency of time security verification and fairness verification of auction contracts, an abstract modeling and verification method for role-based auction contracts was proposed. Firstly, the source code of the contract was abstractly modeled based on account roles and converted into a timed automaton network model. Formal descriptions of time security were provided and verified using the UPPAAL tool. Secondly, the mechanisms in the source code of the contract were extracted to establish a smart contract mechanism model, which was also converted into a timed automaton network model. Formal descriptions of four types of fairness were provided and verified using UPPAAL. Finally, the feasibility and effectiveness of the proposed method were demonstrated through two classic cases.