基于模型检测工具SPIN的安全协议分析和验证
| 原创性声明 | 第1-3页 |
| 关于学位论文使用授权的声明 | 第3-4页 |
| 摘要 | 第4-5页 |
| ABSTRACT | 第5-6页 |
| 目录 | 第6-8页 |
| 第一章 绪论 | 第8-11页 |
| §1.1 背景 | 第8-9页 |
| ·分析和验证安全协议的困难性 | 第8-9页 |
| ·国内外研究现状 | 第9页 |
| §1.2 本文工作 | 第9-10页 |
| §1.3 论文结构 | 第10-11页 |
| 第二章 理论背景 | 第11-26页 |
| §2.1 模型检测理论基础 | 第11-13页 |
| ·概念及相关技术 | 第11-12页 |
| ·应用 | 第12-13页 |
| §2.2 模型检测工具SPIN | 第13-22页 |
| ·SPIN的基本结构 | 第14-15页 |
| ·Promela语言 | 第15-16页 |
| ·线性时态逻辑(LTL) | 第16-19页 |
| ·基本算法 | 第19-22页 |
| §2.3 安全协议形式化分析方法理论基础 | 第22-25页 |
| ·形式化方法分析安全协议概述 | 第22页 |
| ·常见的形式化分析安全协议的方法 | 第22-25页 |
| BAN逻辑及BAN类逻辑 | 第23页 |
| 串空间(strand space)模型 | 第23-24页 |
| CSP模型与分析方法 | 第24页 |
| 定理证明的方法及模型检测方法 | 第24-25页 |
| §2.4 小结 | 第25-26页 |
| 第三章 基于SPIN的安全协议形式化分析和验证 | 第26-51页 |
| §3.1 协议描述 | 第27-29页 |
| ·Netbill协议的内容 | 第27-28页 |
| ·Netbill协议的说明 | 第28-29页 |
| §3.2 协议的行为抽象 | 第29-36页 |
| ·模型的PROMELA结构 | 第30-32页 |
| ·主体的状态及行为描述 | 第32-36页 |
| §3.3 协议的属性说明 | 第36-39页 |
| ·SPIN可验证的正确性属性 | 第37页 |
| ·协议的时态行为分析 | 第37-39页 |
| §3.4 协议行为模拟分析 | 第39-45页 |
| §3.5 属性验证结果分析 | 第45-49页 |
| ·LTL属性P1的验证 | 第45-48页 |
| ·关于其它属性的验证 | 第48-49页 |
| §3.6 和SMV方法比较 | 第49-50页 |
| §3.7 小结 | 第50-51页 |
| 第四章 结论及展望 | 第51-53页 |
| §4.1 论文的主要工作 | 第51页 |
| §4.2 与其他方法的比较 | 第51页 |
| §4.3 进一步的工作 | 第51-53页 |
| 参考文献 | 第53-55页 |
| 致谢 | 第55-56页 |
| 附录1 | 第56-58页 |
| 附录2 | 第58-60页 |
