| 摘要 | 第1-5页 |
| ABSTRACT | 第5-10页 |
| 第一章 绪论 | 第10-14页 |
| ·安全协议 | 第10页 |
| ·安全协议的形式化方法 | 第10-12页 |
| ·时序逻辑和分布式时序逻辑 | 第12-13页 |
| ·本文的研究内容及结构安排 | 第13-14页 |
| 第二章 分布式时序逻辑 | 第14-27页 |
| ·DTL 的语形 | 第14-15页 |
| ·DTL 的语义 | 第15页 |
| ·DTL 中公式的等价性定理 | 第15-26页 |
| ·对偶律 | 第16-17页 |
| ·幂等律 | 第17-20页 |
| ·吸收律 | 第20-22页 |
| ·分配律 | 第22-24页 |
| ·扩张律 | 第24-26页 |
| ·本章小结 | 第26-27页 |
| 第三章 用分布式时序逻辑验证IEEE802.11i 协议 | 第27-41页 |
| ·IEEE802.11i 协议 | 第27页 |
| ·IEEE802.11i 协议的DTL 模型 | 第27-33页 |
| ·消息以及和消息有关的概念 | 第27-28页 |
| ·基于信道的模型 | 第28-29页 |
| ·DTL 的公理 | 第29-33页 |
| ·K 公理以及由K 公理推出的公理 | 第29-30页 |
| ·新鲜性和唯一性公理 | 第30-31页 |
| ·关于信道CH 和主体的公理 | 第31-32页 |
| ·关于公钥、私钥和共享密钥的公理 | 第32-33页 |
| ·引理及命题 | 第33页 |
| ·IEEE802.11i 协议的网络模型和事件结构模型 | 第33-36页 |
| ·IEEE802.11i 协议的认证性 | 第36-40页 |
| ·申请者认证 | 第36-39页 |
| ·认证者认证 | 第39-40页 |
| ·认证服务器认证 | 第40页 |
| ·本章小结 | 第40-41页 |
| 第四章 分布式计算树时序逻辑 | 第41-51页 |
| ·DCTL 的语形 | 第41页 |
| ·DCTL 的语义 | 第41-46页 |
| ·DCTL 中公式的等价性定理 | 第46-50页 |
| ·对偶律 | 第46-47页 |
| ·分配律 | 第47-48页 |
| ·扩张律 | 第48-50页 |
| ·本章小节 | 第50-51页 |
| 第五章 用分布式计算树时序逻辑分析多方认证电子邮件协议 | 第51-65页 |
| ·多方认证电子邮件协议 | 第51-53页 |
| ·多方认证电子邮件协议的网络模型 | 第53-57页 |
| ·没有可信第三方的参与 | 第53-54页 |
| ·有可信第三方的参与 | 第54-57页 |
| ·用 DCTL 描述多方认证电子邮件协议 | 第57-60页 |
| ·交换子协议的事件结构模型 | 第57-58页 |
| ·取消子协议的事件结构模型 | 第58-59页 |
| ·结束子协议的事件结构模型 | 第59-60页 |
| ·多方认证电子邮件协议的不可否认性 | 第60-63页 |
| ·发起者的不可否认性 | 第60-62页 |
| ·没有可信第三方的参与 | 第60-61页 |
| ·有可信第三方的参与 | 第61-62页 |
| ·接收者的不可否认性 | 第62-63页 |
| ·没有可信第三方的参与 | 第62-63页 |
| ·有可信第三方的参与 | 第63页 |
| ·本章小结 | 第63-65页 |
| 第六章 总结与展望 | 第65-66页 |
| ·总结 | 第65页 |
| ·展望 | 第65-66页 |
| 参考文献 | 第66-70页 |
| 致谢 | 第70-71页 |
| 在学期间研究成果及发表的学术论文 | 第71-72页 |
| 附录 | 第72-79页 |
