Abstract: 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.

Key words: E-commerce protocol, Model checking, Logic proving, Communication finite state machine