学位论文 > 优秀研究生学位论文题录展示
鉴别协议的分析研究
作 者: 袁建廷
导 师: 刘西洋
学 校: 西安电子科技大学
专 业: 计算机系统结构
关键词: 鉴别协议 形式化方法 模型检测 NuSMV 设计方法
分类号: TP393.08
类 型: 硕士论文
年 份: 2008年
下 载: 37次
引 用: 1次
阅 读: 论文下载
内容摘要
鉴别协议在网络安全中占有很重要的地位,而对于鉴别协议的设计和分析都是很困难的。如果通过验证已有的攻击手段来分析鉴别协议,最主要的问题是我们无法穷尽所有的攻击类型。所以我们求助于形式化的方法。模型检测技术已经被证实是比较成功的协议分析的方法。我们采用模型检测工具NuSMV去验证鉴别协议,NuSMV支持线性时序逻辑。另外,我们采用了Gavin Lowe的研究成果,即如果要验证的协议满足一些前提条件并且在小系统模型上没有攻击,那么在任意的系统上都没有攻击,也即,对这个协议来说,模型检测是完备的。我们修改了一些协议,使其满足“一些前提条件”,然后在小系统模型上进行验证。通过修改、验证协议的过程,我们提出了一种新的鉴别协议设计方法。用这种方法设计出来的鉴别协议在小系统模型上如果是安全的,那么我们确信它是安全的。并且,我们在这个设计思想指导下设计了一个新的Test协议,使用NuSMV验证,验证的结果它是安全的。
|
全文目录
摘要 3-4 Abstract 4-6 第一章 绪论 6-10 1.1 安全协议简介 6-7 1.2 研究的背景 7-8 1.3 研究的内容和意义 8-9 1.4 本文的组织和结构 9-10 第二章 鉴别协议 10-22 2.1 鉴别的基本知识 10-12 2.2 鉴别协议的介绍 12-16 2.3 鉴别协议的攻击 16-22 第三章 模型检测技术 22-32 3.1 形式化方法介绍 22-24 3.2 模型检测概述 24-26 3.3 线性时序逻辑(LTL) 26-29 3.4 模型检测器NuSMV 29-32 第四章 鉴别协议的分析及设计 32-50 4.1 鉴别协议分析的形式化方法 32-35 4.2 鉴别协议的建模 35-36 4.3 改进的 Helsinki 协议的验证 36-42 4.4 一种新的鉴别协议的设计方法 42-45 4.5 Test 协议的设计及其验证 45-49 4.6 进一步的讨论 49-50 第五章 结束语 50-51 致谢 51-52 参考文献 52-55 研究成果 55-56
|
相似论文
- 基于BMC的Web服务失配检测方法研究,TP311.52
- 网页设计元素解析与探究,TP393.092
- 基于AD和TRIZ的自行车概念创新设计方法研究,U484
- 应用L系统理论设计家纺简约主义风格的方法,J504
- 服装二次设计—对闲置服装的再利用,TS941.2
- 基于四方的安全电子商务支付协议研究,TP393.08
- 基于基元式夹钳机构设计方法及性能的研究,TH21
- 纳米晶存储器中的高压产生系统设计,TN47
- 国内外公路桥梁混凝土构件设计方法对比分析,U448.14
- 超大粒径沥青混合料设计方法研究,U414
- 橡胶沥青混合料温拌技术的研究,U414
- 朋克元素在现在奢侈品服饰设计中的应用研究,J53
- 约束模块在软性磨粒流精整加工中的应用及其设计方法,TG664
- 基于“需求理论”的用户体验设计合理化研究,TB47
- 高速铁路桥梁减隔震研究,U442.55
- 沥青路面超薄罩面关键技术研究,U416.217
- 碎石化的旧水泥路面上水泥混凝土加铺层脱空预估研究,U414
- 波纹钢腹板预应力混凝土箱梁腹板稳定性研究,U448.213
- 矩形钢管混凝土桁架拱桥及其静力性能分析,U441
- 高填方涵洞EPS减荷技术应用研究,U449
- 基于视觉特性的高速公路景观要素设计研究,U418.9
中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机的应用 > 计算机网络 > 一般性问题 > 计算机网络安全
© 2012 www.xueweilunwen.com
|