A New Formal Verification Method Based on SVO
Deli Yang · Computer Integrated Manufacturing Systems · 2004
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.