基于应用PI演算的远程网络投票协议安全性自动化证明
| 摘要 | 第1-9页 |
| Abstract | 第9-11页 |
| 第1章 绪论 | 第11-18页 |
| ·引言 | 第11页 |
| ·课题研究背景 | 第11-15页 |
| ·网络投票定义和分类 | 第11-14页 |
| ·投票协议安全属性 | 第14-15页 |
| ·相关研究工作 | 第15-16页 |
| ·主要工作及结构安排 | 第16-18页 |
| ·主要工作 | 第16-17页 |
| ·结构安排 | 第17-18页 |
| 第2章 基于定理证明的安全协议形式化分析 | 第18-28页 |
| ·引言 | 第18-19页 |
| ·应用PI 演算 | 第19-23页 |
| ·语法和非形式化语义 | 第20-22页 |
| ·应用PI 演算的语义 | 第22-23页 |
| ·ProVerif | 第23-27页 |
| ·ProVerif 的系统结构 | 第24-25页 |
| ·ProVerif 语法 | 第25-26页 |
| ·安全属性 | 第26-27页 |
| ·本章小结 | 第27-28页 |
| 第3章 一种抗拒绝服务攻击性自动化分析模型 | 第28-45页 |
| ·引言 | 第28页 |
| ·基于定理证明的抗拒绝服务攻击性模型 | 第28-35页 |
| ·扩展的应用PI 演算 | 第30页 |
| ·定义和符号说明 | 第30-32页 |
| ·建模方法 | 第32-35页 |
| ·抗拒绝服务攻击性模型应用 | 第35-44页 |
| ·Acquisti 协议 | 第35-42页 |
| ·IEEE 802.11 四步握手协议 | 第42-44页 |
| ·本章小结 | 第44-45页 |
| 第4章 正确性与抗威胁性 | 第45-60页 |
| ·引言 | 第45页 |
| ·Backes 模型 | 第45-48页 |
| ·远程网络投票协议形式化模型 | 第45-46页 |
| ·安全属性形式化定义 | 第46-48页 |
| ·Backes 模型应用 | 第48-58页 |
| ·Meng 协议 | 第48-53页 |
| ·Acquisti 协议 | 第53-58页 |
| ·本章小结 | 第58-60页 |
| 第5章 总结与展望 | 第60-63页 |
| ·全文工作总结 | 第60-61页 |
| ·后继工作展望 | 第61-63页 |
| 参考文献 | 第63-68页 |
| 致谢 | 第68-69页 |
| 附录A 攻读学位期间所发表的学术论文目录 | 第69-71页 |
| 附录B 攻读学位期间所参加的项目目录 | 第71-72页 |
| 附录C 四步握手请求者Bob 的消息1 的模型 | 第72-73页 |
| 附录D 四步握手请求者Bob 的消息3 的模型 | 第73页 |
