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

摘要

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

目录

文摘

英文文摘

第一章 绪 论

1.1 安全协议

1.1.1 基本概念

1.1.2 安全性质

1.1.3 常见攻击

1.2 安全协议的发展

1.3 论文的研究内容及论文安排

第二章 安全协议形式化分析技术

2.1 概述

2.2 历史与现状

2.3 分类

2.3.1 形式逻辑

2.3.2 模型检测

2.3.3 定理证明

2.4 形式化分析面临的挑战

2.5 形式化分析的贡献

2.6 本章小结

第三章 树自动机推理技术

3.1 自动机理论

3.2 树自动机推理系统

3.2.1 基本概念

3.2.2 项重写系统

3.2.3 逼近技术

3.3 树自动机的应用

3.4 本章小结

第四章 树自动机自动检测安全协议

4.1 总体结构

4.2 攻击者模型

4.3 协议建模

4.3.1 初始树

4.3.2 重写规则

4.3.3 逼近规则

4.3.4 安全目标

4.4 推理迭代

4.5 结果判定和攻击路径重构

4.5.1 路径重构方法

4.5.2 具体过程

4.6 程序设计

4.6.1 SML语言

4.6.2 底层模块

4.7 本章小结

第五章 LPD-IMSR协议检测实现

5.1 初始树

5.2 重写规则

5.3 逼近规则

5.4 安全需求

5.5 检测结果

5.7 分析与改进

5.8 本章小结

第六章 总结与展望

致谢

参考文献

硕士期间发表的论文和参与的科研项目