一种基于SVO逻辑的新形式化验证方法

通过严格的形式化验证方法来分析电子商务交易协议，一直是电子商务领域研究的热点。SVO逻辑以其完善、简洁的特点在协议验证中被广泛应用。文中通过典型实例分析，指出SVO逻辑在分析电子商务交易协议中存在的局限与不足，并在此分析基础上引入交易协议的动态性等概念。对原有SVO逻辑分析框架进行扩展，提出了一种新的适用于分析电子商务交易协议的形式化验证方法。新方法不仅可以静态验证协议的不可否认性，而且可以动态验证协议的原子性。最后，给出了该方法对典型交易协议的验证实例。

A New Formal Verification Method Based on SVO

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.