中文摘要：

通过典型实例分析，发现并指出SVO逻辑在验证电子商务协议中存在的缺陷，并在此基础上，充分考虑交易信道的可靠性和交易实体的诚实情况，对其分析框架进行扩展，提出一种验证电子商务交易协议的新逻辑分析方法。新逻辑分析方法符合电子商务协议运行特征，不仅可以静态验证协议的不可否认性，而且可以动态验证协议的公平性。同时，对协议的分析只依赖协议的运行环境，不需人为引入初始化假设，是一种更为严密的形式化分析方法。最后，以经典协议对新方法的正确性、有效性进行验证。

英文摘要：

A classic instance is given to illustrate the limitations of SVO on verification of electronic commerce protocol in this paper. A new logic analysis method for the electronic commerce protocol is proposed under unreliable communication and dishonest participants, which expands the analysis framework of SVO. In the new framework, the analysis for the protocol only depends on the opera- tional environment there is no need of the initial supposition given by people. Furthermore, the novel method can verify not only non-repudiation in static state, but also fairness in dynamic. At last, one classical transaction protocol is presented to verify the validity of the method. Research results show that the new logic is rigorous and effective.