电子商务支付协议认证性的SVO逻辑验证  

Verification of e-commerce payment protocol authentication properties based on SVO logic

作　　者：肖茵茵[1,2] 苏开乐[2,3] 

机构地区：[1]广东技术师范学院计算机学院,广州510665 [2]中山大学信息科学与技术学院广东省信息安全重点实验室,广州510275 [3]北京大学信息科学技术学院教育部高可信软件技术重点实验室,北京100871

出　　处：《计算机工程与应用》2014年第8期6-10,共5页Computer Engineering and Applications

基　　金：国家自然科学基金(No.60903054);国家重点基础研究发展规划(973)(No.2010CB328103);广东高校优秀青年创新人才培育项目(No.LYM11085;No.LYM11084)

摘　　要：与证伪法(如模型检测)相比,采用证真法(如定理证明和逻辑推理)能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。Compared with the falsification-oriented approaches（such as model checking）, the justification-oriented approaches （such as theorem proof and logic reasoning）can verify the correctness of protocols in unbounded number of sessions. However, those approaches are difficult and the verification process is complicated. Based on the SVO logic, this paper chooses the Netbill micropayment protocol to formally analyze the authentication properties of E-commerce payment pro-tocol. First, the axiom set of SVO is extended. Then, a simplified model of Netbill protocol is proposed without affecting the original security properties. According to the protocol’s characteristic, the verifying goals are improved. Moreover, the more reasonable protocol assumptions than before are given, the detailed reasoning process is showed, and the result is analyzed. The result shows that Netbill protocol satisfies the authentication properties. In the end, a comparison with other related research works is showed.

关 键 词：SVO逻辑 电子商务支付 Netbill协议 认证性 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]