基于UML安全协议的建模和自动检测
| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 绪论 | 第7-10页 |
| ·课题背景 | 第7-8页 |
| ·本文的主要工作和目标 | 第8-9页 |
| ·论文的结构 | 第9-10页 |
| 第二章 安全协议 | 第10-15页 |
| ·安全协议的类别和性质 | 第10-12页 |
| ·安全攻击 | 第12页 |
| ·形式化方法 | 第12-15页 |
| 第三章 模型检测 | 第15-26页 |
| ·模型检测简介 | 第15-16页 |
| ·时态逻辑 | 第16-19页 |
| ·CTL(计算树逻辑) | 第16-18页 |
| ·LTL(线性时态逻辑) | 第18-19页 |
| ·模型检测工具SPIN | 第19-26页 |
| ·SPIN工具 | 第19页 |
| ·SPIN状态优化技术 | 第19-21页 |
| ·PROMELA语言 | 第21-26页 |
| 第四章 统一建模语言UML | 第26-37页 |
| ·UML简介 | 第26-29页 |
| ·UML的特性 | 第26-27页 |
| ·UML基本概念 | 第27-29页 |
| ·UML建模 | 第29-31页 |
| ·建模的目的 | 第29页 |
| ·UML的一般建模过程 | 第29-31页 |
| ·UML类图 | 第31-32页 |
| ·UML顺序图 | 第32-33页 |
| ·XMI文件 | 第33-37页 |
| ·XMI表示UML类图 | 第33-35页 |
| ·XMI表示UML顺序图 | 第35-37页 |
| 第五章 安全协议建模 | 第37-48页 |
| ·安全协议的静态模型 | 第37-45页 |
| ·安全协议的一般表示形式 | 第37-38页 |
| ·建立安全协议的数据模型 | 第38-40页 |
| ·建立安全协议的类模型 | 第40-45页 |
| ·安全协议的动态模型 | 第45-48页 |
| ·从安全协议的一般描述到UML顺序图 | 第45页 |
| ·实例分析 | 第45-48页 |
| 第六章 自动验证 | 第48-65页 |
| ·自动验证过程 | 第48-49页 |
| ·分析并提取基本信息集 | 第49-54页 |
| ·分析并提取类的基本信息 | 第49-51页 |
| ·分析并提取顺序图的信息集 | 第51-53页 |
| ·合并类和顺序图的基本信息集 | 第53-54页 |
| ·协议主体UML模型转化到PROMELA程序 | 第54-57页 |
| ·协议主体的UML模型到PROMELA程序的映射 | 第54-55页 |
| ·转化过程 | 第55-57页 |
| ·攻击者模型的自动生成和转化 | 第57-65页 |
| ·自动生成攻击者知识库 | 第58-62页 |
| ·生成攻击者模型的PROMELAT程序 | 第62-65页 |
| 第七章 自动验证工具的设计与实现 | 第65-69页 |
| ·体系结构 | 第65-66页 |
| ·设计与实现 | 第66-69页 |
| 第八章 结束语 | 第69-70页 |
| ·本文主要内容 | 第69页 |
| ·下一步工作 | 第69-70页 |
| 参考文献 | 第70-73页 |
| 攻读硕士研究生生期间公开发表论文 | 第73-74页 |
| 致谢 | 第74-75页 |
