SET证书申请协议在SPV下的自动化验证及改进  

The Automatic Verification and Improvement of SET Certificate Registration Protocols with SPV

作　　者：肖茵茵[1] 苏开乐[1] 岳伟亚[1] 陈清亮[2] 吕关锋[3] 杨晋吉[1] 

机构地区：[1]中山大学信息科学与技术学院广东省信息安全重点实验室,广州510275 [2]暨南大学计算机科学系,广州510632 [3]北京工业大学计算机学院,北京100022

出　　处：《计算机学报》2008年第6期1035-1045,共11页Chinese Journal of Computers

基　　金：国家“九七三”重点基础研究发展规划项目基金(2005CB321902);国家自然科学基金(60496327,10410638,60473004);广东省自然科学基金(06023195);广东省自然科学基金团队项目(04205407)资助~~

摘　　要：基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.Based on the Instantiation Space Logic theory and knowledge reasoning, the authors implement the totally automatic verification on the complete SET certificate registration protocols＇ authentication and secrecy properties using SPV, and improve the protocols. SPV can efficiently verify whether the security protocol satisfies the goals in CAPSL（Common Authentication Protocol Specification Language） as well as multi-level epistemic specifications using modern SAT solvers. All protocols should be simplified before being verified by logics or tools. As to the SET protocols, it is the most complex industrial protocol at present, which has the document of over 1000 pages. Therefore, it is very difficult to simplify and there are few research works about it. Besides, some existent simplified models are not complete enough. Consequently, the paper gives a simplified model which is more close to the original SET certificate registration protocols, and introduces the model＇s formal description in SPV with the verification process and results. More over, according to the hidden danger of the protocols brought by the unsatisfied epistemic specification, the authors improve the protocols and show the effectiveness. The work also justifies that SPV has the ability to deal with complex industrial protocols.

关 键 词：SET证书申请协议 自动化验证 SPV 认证性 秘密性 

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