基于串空间模型的协议分析方法研究

论文摘要

计算机网络的高速发展和网络新应用的不断涌现给网络安全带来了很大的冲击,网络安全成为新的信息安全的热点;安全协议作为计算机网络安全体系的重要组成部分,也就变得越来越重要。然而,由于安全协议的复杂性,设计一个完美的安全协议是十分困难的,许多公开发表的安全协议中后来被发现它们存在各种各样的安全漏洞。因此,以确保安全协议正确性为目的的安全协议分析成为一项重要的研究课题。安全协议分析可分为形式化分析和非形式化分析,其中,形式化分析方法是安全协议理论研究的热点之一。常见的形式化分析方法有BAN逻辑,Kailar逻辑,SPI演算,CSP方法,串空间模型等。串空间模型理论是安全协议分析领域最新的研究成果,它是在1998年由Thayer, Herzog和Guttman提出的,具有高效、直观、实用等特点,不仅可以用于证明安全协议的正确性,还可以用于构造攻击,揭示安全协议的内在缺陷。该方法已经成功地分析了Needham-Schroeder-Lowe协议,Otway-Rees协议,Yahalom协议等诸多协议,被公认为是一种先进的高效的协议分析方法。本文以串空间理论作为研究基础,主要进行了以下研究:（1）深入研究串空间模型的基础理论,应用串空间模型分析了Natalia Miloslavskaya等人提出的一个双向认证协议,发现该协议在认证方面存在缺陷,并对该协议进行了改进。（2）对运用串空间理论分析不可否认协议进行研究,发现了以往运用串空间理论分析协议公平性的两个问题,并给出了解决方法。随后对不可否认协议中弹性信道、同步消息等特定假设条件,采用串空间理论的方式进行形式化描述及推理,从而为串空间理论分析不可否认协议扫除了障碍。然后以一个实例来说明如何运用串空间理论证明不可否认协议的公平性,其中,关键之处是如何构造正确的命题。（3）分析TEENP不可否认协议,发现它的安全缺陷,在此基础上提出了一个新的不可否认协议。同时,对另外两个不可否认协议进行分析,发现以往文献中未提及的新的漏洞。（4）此外,还对不可否认协议中的公平性,异常数据处理等问题提出了自己的一些想法。

论文目录

• 摘要
• ABSTRACT
• 1 绪论
• 1.1 课题的背景及意义
• 1.2 该领域的国内外研究现状综述
• 1.3 论文的主要工作
• 2 安全协议形式化分析综述
• 2.1 密码学概述
• 2.1.1 密码学简介
• 2.1.2 基本概念
• 2.1.3 密码体制
• 2.2 安全协议
• 2.2.1 安全协议的目标
• 2.2.2 安全协议的缺陷
• 2.2.3 安全协议的运行环境
• 2.3 形式化分析历史
• 2.4 形式化分析方法分类
• 2.4.1 基于推理的结构化方法
• 2.4.2 基于攻击的结构化方法
• 2.4.3 基于证明的结构化方法
• 3 串空间理论与模型
• 3.1 串空间基础
• 3.1.1 基本概念
• 3.1.2 丛与因果依赖关系
• 3.1.3 项与加密
• 3.1.4 攻击者串
• 3.1.5 攻击者的能力范围
• 3.2 诚实与理想
• 3.2.1 理想
• 3.2.2 入口点与诚实
• 3.3 认证测试方法
• 3.3.1 分量
• 3.3.2 攻击者密钥和安全密钥
• 3.3.3 被变换边与变换边
• 3.3.4 认证测试原理
• 4 运用串空间理论分析认证协议
• 4.1 认证协议的认证性与机密性
• 4.2 NAD 协议介绍
• 4.3 NAD 协议的分析
• 4.3.1 NAD PartⅠ的分析
• 4.3.2 NAD PartⅠ的缺陷分析
• 4.3.3 NAD PartⅡ的分析
• 4.4 对NAD 协议的改进
• 4.5 改进的NAD 协议的分析
• 4.5.1 改进的NAD PartⅠ的分析
• 4.5.2 改进的NAD PartⅡ的分析
• 4.5.3 小结
• 5 运用串空间理论分析不可否认协议
• 5.1 不可否认协议介绍
• 5.1.1 基本假设
• 5.1.2 不可否认证据
• 5.1.3 不可否认协议的性质
• 5.2 不可否认协议若干问题的讨论
• 5.2.1 对异常数据的处理
• 5.2.2 M 的拥有者对协议公平性的影响
• 5.3 现有串空间理论分析协议公平性的不足及纠正
• 5.3.1 串空间理论分析协议公平性的现状
• 5.3.2 串空间模型对内部攻击者的处理方法
• 5.3.3 串空间模型对公平性的描述
• 5.4 不可否认协议的特定假设的处理
• 5.4.1 同步消息的处理
• 5.4.2 弹性信道的处理
• 5.5 TEENP 协议分析与改进
• 5.5.1 标识符号说明
• 5.5.2 TEENP 协议过程
• 5.5.3 TEENP 协议缺陷
• 5.5.4 TEENP 协议的细节分析
• 5.5.5 新不可否认协议
• 5.5.6 NTEENP 协议的形式化分析
• 5.6 AF 不可否认协议分析
• 5.6.1 标识符号说明
• 5.6.2 AF 协议描述
• 5.6.3 AF 协议缺陷
• 5.7 KM 不可否认协议分析
• 5.7.1 标识符号说明
• 5.7.2 KM 协议描述
• 5.7.3 KM 协议缺陷
• 6 结论
• 致谢
• 参考文献
• 附录
• A. 作者在攻读学位期间发表的论文目录
• B. 作者在攻读学位期间参与的科研项目目录