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