《计算机学报》文章摘要   全文下载
文章题目	SET证书申请协议在SPV下的自动化验证及改进
作者	肖茵茵1) 苏开乐1),2) 岳伟亚1) 陈清亮3) 吕关锋4) 杨晋吉1),5)
作者单位	1)(中山大学信息科学与技术学院广东省信息安全重点实验室 广州 510275) 2)(北京大学信息科学技术学院教育部高可信软件技术重点实验室 北京 100871) 3)(暨南大学计算机科学系 广州 510632) 4)(北京工业大学计算机学院 北京 100022) 5)(华南师范大学计算机学院 广州 510631)
发表年份	2008
发表月份	6期(1035—1045)
文章摘要	摘要 基于实例化空间逻辑理论，使用知识推理方法，在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明，并对协议进行了改进.SPV调用工业级SAT求解器，能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化，而SET协议作为当前最复杂的工业级协议，其原始文档有上千页，因此简化过程相当困难，相关研究较少，已有的一些简化模型也不够完整.因此，文章针对SET证书申请协议，给出了比以往更贴近原协议的简化模型，并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果，分析了由于协议不满足某些认知规范所带来的安全隐患，从而对协议进行改进，最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议. 关键词：SET证书申请协议；自动化验证；SPV；认证性；秘密性