一种基于有色Petri网模型的安全协议检测技术的研究

摘要

本文在深入研究现有的基于有色Petr i网的安全协议分析方法的基础上，针对其中存在若干问题，提出了一种新的基于有色Petri网模型的安全协议检测方法。 为了证明本文提出方法的有效性，我们用新方法对Neeham-Schroedor公钥协议和TMN密码协议两个经典协议进行了检测。实验结果证明，我们提出的基于有色Petri网的安全协议检测方法是可行的，该方法的优势在于对安全协议的分析更加全面，且具有通用、易实现、易于理解和交互性好等诸多优点。

目录

文摘

英文文摘

第一章引论

1.1课题背景

1.2研究现状

1.3本文的研究内容和所做的工作

1.4论文组织结构

第二章安全协议的基本知识

2.1密码体制

2.1.1对称密钥密码体制

2.1.2公钥密码体制

2.2安全协议的基本概念

2.3常见的安全协议

2.3.1无可信第三方的对称密钥协议

2.3.2应用密码校验函数(CCF)的认证协议

2.3.3具有可信第三方的对称密钥协议

2.3.4对称密钥重复认证协议

2.3.5无可信第三方的公开密钥协议

2.3.6具有可信第三方的公开密钥协议

2.3.7其它协议

2.4常见的安全协议攻击方法

2.4.1攻击者的知识和能力

2.4.2重放攻击

第三章有色Petri网理论和CPN tools

3.1有色Petri网基本理论

3.1.1 Petri网的基本概念

3.1.2有色Petri网的基本定义

3.1.3有色Petri网的动态特性

3.2 CPN ML

3.2.1标识符

3.2.2颜色集

3.2.3变量

3.2.4常量

3.2.5函数

3.3 CPN tools

3.3.1有色Petri网的编辑

3.3.2语义检查

3.3.3网络模拟

3.3.4状态空间分析

第四章基于有色Petri网的安全协议模型检测方法

4.1安全协议的形式化分析方法

4.2基于有色Petri网的模型检测方法

4.2.1传统的有色Petri网安全协议分析方法

4.2.2新的有色Petri网安全协议分析方法

4.3性能比较分析

第五章使用有色Petri网方法检测安全协议

5.1使用有色Petri网方法检测Needham-Schroeder公钥协议

5.1.1 Needham-Schroedor公钥协议

5.1.2 Needham-Schroedor协议中消息的颜色集定义

5.1.3 Needham-Schroedor公钥协议正常通信时的有色Petri网模型

5.1.4加入入侵者后的Needham-Schroedor公钥协议有色Petri网模型

5.1.5在Needham-Schroedor公钥协议有色Petri网模型中检查漏洞

5.1.6对Lowe改进版本的Needham-Schroedor公钥协议的检测

5.2使用有色Petri网方法检测TMN密码协议

5.2.1 TMN密码协议

5.2.2 TMN密码协议中消息的颜色集定义

5.2.3 TMN密码协议正常通信时的有色Petri网模型

5.2.4加入入侵者后的TMN密码协议的有色Petri网模型

5.2.5在TMN密码协议的有色Petri网模型中检查漏洞

第六章研究工作总结与展望

6.1研究工作总结

6.2对未来工作的展望

参考文献

致谢

攻读硕士学位期间参加的科研项目

攻读硕士学位期间发表的学术论文