A Combining Deterministic Finite Automaton With Logic Rules Approach For Analyzing Of E-commerce Protocol

In recent years, e-commerce has got an unprecedented development, and the securityof e-commerce has been paid more attention. The e-commerce protocol is an importantguarantee for e-commerce activities. To ensure the correctness and security of e-commerceprotocols, formal analysis methods are needed to analyze e-commerce protocols and findtheir defects. Currently model checking and logical analysis are popular formal methods,but both of them have Limitations. In this paper model checking and logical analysis weredeeply studied, and based the study a new formal analysis method was raised.Firstly, existing formal analysis methods of e-commerce protocols were deeplystudied. Model checking and logical analysis are two of common formal analysis methods.In this paper the advantages and disadvantages of the two methods were found.Secondly, based on the advantages and disadvantages of model checking and logicalanalysis, a new formal analysis method was raised. This method could analyze manysecurity properties of e-commerce protocols such as accountability, fairness and timeliness,and could give the state transition diagram which can describe the running process ofprotocols, and could correctly analyze the property when the replay attack occurs.Thirdly, when the new formal analysis method was used to analyze CMP1protocol,many defects such as exposed ciphertext and replay attacks were found, so an improvedCMP1protocol was raised in this paper. The improved CMP1protocol satisfied securityproperties of accountability, fairness and timeliness, and had no replay attacks.Lastly, the model-checking tool UPPAAL was used to verify that the analysis of KZGprotocol, CMP1protocol and CMP1protocol was correct.