| 摘要 | 第1-4页 |
| Abstract | 第4-5页 |
| 目录 | 第5-7页 |
| 第1章 序言 | 第7-9页 |
| 第2章 安全协议验证 | 第9-19页 |
| ·安全协议 | 第9-10页 |
| ·安全协议攻击 | 第10-11页 |
| ·安全协议形式化分析 | 第11-19页 |
| 第3章 基于知识理论的安全协议形式化验证方法 | 第19-37页 |
| ·加密信息交换模型 | 第19-22页 |
| ·协议的实例化空间(Instantiation Space) | 第22-26页 |
| ·协议的验证逻辑 | 第26-34页 |
| ·观察理论(Observation Theory) | 第34-37页 |
| 第4章 基于知识的安全协议验证方法在对称密钥交换协议中的应用 | 第37-71页 |
| ·Kao Chow协议的形式化验证 | 第37-51页 |
| ·Yahalom协议的形式化验证 | 第51-69页 |
| ·小结 | 第69-71页 |
| 第5章 SPV工具在对称密钥交换协议中的应用 | 第71-79页 |
| ·输入文件语法定义 | 第71-75页 |
| ·对称密钥交换协议的SPV工具验证 | 第75-79页 |
| 第6章 总结与展望 | 第79-83页 |
| ·工作总结 | 第79-80页 |
| ·工作展望 | 第80-83页 |
| 参考文献 | 第83-89页 |
| 附录 协议验证源文件 | 第89-111页 |
| 1 Wide Mouthed Frog Protocol | 第89-91页 |
| 2 BAN concrete Andrew Secure RPC | 第91-94页 |
| 3 Carlsen's Secret Key Initiator Protocol | 第94-97页 |
| 4 Denning Sacco Protocol | 第97-99页 |
| 5 Kehne Langendorfer Schoenwalder KLS | 第99-103页 |
| 6 Neumann Stubblebine | 第103-106页 |
| 7 Otway-Rees Protocol | 第106-111页 |
| 致谢 | 第111-113页 |
| 原创性声明 | 第113页 |
