| 摘要 | 第1-7页 |
| ABSTRACT | 第7-11页 |
| 第一章 绪论 | 第11-16页 |
| ·研究背景与意义 | 第11-12页 |
| ·国内外研究现状 | 第12-14页 |
| ·非概率框架下使用逻辑再结合model checking 验证 | 第13页 |
| ·在非概率框架下用进程演算建模再结合互模拟验证 | 第13-14页 |
| ·对带概率的匿名协议使用逻辑再结合model checking 验证 | 第14页 |
| ·香农的熵理论 | 第14页 |
| ·研究内容 | 第14-15页 |
| ·论文的结构 | 第15-16页 |
| 第二章 PAPi | 第16-25页 |
| ·语法 | 第16-18页 |
| ·其他的概念 | 第18-19页 |
| ·语义 | 第19-21页 |
| ·执行序列 | 第21-23页 |
| ·等价关系 | 第23-25页 |
| 第三章 进程之间的度量 | 第25-33页 |
| ·state-metric | 第25-27页 |
| ·计算的方法 | 第27-29页 |
| ·metric 与互模拟的联系 | 第29-33页 |
| 第四章 匿名度的描述 | 第33-38页 |
| ·匿名性的分类 | 第33页 |
| ·匿名度的定义（按消息主体划分） | 第33-35页 |
| ·匿名度的定义（按匿名动作划分） | 第35-36页 |
| ·一些例子 | 第36-38页 |
| 第五章 实例分析 | 第38-45页 |
| ·问题的介绍 | 第38-39页 |
| ·概率用户 | 第39-42页 |
| ·DCP 问题的建模 | 第39-40页 |
| ·实例分析与结果 | 第40-42页 |
| ·不确定用户 | 第42-43页 |
| ·小结 | 第43-45页 |
| 第六章 总结与展望 | 第45-47页 |
| ·主要结论 | 第45页 |
| ·不足之处与未来展望 | 第45-47页 |
| 参考文献 | 第47-50页 |
| 符号与标记(附录1) | 第50-51页 |
| 致谢 | 第51-52页 |
| 攻读硕士学位期间已发表或录用的论文 | 第52-55页 |
| 上海交通大学学位论文答辩决议书 | 第55页 |