| 摘要 | 第1-5页 |
| ABSTRACT | 第5-9页 |
| 第一部分 绪论 | 第9-28页 |
| 第1章 并发系统的研究方法、密码协议的形式化研究进展 | 第10-28页 |
| ·并发系统的研究方法概述 | 第10-19页 |
| ·密码协议的形式化研究进展 | 第19-25页 |
| ·本文的主要内容 | 第25-28页 |
| 第二部分 π-网 | 第28-84页 |
| 第2章 π-演算和Spi-演算简介 | 第29-39页 |
| ·π-演算 | 第29-32页 |
| ·π-演算的标号操作语义 | 第32-33页 |
| ·π-演算的结构同余 | 第33-34页 |
| ·进程的互模拟 | 第34-35页 |
| ·Spi-演算 | 第35-37页 |
| ·小结 | 第37-39页 |
| 第3章 π-网的定义和复合规则 | 第39-62页 |
| ·引言 | 第39-41页 |
| ·利用Petri网来表达π-演算进程的基本思想 | 第41-45页 |
| ·π-网的定义 | 第45-49页 |
| ·基本π-网 | 第49-50页 |
| ·π-网的变迁规则 | 第50-52页 |
| ·π-网的复合规则 | 第52-60页 |
| ·小结 | 第60-62页 |
| 第4章 π-网的强互模拟等价 | 第62-84页 |
| ·引言 | 第62-63页 |
| ·π-网的语义规则 | 第63-71页 |
| ·π-网和π-演算的系统等价 | 第71-77页 |
| ·π-网的强互模拟等价 | 第77-82页 |
| ·小结 | 第82-84页 |
| 第三部分 密码协议的π-网形式化描述和验证 | 第84-113页 |
| 第5章 密码协议的π-网形式化描述和分析 | 第85-103页 |
| ·引言 | 第85-86页 |
| ·改进的π-网 | 第86-90页 |
| ·基本π-网 | 第90-93页 |
| ·π-网的变迁规则 | 第93-94页 |
| ·π-网的复合规则和EPL 语言 | 第94-96页 |
| ·π-网对密码学协议的形式化描述 | 第96-100页 |
| ·小结 | 第100-103页 |
| 第6章 密码协议的π-网形式化验证 | 第103-113页 |
| ·引言 | 第103-104页 |
| ·密码协议系统的基本假设 | 第104页 |
| ·π-网的结构同余和归约法则 | 第104-105页 |
| ·密文环境 | 第105-107页 |
| ·π-网的观测等价关系 | 第107-109页 |
| ·协议的鉴别性和安全性 | 第109-112页 |
| ·小结 | 第112-113页 |
| 第四部分 总结与展望 | 第113-118页 |
| 第7章 总结与展望 | 第114-118页 |
| ·主要研究内容与结论 | 第114-116页 |
| ·主要创新之处 | 第116页 |
| ·展望 | 第116-118页 |
| 参考文献 | 第118-129页 |
| 致谢 | 第129-130页 |
| 攻读博士学位期间发表、录用或完成的学术论文 | 第130-132页 |