New Approach for Analyzing of E-commerce Protocol
一种新的电子商务协议分析方法

This paper presented an extended CSFM by combining communication finite state machine(CSFM) with some new logic rules based on Qing-Zhou logic to analyze security properties of E-commerce protocols. It not only can describe the knowledge and behavior of participants, but also analyze the security properties without initial state assumptions. In addition, this method enables us to verity other security properties after abstracting and modifying the model. Using this method,accountability,fairness and atomicity were analyzed to be satisfied in the anonymous and failure resilient fair-exchange ecommerce protocol. Then UPPAAL was used to verify the properties of fairness, liveness and timeliness.