Computer Engineering and Applications ›› 2014, Vol. 50 ›› Issue (8): 6-10.

Previous Articles     Next Articles

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

XIAO Yinyin1,2, SU Kaile2,3   

  1. 1.School of Computer Science, Guangdong Polytechnic Normal University, Guangzhou 510665, China
    2.Guangdong Key Lab of Information Security Technology, School of Information Science and Technology, Sun Yat-sen University, Guangzhou 510275, China
    3.Key Lab of High Confidence Software Technologies, Ministry of Education, School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China
  • Online:2014-04-15 Published:2014-05-30

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

肖茵茵1,2,苏开乐2,3   

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

Abstract: 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 protocol. 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.

Key words: SVO logic, e-commerce payment, Netbill protocol, authentication properties

摘要: 与证伪法(如模型检测)相比,采用证真法(如定理证明和逻辑推理)能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。

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