关键词: 电子商务, 交易协议, 形式化验证, 原子性, 不可否认性

Abstract: There is a growing interest in formal verification for analysis of transaction protocol in electronic commerce field. SVO is perfect and compendious BAN-like logic. The two instances are given to illustrate the limitations of SVO when analyzing the protocol of electronic commerce. The new formal verification method is proposed in this paper, which expands the analysis framework of SVO and introduces the dynamic notion. In the new framework, the initial possession set depends on environment instead of human being. Furthermore, the new method can verify not only the non-repudiation of protocol in static state, but also atomicity in dynamic. At last, it is very valid by the analysis of several classic transaction protocols.

Key words: electronic commerce, transaction protocol, formal verification, atomicity, non-repudiation