基于时延Petri网的密码协议分析和评估

摘要

密码协议安全性分析是网络安全的一个难题,运用形式化方法对密码协议进行分析一直是该领域的研究热点.形式化分析由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入,该文主要研究了基于时延Petri网的密码协议分析和评估方法.作者所取得的主要研究结果如下:(1)对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点.(2)首次提出用时延Petri网作为工具来分析和评估密码协议,并且给出了用它分析和评估密码协议的具体方法和步骤.该方法不但能够反映协议的结构特性和动态特性,而且能够对密码协议进行时间、空间上的性能评估.(3)给出了时延Petri网的引发规则、时间可达图定义和构造算法,并且介绍了时延Petri网的两个基本分析方法:时间可达图(或可覆盖图)和状态方程.(4)用时延Petri网对MSR协议、Aziz-Diffle协议和TMN协议进行了具体和详细的分析,给出了这三种协议的发生序列(执行剧情)和攻击者对这三种协议的详细攻击剧情,并且对Aziz-Diffle协议给出了一个改进方案.(5)该文对这三种密码协议的执行时间、结构特性以及实现分析的软件复杂度给出了客观的评估.最后,该文建立了实现自动化分析密码协议工具—时延Petri网分析器的结构框架.

目录

文摘

英文文摘

声明

1绪论

1.1课题的提出

1.2密码协议

1.3密码协议的安全性

1.4密码协议分类

1.5论文的安排

2密码协议的形式化分析

2.1形式化分析的研究与进展

2.2 BAN 逻辑

2.3模型检测方法

2.4定理证明方法

2.5形式化分析技术小结

3时延Petri网

3.1 Petri网及其应用简介

3.2 Petri网基本知识

3.3时延Petri网（Timed Petri Net）

3.4时延Petri网的基本分析方法

4时延Petri网分析和评估密码协议的方法

4.1分析方法概述

4.2密码协议的评估方法

5若干密码协议的TPN分析和评估

5.1引言

5.3Aziz-Diffie协议分析和评估

5.4 TMN协议分析

5.5本章小结

6自动化密码协议分析工具TPN分析器的研究与开发

6.1时间Petri网的常用分析工具

6.2 TPN分析器的结构

7 结论

7.1讨论

7.2本文的主要工作

7.3进一步的工作

致谢

参考文献

作者在读期间的研究成果