鉴别协议的分析研究

论文摘要

鉴别协议在网络安全中占有很重要的地位,而对于鉴别协议的设计和分析都是很困难的。如果通过验证已有的攻击手段来分析鉴别协议,最主要的问题是我们无法穷尽所有的攻击类型。所以我们求助于形式化的方法。模型检测技术已经被证实是比较成功的协议分析的方法。我们采用模型检测工具NuSMV去验证鉴别协议,NuSMV支持线性时序逻辑。另外,我们采用了Gavin Lowe的研究成果,即如果要验证的协议满足一些前提条件并且在小系统模型上没有攻击,那么在任意的系统上都没有攻击,也即,对这个协议来说,模型检测是完备的。我们修改了一些协议,使其满足“一些前提条件”,然后在小系统模型上进行验证。通过修改、验证协议的过程,我们提出了一种新的鉴别协议设计方法。用这种方法设计出来的鉴别协议在小系统模型上如果是安全的,那么我们确信它是安全的。并且,我们在这个设计思想指导下设计了一个新的Test协议,使用NuSMV验证,验证的结果它是安全的。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 安全协议简介
• 1.2 研究的背景
• 1.3 研究的内容和意义
• 1.4 本文的组织和结构
• 第二章 鉴别协议
• 2.1 鉴别的基本知识
• 2.2 鉴别协议的介绍
• 2.3 鉴别协议的攻击
• 第三章 模型检测技术
• 3.1 形式化方法介绍
• 3.2 模型检测概述
• 3.3 线性时序逻辑（LTL）
• 3.4 模型检测器NuSMV
• 第四章 鉴别协议的分析及设计
• 4.1 鉴别协议分析的形式化方法
• 4.2 鉴别协议的建模
• 4.3 改进的 Helsinki 协议的验证
• 4.4 一种新的鉴别协议的设计方法
• 4.5 Test 协议的设计及其验证
• 4.6 进一步的讨论
• 第五章 结束语
• 致谢
• 参考文献
• 研究成果