| 表目录 | 第6-7页 |
| 图目录 | 第7-8页 |
| 摘要 | 第8-9页 |
| Abstract | 第9页 |
| 第一章 引言 | 第11-18页 |
| 1.1 云计算发展现状与关键技术 | 第11-14页 |
| 1.2 安全协议形式化分析方法与自动化证明器介绍 | 第14-16页 |
| 1.3 本文研究内容与组织结构和主要创新点 | 第16-18页 |
| 第二章 计算的协议组合逻辑扩展 | 第18-33页 |
| 2.1 基于计算的协议分析模型 | 第18-20页 |
| 2.2 协议安全属性及其轨迹表示 | 第20-29页 |
| 2.2.1 若干基本概念 | 第20-23页 |
| 2.2.2 协议安全属性的轨迹表示 | 第23-29页 |
| 2.3 CPCL 逻辑系统 | 第29-33页 |
| 第三章 基于 TPM 的 IaaS 和 SaaS 协议设计 | 第33-41页 |
| 3.1 设计背景 | 第33-34页 |
| 3.1.1 Eucalyptus | 第33-34页 |
| 3.1.2 可信平台模块 | 第34页 |
| 3.2 整体架构设计 | 第34-36页 |
| 3.3 基础设施服务实现细节 | 第36-40页 |
| 3.3.1 服务注册 | 第36-37页 |
| 3.3.2 租用方上传数据 | 第37-38页 |
| 3.3.3 租用方获取计算资源 | 第38-39页 |
| 3.3.4 虚拟机迁移 | 第39-40页 |
| 3.4 软件服务实现细节 | 第40-41页 |
| 3.4.1 建立服务链接 | 第40-41页 |
| 第四章 基于 TPM 的 IaaS 与 SaaS 协议安全性分析 | 第41-49页 |
| 4.1 攻击者模型 | 第41页 |
| 4.2 IaaS 和 SaaS 服务过程的安全性证明 | 第41-49页 |
| 4.2.1 服务注册协议的安全性证明 | 第43-44页 |
| 4.2.2 建立服务链接协议的安全性证明 | 第44-45页 |
| 4.2.3 租用方获取计算资源协议的安全性证明 | 第45-47页 |
| 4.2.4 虚拟机迁移协议的安全性证明 | 第47-49页 |
| 结束语 | 第49-50页 |
| 附录 1 | 第50-52页 |
| 附录 2 | 第52-57页 |
| 参考文献 | 第57-61页 |
| 作者简历 攻读硕士学位期间完成的主要工作 | 第61-62页 |
| 致谢 | 第62页 |
