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

摘要

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