1、 题目：题目： 基于基于公开密钥认证协议安全性的分公开密钥认证协议安全性的分 析与研究析与研究 - 1- 基于基于公开密钥认证协议安全性的分析与研究公开密钥认证协议安全性的分析与研究 摘摘 要要 公开密钥认证协议安全性分析与研究对于促进我国信息化建设以及网络安全和 信息安全研究具有非常重要的意义。 本文主要研究运用模型检测技术和基于模型检测 技术的运行模式分析法，并研究了公开密钥认证协议的理论与技术。在此基础上，对 公开密钥认证协议进行了运行模式的手工分析。研究成果如下： 系统介绍了公开密钥认证协议的基本概念及安全性分析的重要意义、研究进展和 现状。 研究了模型检测技术以及公开密钥认证协议运行
2、模式分析法。 给出了运用模型检测工具 SMV 分析公开密钥认证协议的方法。 研究了公开密钥认证协议，运用运行模式分析法分析公开密钥认证协议的安全 性，成功地发现了该协议的安全漏洞。并在学习了 SMV 模型检测工具的基础上， 研究了公开密钥认证协议的 SMV 检测程序的框架和数据结构。 关键词：关键词：公开密钥认证协议，模型检测协议分析，形式方法， 运行模式分析法， SMV - 2- Abstract Analysis of security protocols has a significance to promote the information construction and the
3、research of the network and the information security in our country. This dissertation focuses on the theory and the technique of the model checking of the security protocols. Following are the main results of this thesis: Introduce the basic conception, the significance, the evolvement and the stat
4、e of the cryptographic protocols analysis. Study the methods of model checking and running modes. Give the method of model checking by using the sofeware of Symbolic Model Verifier to analysis protocol. Design the protocol, Use the running-mode analysis approach based on the two-party cryptographic
5、protocols to analyze the protocol, and design a SMV program to check the TW protocol. In the basis of the SMV program of protocol, Design the general program of SMV to check the two-party protocol. Keywords: Cryptographic protocolModel, checkingprotocol analysis, Formal methods，Running-mode, analysi
6、s approach， SMV - 3- 目录目录 中文摘要 . 英文摘要 . 1 绪论 . 错误错误! !未定义书签。未定义书签。 1.1 本课题的开发背景以及开发意义. 5 1.2 国内外研究现状. 错误错误! !未定义书签。未定义书签。 1.3 本课题研究的主要内容 . 错误错误! !未定义书签。未定义书签。 2 公开密钥认证协议 . 错误错误! !未定义书签。未定义书签。 1.1 公开密钥认证协议的基本概念. 错误错误! !未定义书签。未定义书签。 1.2 公开密钥认证协议分类. 错误错误! !未定义书签。未定义书签。 1.3 公开密钥认证协议的安全性及其设计规范. 错误错误! !未定义书签。未定义书签。 1.3.1 公开密钥认证协议的安全性分析及攻击 .错误错误! !未定义书签。未定义书签。 1.3.2 安全协议设计规范 .错误错误! !未定义书签。未定义书签。 1.4 公开密钥认证协议模型检测分析技术的研究与进展. 错误错误! !未定义书签。未定义书签。 1.5 论文安排与研究成果. 错误错误! !未定义书签。未定
