学位论文 > 优秀研究生学位论文题录展示

基于树自动推理的安全协议自动化检测

作　者: 秦好磊
导　师: 马文平
学　校: 西安电子科技大学
专　业: 通信与信息系统
关键词: 安全协议形式化分析自动化检测树自动机项重写 Dolev-Yao模型定理证明
分类号: TP393.08
类　型: 硕士论文
年　份: 2011年
下　载: 21次
引　用: 0次
阅　读: 论文下载

内容摘要

本文介绍了树自动机结合项重写系统分析安全协议的方法。首先,协议步骤转化为项重写系统,通信请求被建模成树自动机;树自动机按照项重写系统进行推理迭代,自动超逼近网络中协议消息交换集合。最后,当树自动机终止时,通过判断终止逼近集和不允许行为集的交集是否为空,来实现对安全性质的检验。根据上述原理,本文开发了基于树自动推理的安全协议自动化检测系统TAVS(Tree Automata Verification System)。该系统在传统树自动机的基础上,引入了逼近规则,演进更加高效。TAVS根据协议形式自动建模、自动检测安全目标和构造攻击路径,可以检测认证协议和密钥交换协议等多种协议。本文最后,对LPD-IMSR协议进行检测,发现了一个针对认证性的中间人攻击;并对部分字段进行签名,改进了该协议,避免了中间人攻击。

全文目录

摘要  3-4
Abstract  4-7
第一章绪论  7-11
  1.1 安全协议  7-9
    1.1.1 基本概念  7
    1.1.2 安全性质  7-9
    1.1.3 常见攻击  9
  1.2 安全协议的发展  9-10
  1.3 论文的研究内容及论文安排  10-11
第二章安全协议形式化分析技术  11-21
  2.1 概述  11-12
  2.2 历史与现状  12-13
  2.3 分类  13-17
    2.3.1 形式逻辑  13-14
    2.3.2 模型检测  14-16
    2.3.3 定理证明  16-17
  2.4 形式化分析面临的挑战  17-19
  2.5 形式化分析的贡献  19
  2.6 本章小结  19-21
第三章树自动机推理技术  21-29
  3.1 自动机理论  21-22
  3.2 树自动机推理系统  22-28
    3.2.1 基本概念  22-23
    3.2.2 项重写系统  23-24
    3.2.3 逼近技术  24-28
  3.3 树自动机的应用  28
  3.4 本章小结  28-29
第四章树自动机自动检测安全协议  29-47
  4.1 总体结构  29-30
  4.2 攻击者模型  30-31
  4.3 协议建模  31-37
    4.3.1 初始树  31-32
    4.3.2 重写规则  32-35
    4.3.3 逼近规则  35-37
    4.3.4 安全目标  37
  4.4 推理迭代  37-40
  4.5 结果判定和攻击路径重构  40-43
    4.5.1 路径重构方法  40-41
    4.5.2 具体过程  41-43
  4.6 程序设计  43-45
    4.6.1 SML 语言  43
    4.6.2 底层模块  43-45
  4.7 本章小结  45-47
第五章 LPD-IMSR 协议检测实现  47-57
  5.1 初始树  47-48
  5.2 重写规则  48-49
  5.3 逼近规则  49-50
  5.4 安全需求  50
  5.5 检测结果  50-55
  5.7 分析与改进  55-56
  5.8 本章小结  56-57
第六章总结与展望  57-59
致谢  59-61
参考文献  61-65
硕士期间发表的论文和参与的科研项目  65-66

基于树自动推理的安全协议自动化检测

内容摘要

全文目录

相似论文