肖茵茵 ，苏开乐

XIAOYinyin1，2,SU Kaile2，3

1.广东技术师范学院 计算机学院，广州 510665

2.中山大学 信息科学与技术学院 广东省信息安全重点实验室，广州 510275

3.北京大学 信息科学技术学院 教育部高可信软件技术重点实验室，北京100871

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

1 引言

随着电子商务的普及和发展，SSL、SET、Netbill等电子商务支付协议的地位越来越重要。安全协议的手工分析十分困难，容易出错，特别是对复杂的电子商务支付协议来说，采用形式化的理论和工具验证其安全性十分必要[1]。在现有的电子商务协议安全性研究中，多采用有限模型检测法寻找协议的漏洞和潜在攻击的路径（证伪法）[2-4]，这类方法具有自动化工具（SMV、SPIN等），使用方便，但检测的状态空间有限，即使检测不出攻击，也无法保证协议在任意会话中的正确性。另一类方法采用定理证明和逻辑推理，可验证协议能否满足特定的安全性质以及证明协议的正确性（证真法）[5-7]，这类方法准确度高，但验证过程繁杂，验证复杂协议时难度较大，如文献[5]用实例化空间逻辑验证了SET协议的秘密性和认证性，但文中并未说明其具体推理过程；文献[8-9]展示了使用类BAN逻辑验证Netbill协议的推理过程，但文中主要关注的是协议的原子性和时限责任等问题，而未讨论其认证性。

本文使用SVO逻辑方法[10]，选取Netbill协议[11]，对其认证性进行形式化分析：首先对SVO逻辑的公理集进行扩展，然后在不影响Netbill协议安全性的前提下，为其建立简化模型，之后针对协议特点，修正和补充了其验证目标，最后给出了具体的推理过程和验证结果以及相关工作的比较。……