| 致谢 | 第1-6页 |
| 摘要 | 第6-7页 |
| ABSTRACT | 第7-10页 |
| 1 绪论 | 第10-14页 |
| ·研究背景 | 第10-11页 |
| ·研究现状 | 第11-12页 |
| ·研究内容 | 第12-14页 |
| 2 理论背景 | 第14-23页 |
| ·VoIP概述 | 第14-16页 |
| ·基于SIP的VoIP安全机制 | 第16-17页 |
| ·ZRTP协议 | 第17-19页 |
| ·可信计算 | 第19-23页 |
| 3 可信ZRTP协议方案的设计 | 第23-35页 |
| ·ZRTP会话密钥协商 | 第23-26页 |
| ·可信度量方案的选取 | 第26-28页 |
| ·整合的可行性分析 | 第28-29页 |
| ·可信ZRTP协议方案 | 第29-35页 |
| ·ZRTP协议的修改方案 | 第29-32页 |
| ·可信ZRTP会话密钥协商 | 第32-35页 |
| 4 可信ZRTP协议的形式化验证 | 第35-53页 |
| ·安全协议的形式化分析技术 | 第35-41页 |
| ·模型检测技术 | 第36-37页 |
| ·模型检测工具SPIN | 第37-38页 |
| ·SPIN/ProMeLa模型 | 第38-40页 |
| ·SPIN的图形界面XSPIN | 第40-41页 |
| ·可信ZRTP协议建模 | 第41-46页 |
| ·可信ZRTP协议的抽象化 | 第41-42页 |
| ·可信ZRTP协议的ProMeLa模型 | 第42-46页 |
| ·可信ZRTP协议的安全属性及其线性时序逻辑描述 | 第46-49页 |
| ·抽象化的可信ZRTP协议的安全属性 | 第46-47页 |
| ·抽象化的可信ZRTP协议的LTL描述 | 第47-49页 |
| ·使用XSPIN验证可信ZRTP协议的ProMeLa模型 | 第49-53页 |
| 5 可信ZRTP协议的改进 | 第53-62页 |
| ·可信ZRTP协议抽象模型的优化 | 第53页 |
| ·可信ZRTP协议ProMeLa模型的优化 | 第53-55页 |
| ·使用XSPIN验证优化的ProMeLa模型 | 第55-56页 |
| ·改进可信ZRTP协议 | 第56-62页 |
| ·可信ZRTP协议的修改方案 | 第56-59页 |
| ·改进后的可信ZRTP会话密钥协商 | 第59-62页 |
| 6 总结和展望 | 第62-64页 |
| ·论文总结 | 第62页 |
| ·不足与展望 | 第62-64页 |
| 参考文献 | 第64-66页 |
| 作者简历 | 第66-68页 |
| 学位论文数据集 | 第68页 |