|
|||||
|
|
| SET证书申请协议在SPV下的自动化验证及改进 | |
| 引用本文： | 肖茵茵,苏开乐,岳伟亚,陈清亮,吕关锋,杨晋吉.SET证书申请协议在SPV下的自动化验证及改进[J].计算机学报,2008,31(6):1035-1045. |
| 作者姓名： | 肖茵茵 苏开乐 岳伟亚 陈清亮 吕关锋 杨晋吉 |
| 作者单位： | 1. 中山大学信息科学与技术学院广东省信息安全重点实验室,广州,510275 2. 中山大学信息科学与技术学院广东省信息安全重点实验室,广州,510275;北京大学信息科学技术学院教育部高可信软件技术重点实验室,北京,100871 3. 暨南大学计算机科学系,广州,510632 4. 北京工业大学计算机学院,北京,100022 5. 中山大学信息科学与技术学院广东省信息安全重点实验室,广州,510275;华南师范大学计算机学院,广州,510631 |
| 基金项目： | 国家重点基础研究发展计划(973计划) , 国家自然科学基金 , 广东省自然科学基金 , 广东省自然科学基金 |
| 摘 要： | 基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议. |
| 关 键 词： | SET证书申请协议 自动化验证 SPV 认证性 秘密性 |
| 修稿时间： | 2007年7月12日 |
The Automatic Verification and Improvement of SET Certificate Registration Protocols with SPV |
|
| XIAO Yin-Yin,SU Kai-Le,YUE Wei-Ya,CHEN Qing-Liang,LU Guan-Feng,YANG Jin-Ji.The Automatic Verification and Improvement of SET Certificate Registration Protocols with SPV[J].Chinese Journal of Computers,2008,31(6):1035-1045. | |
| Authors: | XIAO Yin-Yin SU Kai-Le YUE Wei-Ya CHEN Qing-Liang LU Guan-Feng YANG Jin-Ji |
| Abstract: | |
| Keywords: | SET certificate registration protocols automatic verification SPV authentication secrecy |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |