A formal method which can be used to analyze security properties such as accountability and fairness in electronic commerce protocols is presented. Compared with the previous work, the main contributions are the following. Firstly, a formal definition is given to the possession set of each protocol participant, and the initial possession set depends only on the environment. Secondly, the set of initial state assumptions is divided into three categories: basic assumptions, trust assumptions, and protocol comprehension assumptions, in order to avoid analysis errors caused by informal initial state assumptions. Thirdly, the set of trust assumptions is articulated by formal specification at a lower level of granularity, exposing the essence of the protocol. Fourthly, establishing an axiom system makes the new approach more rigorous and expressive.