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

• 作者: 吕关锋 岳伟亚 杨晋吉 肖茵茵 苏开乐 陈清亮
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: SET证书申请协议 自动化验证 SPV 认证性 秘密性
• 年，卷（期）: 2008,（6）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1035-1045
• 页数: 11页
• 分类号: TP309
• 字数: 9426字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2008.06.016

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖茵茵	中山大学信息科学与技术学院广东省信息安全重点实验室	11	57	5.0	7.0
2	苏开乐	中山大学信息科学与技术学院广东省信息安全重点实验室	22	309	11.0	17.0
6	岳伟亚	中山大学信息科学与技术学院广东省信息安全重点实验室	5	80	4.0	5.0
7	陈清亮	暨南大学计算机科学系	10	50	5.0	7.0
8	吕关锋	北京工业大学计算机学院	7	113	4.0	7.0
9	杨晋吉	中山大学信息科学与技术学院广东省信息安全重点实验室	10	111	6.0	10.0