Research Of Analyzing E-commerce Protocols Based On Colored Petri Nets

With the rapid development of Internet, e-commerce has been deep into every cornerof the society. How to confirm an e-commerce transaction safe and reliable has become animportant research topic. E-commerce protocol is a protocol to ensure that e-commercetransactions carry out properly. E-commerce protocol should not only satisfy theproperties of security protocols but also satisfy special properties such as accountability,fairness and timeliness. Formal analysis is an effective tool of e-commerce protocol whichcan easily and exactly find the defects in it. In this paper, an e-commerce protocolmodeling method based on colored Petri nets is proposed which can model three importantsecurity propertie. The attacks are modeled and analyzed.First, an e-commerce protocol modeling method based on senior net colored Petri netis proposed which can model three important security properties as accountability, fairness,and timeliness. On the basic of accountability and fairness model, timeliness which iscomplex and hard is added to the model. A model with timeliness is established. Reversestate analyzing method is used to analyze the model. Improved ZG protocol KZG protocolis taken as an example in this chapter. With the modeling method we propose, a coloredPetri net model of KZG protocol is established. After the analysis of the model, we findthat KZG protocol satisfies accountability, fairness and timeliness.Second, insecure state of e-commerce protocols is studied. We extract from EOO andEOR to define the insecure state of the protocol. This deals with the difficulty in defininginsecure state. A modeling method to model the protocol with intruders is proposed. Withthe reverse state analysis, whether the insecure state is approachable is analyzed. CMP1protocol is taken as an example. An insecure state is found.Finally, CPN Tools is taken to testify KZG and CMP1’s colored Petri net models areanalyzed in the CPN Tools.