电子商务协议的串空间分析

电子商务协议常常具有复杂结构,协议可能由多个子协议组合而成.因此,电子商务协议的安全分析较认证协议更为复杂.传统的信念逻辑不适宜分析电子商务协议.Kailar逻辑适宜分析电子商务协议的可追究性,但不适宜分析协议的公平性.本文介绍并扩展了串空间逻辑,分析了ISI支付协议的串,并证明其不满足公平性.还提出一种新的串节点路径法,用以分析了ASW协议,该协议系由多个子协议组成的分支结构协议,通过串空间分析证明了该协议的公平性.通过对两个协议的分析,分别提供了对电子商务在线交易协议和离线交易协议的形式化分析方法.

Strand Spaces Analysis of Electronic Commerce Protocols

The electronic commerce protocols often have more complex structures than authentication protocols,and a protocol might be composite of multiple sub-protocols,so the security analysis of electronic commerce protocols is more complex than the analysis of authentication protocols.Traditional belief logic is not suitable for analyzing the electronic commerce protocol.Kailar logic is suitable for analyzing the accountability of commerce protocol and it is not suitable for fairness analysis.In this paper,the strand space model is described and expanded,and the ISI protocol is proven unfair by analyzing its strands.Based on strand space model,a universal strand node path method is presented to analyze the ASW protocol,which consists of multiple sub-protocols with branch structure,and the strand space analysis shows that the ASW protocol is fair.The formal analysis methods are proposed for electronic commerce exchange protocols with on-line TTP and off-line TTP by analyzing ISI protocol and ASW protocol.