| 摘要 | 第1-10页 |
| ABSTRACT | 第10-12页 |
| 第一章 绪论 | 第12-18页 |
| ·课题背景及意义 | 第12-13页 |
| ·国内外发展趋势及现状 | 第13-15页 |
| ·安全性证明模型 | 第13-14页 |
| ·自动化安全性证明的发展 | 第14-15页 |
| ·研究内容及难点 | 第15-17页 |
| ·论文结构安排 | 第17-18页 |
| 第二章 预备知识 | 第18-27页 |
| ·可计算理论 | 第18-21页 |
| ·公钥加密体制 | 第21-24页 |
| ·公钥加密体制的安全性定义 | 第21-24页 |
| ·安全性间的关系 | 第24页 |
| ·签名体制 | 第24-26页 |
| ·数学难题 | 第26页 |
| ·小结 | 第26-27页 |
| 第三章 自动化安全性证明方法研究 | 第27-41页 |
| ·计算模型 | 第27-29页 |
| ·基于游戏转换的可证明安全性 | 第29-32页 |
| ·可证明安全性 | 第29-30页 |
| ·基于游戏转换的安全性证明 | 第30-32页 |
| ·进程演算 | 第32-37页 |
| ·项代数的相关概念 | 第32-33页 |
| ·符号说明 | 第33页 |
| ·进程演算的语法 | 第33-36页 |
| ·类型系统 | 第36页 |
| ·两类密码原语及其安全性的形式化描述 | 第36-37页 |
| ·基于进程演算的密码体制安全性自动化证明方法 | 第37-40页 |
| ·游戏序列生成 | 第38-40页 |
| ·可证明安全性的判别条件 | 第40页 |
| ·小结 | 第40-41页 |
| 第四章 可证安全自动化分析系统 | 第41-50页 |
| ·可证安全自动化分析系统概述 | 第41-42页 |
| ·输入文件结构 | 第42-45页 |
| ·基于观察等价式的游戏转换 | 第45-47页 |
| ·游戏的语法转换和化简 | 第47-48页 |
| ·游戏的语法转换 | 第47-48页 |
| ·游戏的化简 | 第48页 |
| ·转换策略和证明路径搜索 | 第48-49页 |
| ·小结 | 第49-50页 |
| 第五章 ElGamal加密体制的自动化安全性证明 | 第50-64页 |
| ·数学架构 | 第50-52页 |
| ·概率 | 第50-51页 |
| ·循环群 | 第51页 |
| ·循环群的概率性质 | 第51-52页 |
| ·形式安全 | 第52-55页 |
| ·DDH假设 | 第52-53页 |
| ·熵平滑 | 第53页 |
| ·语义安全 | 第53-54页 |
| ·适应性选择密文攻击下密文不可区分（IND-CCA2） | 第54页 |
| ·加密体制的正确性 | 第54-55页 |
| ·ElGamal加密体制的安全性证明 | 第55-57页 |
| ·算法描述 | 第55页 |
| ·ElGamal加密体制的初始输入(IND-CPA) | 第55-57页 |
| ·证明结果 | 第57页 |
| ·带hash的ElGamal加密体制的安全性证明 | 第57-60页 |
| ·算法描述 | 第57-58页 |
| ·带hash的ElGamal加密体制的初始输入(IND-CPA) | 第58-60页 |
| ·证明结果 | 第60页 |
| ·证明失败案例 | 第60-62页 |
| ·ElGamal加密体制的初始输入（IND-CCA2） | 第60-62页 |
| ·证明结果 | 第62页 |
| ·小结 | 第62-64页 |
| 结束语 | 第64-66页 |
| 参考文献 | 第66-69页 |
| 附录 带hash的ElGamal加密体制自动化安全性证明过程（IND-CPA） | 第69-72页 |
| 作者简历 作者攻读硕士学位期间完成的主要工作 | 第72-73页 |
| 致谢 | 第73页 |
