Formal Modeling And Verification Of Supply Chain Smart Contract Based On Game Theory

Blockchain,which emerges in the 21 st century,has the characteristics of unforgeability and decentralization,and has great potential in the field of information technology and finance.Smart contract is an critical technical support of blockchain,once smart contract which is defective deployed will cause immeasurable losses due its features of mandatory of execution and irreversibility of transaction.Therefore,the high reliability of smart contract must be guaranteed prior to the deployment of smart contract.Contract logic is an important factor affecting the high reliability of smart contracts,so ensuring the rationality of smart contract logic has become a key issue.Due to its rigorous mathematical model and reliable logic analysis,formal verification provides an important technical means for the logical rationality verification of smart contracts,and has become a research hotspot in the field of blockchain.This paper proposes a formal modeling and verification method for supply chain smart contracts based on game theory,which can simulate and verify whether the game results of supply chain entities are consistent with the execution results of smart contracts before the deployment of smart contracts to detect their logical rationality.The main contents are as follows:(1)Aiming at the potential risks in the smart contract logic,a supply chain smart contract model based on game theory is proposed to verify the rationality of its game-related logic.This paper redefines the return function by introducing distortion technology,and realizes the two-party supply chain game.In the pure strategy game,the influence of the Nash equilibrium and the discount factor on the multi-round game is analyzed.At the same time,the factors,including penalty strategy,subjective attitude of participation and environmental factors,that affect the game are discussed in the mixed strategy game,and calculated the Nash equilibrium.In addition,combining game theory and formal methods,a discrete-time Markov game model is established,and some attributes related to game results in the model are verified by probabilistic model checking tools,which provides guidance for the optimization of smart contracts.(2)The equilibrium solution of the two-party game is not necessarily the optimal solution of the supply chain system.The intervention of a third-party regulatory agency is conducive to optimizing the equilibrium solution.Based on the two-party game,this paper introduces a supply chain supervisory agency,and then proposes a three-party supply chain smart contract model based on evolutionary game.Through the reward and punishment strategy of the supervisor,the three-party revenue function is proposed,and the three-dimensional revenue matrix of the game is designed.The expected return in the game and the dynamic replication equation are calculated,the evolutionary equilibrium point is solved and its influencing factors are analyzed.Subsequently,probabilistic model detection is used to model the uncertainty in the behavior of participants,to verify the consistency of the model game results with theoretical analysis,and to provide guidance for the optimization of supply chain contracts.(3)This paper uses an example of supply chain smart contract,combined with theoretical analysis and formal verification method,to carry out experiments and analysis for case example from the four aspects of modeling,simulation,verification and deployment.Finally,through the effectiveness analysis,the usability of the research results in practical application is verified.