乐观公平交换协议形式化逻辑及其自动证明技术
| 中文摘要 | 第1-5页 |
| 英文摘要 | 第5-10页 |
| 1 绪论 | 第10-16页 |
| ·研究背景 | 第10-11页 |
| ·研究内容 | 第11-14页 |
| ·安全属性 | 第11-13页 |
| ·安全协议 | 第13-14页 |
| ·形式化方法 | 第14页 |
| ·论文主要工作和结构安排 | 第14-15页 |
| ·论文主要工作 | 第14-15页 |
| ·论文结构安排 | 第15页 |
| ·本章小结 | 第15-16页 |
| 2 相关背景知识 | 第16-22页 |
| ·命题模态逻辑句法和公理系统 | 第17页 |
| ·克里普克模型 | 第17-19页 |
| ·时序逻辑 | 第19-21页 |
| ·线性时序逻辑 | 第19-20页 |
| ·计算树逻辑 | 第20-21页 |
| ·本章小结 | 第21-22页 |
| 3 公平交换协议及其形式化技术研究综述 | 第22-44页 |
| ·引言 | 第22页 |
| ·公平交换协议研究综述 | 第22-31页 |
| ·公平交换的概念和一般模型 | 第22-23页 |
| ·公平交换协议分类及主要协议研究 | 第23-26页 |
| ·公平交换协议安全性定义 | 第26-28页 |
| ·公平交换协议研究中的主要问题分析 | 第28-31页 |
| ·公平交换协议的形式化技术研究综述 | 第31-42页 |
| ·基于信任逻辑的方法 | 第31-36页 |
| ·基于模型检测的方法 | 第36-39页 |
| ·其它方法 | 第39-40页 |
| ·分析和讨论 | 第40-42页 |
| ·本章小结 | 第42-44页 |
| 4 乐观公平交换协议形式化逻辑 | 第44-68页 |
| ·引言 | 第44-45页 |
| ·乐观公平交换协议形式化模型定义 | 第45-48页 |
| ·乐观公平交换协议形式逻辑 | 第48-56页 |
| ·逻辑定义 | 第48-54页 |
| ·推理公理 | 第54-55页 |
| ·逻辑描述和正确性证明 | 第55-56页 |
| ·案例分析 | 第56-65页 |
| ·PVG 协议分析 | 第56-61页 |
| ·JAB 协议分析 | 第61-65页 |
| ·分析与比较 | 第65-67页 |
| ·本章小结 | 第67-68页 |
| 5 乐观公平交换协议自动证明技术 | 第68-90页 |
| ·引言 | 第68页 |
| ·主要问题分析 | 第68-69页 |
| ·ISABELLE 定理证明器 | 第69-72页 |
| ·Isabelle 系统结构 | 第69-70页 |
| ·Isabelle 的逻辑 | 第70页 |
| ·Isabelle 定理证明方法 | 第70页 |
| ·Isabelle 证明理论 | 第70-72页 |
| ·案例分析 | 第72-87页 |
| ·ASW 协议描述 | 第72-75页 |
| ·ASW 协议攻击和改进 | 第75-76页 |
| ·ASW 协议形式化描述 | 第76-87页 |
| ·ASW 协议分析 | 第87页 |
| ·相关研究分析 | 第87-88页 |
| ·本章小结 | 第88-90页 |
| 6 乐观型电子支付协议设计及形式化分析 | 第90-114页 |
| ·引言 | 第90-91页 |
| ·电子支付协议的密码技术 | 第91-97页 |
| ·双线性映射理论和困难数学问题及假设 | 第91页 |
| ·部分盲签名机制定义 | 第91-93页 |
| ·部分盲签名机制安全模型定义 | 第93-95页 |
| ·部分盲签名算法设计 | 第95-97页 |
| ·基于椭圆曲线的公钥加密机制 | 第97页 |
| ·基于双线性对的短签名机制 | 第97页 |
| ·乐观型电子支付协议设计 | 第97-105页 |
| ·乐观型电子支付协议分析 | 第105-112页 |
| ·部分盲签名机制分析 | 第105-108页 |
| ·电子支付协议安全性分析 | 第108-110页 |
| ·对比分析 | 第110-112页 |
| ·本章小结 | 第112-114页 |
| 7 总结与展望 | 第114-116页 |
| ·全文总结 | 第114-115页 |
| ·进一步研究展望 | 第115-116页 |
| 致谢 | 第116-118页 |
| 参考文献 | 第118-128页 |
| 附录 | 第128页 |
| A. 作者在攻读学位期间发表的论文目录 | 第128页 |
| B. 作者在攻读学位期间参与项目情况 | 第128页 |
