Formal Analysis Of E-commerce Protocols

The growing popularity of the Internet has made the electronic transactions over the Internet a new promising shopping model. And the correspondent e-commerce protocols are the keys to make sure that the new exchange model runs smoothly. In the Internet environ-ment, the guarantee of security, atomicity, privacy and anonymity is essential to the wide application of e-commerce. The formal method provides an effective way to describe the protocols and analyze the properties of concern.As one kind of the most important security protocols, e-commerce protocols not only possess the common properties like other security protocols, but also have their own unique properties. In this paper, we first introduce the formal methods for security protocols and the research development in this field. We devote much effort in model checking which is one of the most important formal methods. we briefly describe some typical e-commerce exchange protocols. Some properties like anonymity, non-repudiation, fairness and security are also summarized and discussed.At last we take one concrete e-commerce protocol as an example. We use CSP as the modeling language to model the protocol and the fairness properties (money atomicity, goods atomicity and validated receipt). Then the protocol is verified against the properties by FDR based on the finite state machine concept. We also introduce two kinds of failures into the protocol and demonstrate how the fair properties can be violated in the presence of certain failures. The analysis of the violation scenario can be used to suggest some mechanism to deal with certain failures and make the protocol more robust.