文献类型：期刊文章

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

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

出　　处：《计算机学报》

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

年　　份：2008

卷　　号：31

期　　号：6

起止页码：1035-1045

语　　种：中文

收录情况：BDHX、BDHX2004、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20082811371219)、INSPEC、JST、MR、SCOPUS、ZGKJHX、核心刊

摘　　要：基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.

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

分 类 号：TP309]