首页> 正文

两种安全协议形式化理论的研究

2020-11-22阅读(210)

两种安全协议形式化理论的研究

论文摘要

在本文中，我们探讨了有关两种安全协议形式化理论的若干问题，其中，工作重点集中在对三方认证密钥交换协议的形式化分析上。 网络技术具有快速实现信息共享的特点，这大大提高了人们通信的效率，给人们的生活、学习和工作带来了巨大的改观。但与此同时，人们对网络本身具有的公开性和匿名性所带来的日益严重的信息安全问题也深感不安。 为了解决网络的信息安全问题，人们设计了许多用于开放网络的安全协议来解决各种安全应用问题。所谓安全协议，就是两个或两个以上的参与者采取一系列步骤来完成某项特定的安全任务。它包含三层含义：1．协议需要至少两个参与者。2．参与者之间执行的是消息处理和消息交换交替进行的一系列步骤。3．通过协议执行必须能够完成某种安全任务。 由于每个安全协议都是为了某种安全应用而精心设计的，协议中的各条消息间有着微妙的相互制约关系，因此若采用人工方式对协议进行安全性分析，往往不能发现协议存在的问题，所以必须借助于形式化的方法来完成。形式化方法是一种用于描述系统性质的数学方法，它主要用于发现一个系统中的歧义性、不一致性与不完备性。该系统可以大到一个企业级的软硬件系统，也可以小到有若干条消息组成的协议。对安全协议使用形式化的方法，可挖掘出协议消息所表示的内在含义，对协议的正确性进行验证。通过验证，不仅可证明协议是否符合预期的安全目标，而且对不符合安全目标的协议可分析其缺陷之所在，进而为协议的设计提供有力的支持。 目前在安全协议形式化的研究领域有两种截然不同的理论：符号理论与计算理论：

论文目录

  • 摘要
  • ABSTRACT
  • 符号说明和缩略词
  • 第一章 绪论
  • 1.1、安全协议的一些基本概念
  • 1.1.1、网络协议及会话
  • 1.1.2、安全协议及分类
  • 1.1.3、安全协议的服务
  • 1.2、密码学的相关内容
  • 1.2.1、常用的密码体制
  • 1.2.2、常用的密码要素
  • 1.3、针对安全协议的攻击
  • 1.3.1、消息重放攻击
  • 1.3.2、平行会话攻击
  • 1.3.3、密码学缺陷攻击
  • 1.4、本文工作的背景及意义
  • 1.5、研究工作概要及论文安排
  • 第二章 安全协议的形式化分析方法
  • 2.1、符号理论
  • 2.1.1、基于推理结构的方法
  • 2.1.2、基于攻击结构的方法
  • 2.1.3、基于证明结构的方法
  • 2.1.4、符号理论的缺陷
  • 2.2、计算理论
  • 2.2.1、模式方法
  • 2.2.2、计算理论的缺陷
  • 2.3、安全协议形式化方法的新发展
  • 2.3.1、Abadi和Rowaway的可调和性思想
  • 2.4 本章小结
  • 第三章 对CS逻辑的改进与扩展
  • 3.1、CS逻辑的介绍
  • 3.1.1、基本介绍
  • 3.1.2、CS逻辑的符号
  • 3.1.3、CS逻辑的推理系统
  • 3.2、CS逻辑及已有扩展的缺陷
  • 3.2.1、CS逻辑的缺陷
  • 3.2.2、已有扩展的缺陷
  • 3.3、我们对CS逻辑的扩展
  • 3.3.1、增加的符号
  • 3.3.2、对已有逻辑公理的改进和扩展
  • 3.3.3、新添加的公理
  • 3.4、实例分析
  • 3.4.1、一种对称密钥交换协议的分析实例
  • 3.4.2、协议分析
  • 3.5、本章小结
  • 第四章 MBL逻辑
  • 4.1、BAN类逻辑的缺陷
  • 4.2、MBL逻辑
  • 4.2.1、MBL逻辑对安全协议设计的要求
  • 4.2.2、MBL逻辑的符号
  • 4.2.3、MBL逻辑的敌手模型
  • 4.2.4、MBL逻辑的语义模型
  • 4.2.5、推理规则
  • 4.2.6、推理规则的正确性证明
  • 4.3、分析举例
  • 4.4、MBL逻辑的可扩展性
  • 4.5、本章小结
  • 第五章 MBL逻辑的自动化分析
  • 5.1、有关自动化的已有工作
  • 5.2、基于MBL逻辑的自动化分析法
  • 5.2.1、MBL逻辑符号到Prolog语言的转化
  • 5.2.2、协议信息在Prolog语言的存储
  • 5.2.3、推理的实现
  • 5.2.4、实例分析
  • 5.3、本章小结
  • 第六章 设计安全的认证密钥交换协议
  • 6.1、加密体制的安全性
  • 6.1.1、不可区分的选择明文攻击
  • 6.1.2、不可区分的选择密文攻击
  • 6.1.3、不可区分适应性选择密文攻击
  • 6.1.4、加密体制的选取
  • 6.2、一个协议及其攻击
  • 6.3、安全因素
  • 6.3.1、认证性
  • 6.3.2、正确的密码学保护
  • 6.4、对YAHALOM协议的改进
  • 6.5、对NEEDHAM-SCHREODER公钥认证协议的改进
  • 6.6、本章小结
  • 第七章 计算理论下认证密钥交换协议的安全性
  • 7.1、基本概念
  • 7.1.1、消息驱动的认证密钥交换协议
  • 7.1.2、匹配对话
  • 7.2、认证密钥交换协议的安全性
  • 7.2.1 分析协议的认证性
  • 7.2.2 保密性的讨论
  • 7.3、本章小结
  • 第八章 符号理论和计算理论相结合的分析法
  • 8.1、通信的形式化
  • 8.2、完全性与正确性
  • 8.3、对MBL逻辑的修改和扩展
  • 8.4、改进YAHALOM协议的安全性分析
  • 8.4.1、协议及其安全目标的描述
  • 8.4.2、形式化分析
  • 8.5、本章小结
  • 第九章 总结
  • 参考文献
  • 感谢
  • 博士学习期间发表的论文情况
  • 在读期间参与科研项目情况
  • 学位论文评阅及答辩情况表

    • 相关论文文献

    • [1].考核粗线条影响压力传导怎么办——结合实际在“精、准、效”上下功夫[J]. 中国纪检监察 2020(14)
    • [2].避免合作学习的形式化倾向[J]. 中国教育学刊 2016(04)
    • [3].利用逐步形式化原则完善学生的认知结构[J]. 中国数学教育 2020(17)
    • [4].数学形式化的境域性教学[J]. 学园 2019(01)
    • [5].基于适度形式化的函数图象考查探究[J]. 福建中学数学 2013(04)
    • [6].不能弱化数学形式化[J]. 福建中学数学 2010(06)
    • [7].基于适度形式化的数学“双基”考查探究[J]. 福建中学数学 2011(05)
    • [8].基于适度形式化的试题评析[J]. 福建中学数学 2011(06)
    • [9].试论高中数学的形式化[J]. 数学教学 2008(08)
    • [10].数学形式化的利与弊研究及反思[J]. 中学数学研究 2013(12)
    • [11].刍议数学命题的非形式化解法及功能[J]. 福建中学数学 2014(12)
    • [12].“不要急于创新”值得倾听[J]. 发明与创新(综合科技) 2010(10)
    • [13].走出科学课形式化教学的误区[J]. 山东教育 2015(10)
    • [14].形式化技术在软件工程中的作用[J]. 电子技术与软件工程 2013(21)
    • [15].做有效的国旗下讲话[J]. 辅导员 2008(06)
    • [16].浅谈设计中的形式与内容[J]. 戏剧之家 2020(07)
    • [17].语境形式化中的演绎与归纳[J]. 科学技术哲学研究 2017(05)
    • [18].论中西因素对现代建筑的形式化影响——民国时期建筑[J]. 美与时代(城市版) 2016(06)
    • [19].2010年福建省高考数学试卷评析(十) 基于适度形式化的试题评析[J]. 福建中学数学 2010(06)
    • [20].非形式化:一种提高数学教学有效性的途径[J]. 江苏教育研究 2015(28)
    • [21].力戒教育形式化[J]. 吉林教育 2015(Z2)
    • [22].术前多形式化访视对手术患者治疗效能感及睡眠的影响研究[J]. 中国医药指南 2013(34)
    • [23].谈形式化和绝对化对新课程的负面影响[J]. 魅力中国 2009(29)
    • [24].突破合作互学改革瓶颈须去形式化[J]. 中国教育学刊 2014(04)
    • [25].形式化规范在软件可靠性早期估计中的应用研究[J]. 微型机与应用 2011(11)
    • [26].第12届国际形式化工程大会(ICFEM 2010)[J]. 计算机应用与软件 2010(09)
    • [27].海上编队作战方案形式化描述研究[J]. 舰船电子工程 2009(06)
    • [28].形式化与非形式化在课堂教学中的融合演绎[J]. 中学教研(数学) 2013(10)
    • [29].高中数学形式化与非形式化教学的案例研究[J]. 数学教学通讯 2008(07)
    • [30].重视统计与概率中的非形式化问题教学[J]. 基础教育论坛 2012(13)

    标签：;  ;  ;  ;  ;  

    两种安全协议形式化理论的研究
    下载Doc文档

    猜你喜欢

    © 2024 毕速过 版权所有 鄂ICP备12018319号-5