公钥密码体制可证安全性自动化分析描述模型的设计与实现
| 目录 | 第1-7页 |
| 表目录 | 第7-8页 |
| 图目录 | 第8-9页 |
| 摘要 | 第9-10页 |
| ABSTRACT | 第10-11页 |
| 第一章 引言 | 第11-18页 |
| ·课题背景 | 第11-13页 |
| ·国内外研究现状 | 第13-14页 |
| ·课题来源和主要工作 | 第14-16页 |
| ·课题的难点和创新点 | 第16页 |
| ·论文的结构安排 | 第16-18页 |
| 第二章 预备知识 | 第18-24页 |
| ·可证明安全性理论 | 第18-19页 |
| ·计算复杂度模型 | 第19-22页 |
| ·数字签名体制及其安全性定义 | 第20-21页 |
| ·公钥加密体制及其安全性定义 | 第21-22页 |
| ·基于游戏序列的安全性证明 | 第22-23页 |
| ·小结 | 第23-24页 |
| 第三章 基于进程演算的形式化描述模型 | 第24-34页 |
| ·符号表 | 第24页 |
| ·进程演算 | 第24-27页 |
| ·进程演算基础 | 第25-26页 |
| ·进程观察等价 | 第26-27页 |
| ·形式化描述模型 | 第27-32页 |
| ·项和进程 | 第28-29页 |
| ·操作语义 | 第29-32页 |
| ·安全目标的描述 | 第32页 |
| ·安全性证明 | 第32-33页 |
| ·语法转换 | 第32-33页 |
| ·依据密码原语代数性质或安全假设的转换 | 第33页 |
| ·小结 | 第33-34页 |
| 第四章 公钥密码体制形式化描述规范 | 第34-43页 |
| ·设计原则与目标 | 第34页 |
| ·描述规范 | 第34-39页 |
| ·签名攻击游戏的例子 | 第39-42页 |
| ·攻击游戏的描述 | 第39-40页 |
| ·观察等价式的描述 | 第40-41页 |
| ·相关恒等式的描述 | 第41页 |
| ·证明目标的描述 | 第41-42页 |
| ·使用方法 | 第42页 |
| ·小结 | 第42-43页 |
| 第五章 解析器的设计与实现 | 第43-52页 |
| ·解析器的功能概述 | 第43-44页 |
| ·词法分析程序的设计 | 第44-47页 |
| ·正则表达式 | 第45-46页 |
| ·LEX源程序 | 第46-47页 |
| ·语法分析程序的设计 | 第47-51页 |
| ·BNF文法 | 第48-49页 |
| ·YACC源程序 | 第49-51页 |
| ·冲突处理和错误处理 | 第51页 |
| ·小结 | 第51-52页 |
| 第六章 自动化证明系统的设计与实现 | 第52-65页 |
| ·系统的架构设计 | 第52-53页 |
| ·设计目标 | 第52页 |
| ·系统架构 | 第52-53页 |
| ·系统核心模块设计 | 第53-54页 |
| ·控制调度模块 | 第54-58页 |
| ·存储结构 | 第55-56页 |
| ·对单个结点转换 | 第56-57页 |
| ·系统控制的完成 | 第57-58页 |
| ·系统的输出和界面设计 | 第58-60页 |
| ·系统输出 | 第58-59页 |
| ·界面设计 | 第59-60页 |
| ·试验结果 | 第60-63页 |
| ·应用举例 | 第60-63页 |
| ·试验结果 | 第63页 |
| ·小结 | 第63-65页 |
| 结束语 | 第65-66页 |
| 参考文献 | 第66-69页 |
| 附录A 操作语义 | 第69-71页 |
| 附录B BNF文法 | 第71-74页 |
| 附录C 签名攻击游戏的描述 | 第74-76页 |
| 附录D 签名攻击游戏的证明 | 第76-83页 |
| 作者简历 作者攻读硕士学位期间完成的主要工作 | 第83-84页 |
| 致谢 | 第84页 |
