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

计算机工程与应用 ›› 2014, Vol. 50 ›› Issue (8): 6-10.

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

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

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

出版日期:2014-04-15 发布日期:2014-05-30

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

XIAO Yinyin1，2, SU Kaile2，3

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

摘要/Abstract

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

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

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

肖茵茵1，2，苏开乐2，3. 电子商务支付协议认证性的SVO逻辑验证[J]. 计算机工程与应用, 2014, 50(8): 6-10.

XIAO Yinyin1，2, SU Kaile2，3. Verification of e-commerce payment protocol authentication properties based on SVO logic[J]. Computer Engineering and Applications, 2014, 50(8): 6-10.

[1]	杜梦瑶，王峥，李娜，强彦. 适用于无线体域网的动态口令认证协议[J]. 计算机工程与应用, 2020, 56(14): 68-73.
[2]	杨文霞，王峥，李娜，马建芬. 轻量级移动支付协议LMPP的安全性分析与改进[J]. 计算机工程与应用, 2019, 55(16): 88-93.
[3]	邓飞1，朱莹2. 一种可证明安全的匿名可认证密钥协商协议[J]. 计算机工程与应用, 2018, 54(5): 101-104.
[4]	余磊，魏仕民. 网络管理中一种互认证密码协议的安全性分析[J]. 计算机工程与应用, 2012, 48(4): 94-96.
[5]	何频，陈明. 改进的可证安全的相互认证及密钥协商方法[J]. 计算机工程与应用, 2010, 46(31): 86-90.
[6]	陈莉，郭清溥. 新的复合型电子商务安全协议[J]. 计算机工程与应用, 2010, 46(11): 14-17.
[7]	阮峰¹，候建敏²，张中秋³，范志勇². 一种乐观电子商务协议的公平性分析[J]. 计算机工程与应用, 2009, 45(35): 84-87.
[8]	郭宇燕¹,魏仕民²,卓泽朋³. 对改进的无线认证协议SSM的分析[J]. 计算机工程与应用, 2009, 45(1): 129-130.
[9]	苏仁旺. Sun等两个完美前向安全E-mail协议分析与改进[J]. 计算机工程与应用, 2008, 44(21): 69-71.