基于ProVerif的安全攻击仿真+源代码
本文主要研究应用ProVerif这一安全协议分析工具，来验证相关网络协议的安全性。主要的研究成果如下：
（1）介绍了安全协议的基本概念及安全协议形式化分析方法；
（2）描述了ProVerif的安装和使用，分析了ProVerif工具的整体结构；
（3）介绍了应用Pi演算的语法，分析了ProVerif对基本安全属性的验证；
（4）利用应用Pi演算对协议SE-AKA(secure and efficient group authentication and key agreement protocol)建立了验证模型，并利用ProVerif工具验证其保密性、认证性与匿名性，得出相应的分析结果。
关键字 安全协议 ProVerif 应用Pi演算 保密性 认证性 匿名性
毕业论文设计说明书外文摘要
Title Security attack simulation based on ProVerif
Abstract
At present，information security has become a key problem in the information age。Security protocol is the key means to ensure information security。However, practice shows that a correct and reliable security protocol design is a very difficult task, many widely used security protocols have been pointed out there is a variety of security vulnerabilities。
Therefore，it has important application value to analyze and verify security protocols。Formal methods have been proved to be an effective way for the analysis and verification of security protocols。
This paper mainly studies the application of ProVerif protocol analysis tool，to verify the security of network protocols。The main results are as follows：
(1) introduce the basic concept of security protocols and formal methods；
(2) describe the installation and use of ProVerif, analysis of the overall structure of the ProVerif tool；
(3) introduce the Applied Pi calculus，and analyze the verification of basic security attributes by ProVerif；
(4) model SE-AKA protocol in Applied Pi calculus and verify its confidentiality、authentication and anonymity by ProVerif, then get corresponding analysis results。
Keywords security protocol ProVerif Applied Pi calculus confidentiality authentication anonymity
目 次
1 绪论 1
1.1 安全协议 1
1.1.1 安全协议的基本概念 1
1.1.2 安全协议的常见攻击 1
1.1.3 安全协议的分类 1
1.1.4 安全协议的安全属性 2
1.2 安全协议形式化分析 3
1.2.1 安全协形式化分析的概念 3
1.2.2 安全协议形式化分析方法的分类 3
1.2.3 安全协议分析工具 4
1.3 课题研究的主要内容 4
1.4 章节安排 5
1.5 本章小结 5
2 ProVerif工具的介绍 6
2.1 ProVerif的体系结构 6
2.2 ProVerif的安装和使用 6
2.2.1 ProVerif的安装 6
2.2.1 ProVerif的使用 10
2.3 本章小结 11
3 应用PI演算 12