基于挑战—响应的安全协议分析

作     者：罗军舟 杨明 

作者机构：东南大学计算机科学与工程学院南京210096 

出 版 物：《中国科学（E辑）》 (Science in China(Series E))

年 卷 期：2006年第36卷第12期

页      面：1421-1441页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金重大研究计划项目(批准号:90412014 90604004) 江苏省"网络与信息安全"重点实验室(BM2003201) 江苏省高技术研究项目(BG2004036)资助 

主　　题：网络安全 协议分析 挑战—响应 线空间模型 

摘      要：安全协议的本质是协议主体采用密码学方法通过挑战—响应来对协议其他方的存在做出判断,同时完成一些数据如会话密钥的协商．大部分国内外现有的分析方法或者采用状态检测等定理证明技术,或者采用认证逻辑等推理技术,存在着分析能力与可操作性之间的矛盾．为了解决这个问题,文中提出一种新的安全协议保密性和关联性的分析方法,该方法基于线空间模型理论给出了协议保密目标和认证目标的形式化定义,采用认证逻辑作为基础分析手段．保密性分析被分解为显式泄密和隐性泄密两种情况,其中隐性泄密分析依赖于关联性的判断,而关联性的分析被总结为Strand的存在关系和参数一致性分析的问题．新的分析方法既具有线空间模型的分析能力,又具有认证逻辑的易用性．