| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 第1章 绪论 | 第7-10页 |
| ·研究背景 | 第7-8页 |
| ·论文的主要工作 | 第8-9页 |
| ·论文的结构安排 | 第9-10页 |
| 第2章 相关研究与技术 | 第10-20页 |
| ·安全协议 | 第10-15页 |
| ·安全协议的背景及分类 | 第10-11页 |
| ·安全协议的形式化分析技术 | 第11-15页 |
| ·统一建模语言UML | 第15-18页 |
| ·UML概述 | 第15页 |
| ·UML的语法和语义 | 第15-16页 |
| ·UML的建模机制 | 第16-18页 |
| ·UML的模型检测技术 | 第18-20页 |
| 第3章 模型检测工具SPIN | 第20-26页 |
| ·SPIN概述 | 第20-21页 |
| ·SPIN的特点 | 第20-21页 |
| ·基于SPIN的协议分析 | 第21页 |
| ·SPIN的建模语言PROMELA | 第21-25页 |
| ·数据类型 | 第22页 |
| ·进程说明 | 第22-23页 |
| ·信息传递 | 第23-24页 |
| ·流向控制 | 第24-25页 |
| ·线性时态逻辑LTL | 第25-26页 |
| 第4章 安全协议UML模型及对应PROMELA语义转换 | 第26-36页 |
| ·安全协议的UML模型 | 第26-29页 |
| ·安全协议的类图 | 第26-27页 |
| ·安全协议的序列图 | 第27-28页 |
| ·安全协议的状态图 | 第28-29页 |
| ·UML模型的PROMELA语义转换 | 第29-33页 |
| ·类图Class Diagram的PROMELA语义 | 第29-30页 |
| ·序列图Sequence Diagram的PROMELA语义 | 第30-31页 |
| ·状态图StatesChart的PROMELA语义 | 第31-33页 |
| ·转换工具的分析与设计 | 第33-36页 |
| 第5章 UML模型实例的形式化转换 | 第36-42页 |
| ·Gavin Lowe小系统模型和Dolev-Yao模型 | 第36页 |
| ·NS协议类图的转换 | 第36-37页 |
| ·NS协议状态图的转换 | 第37-38页 |
| ·NS协议顺序图的转换 | 第38-42页 |
| 第6章 总结与展望 | 第42-44页 |
| ·总结 | 第42页 |
| ·下一步工作 | 第42-44页 |
| 致谢 | 第44-45页 |
| 参考文献 | 第45-48页 |
| 攻读学位期间的研究成果 | 第48页 |
