中文摘要 | 第1-4页 |
Abstract | 第4-8页 |
第一章 绪论 | 第8-12页 |
·研究背景与意义 | 第8-10页 |
·电子商务发展现状 | 第8-9页 |
·对电子商务协议分析的意义 | 第9-10页 |
·国内外研究现状 | 第10页 |
·主要工作 | 第10-11页 |
·本文章节安排 | 第11页 |
·小结 | 第11-12页 |
第二章 电子商务协议简介 | 第12-20页 |
·安全电子商务协议概述 | 第12-16页 |
·电子商务协议运行环境中的主要角色 | 第12-13页 |
·安全电子商务协议的主要特性 | 第13-14页 |
·Digicash电子商务协议 | 第14-16页 |
·安全电子商务协议的缺陷 | 第16-18页 |
·常见攻击手段 | 第16-17页 |
·利用协议设计漏洞的攻击 | 第17-18页 |
·新的潜在安全威胁 | 第18-19页 |
·小结 | 第19-20页 |
第三章 基于CSP方法的模型检测技术 | 第20-33页 |
·安全协议的形式化分析基础 | 第20-22页 |
·模态逻辑技术 | 第20-21页 |
·模型检测技术 | 第21-22页 |
·定理证明技术 | 第22页 |
·CSP简介 | 第22-27页 |
·CSP中常用操作符 | 第23-24页 |
·进程 | 第24页 |
·CSP中的迹模型 | 第24-26页 |
·一个简单的CSP系统模型 | 第26-27页 |
·基于CSP的模型检测工具 | 第27-30页 |
·FDR | 第27-28页 |
·Casper | 第28-30页 |
·Casper/FDR中的攻击者模型 | 第30-32页 |
·攻击者能力分析 | 第30-31页 |
·具有攻击者的系统模型 | 第31页 |
·入侵者建模 | 第31-32页 |
·小结 | 第32-33页 |
第四章 基于CASPER/FDR2的电子商务协议形式化分析研究 | 第33-44页 |
·协议背景 | 第33-34页 |
·注册协议建模和分析 | 第34-41页 |
·注册协议 | 第34-36页 |
·注册协议的Casper建模 | 第36-38页 |
·检测结果及分析 | 第38-41页 |
·对注册协议的改进 | 第41-43页 |
·小结 | 第43-44页 |
第五章 电子商务协议扩展原子性的分析验证 | 第44-61页 |
·电子商务协议原子性的扩展 | 第44-46页 |
·接收验证原子性 | 第44-45页 |
·撤销交易原子性 | 第45-46页 |
·建立协议的CSP模型 | 第46-53页 |
·交易协议 | 第46-47页 |
·定义协议的运行环境 | 第47-48页 |
·定义协议数据、通信信道和进程 | 第48页 |
·对交易实体及系统整体进行建模 | 第48-50页 |
·建立协议目标声明 | 第50-51页 |
·协议的非常规状态模型 | 第51-53页 |
·FDR模型检测 | 第53-55页 |
·FDR检测 | 第53-54页 |
·检测结果调试 | 第54-55页 |
·协议原子性目标分析 | 第55-58页 |
·接收验证原子性分析 | 第55-57页 |
·撤销交易原子性分析 | 第57-58页 |
·协议改进 | 第58-60页 |
·小结 | 第60-61页 |
第六章 电子商务协议强匿名性分析验证 | 第61-76页 |
·基于CSP模型的协议匿名性分析理论基础 | 第61-63页 |
·匿名性定义 | 第61-62页 |
·观察者模型 | 第62-63页 |
·改进的电子商务协议匿名性形式化分析框架 | 第63-66页 |
·电子商务协议匿名性要求 | 第63-64页 |
·电子商务协议匿名性模型框架 | 第64-66页 |
·电子商务协议的匿名性模型建立 | 第66-71页 |
·协议环境建模 | 第67-68页 |
·参与实体建模 | 第68-69页 |
·匿名性目标建模 | 第69-71页 |
·结果验证和分析 | 第71-75页 |
·协议观察者 | 第71-72页 |
·模型检测结果和分析 | 第72页 |
·内部观察者模型检测和分析 | 第72-75页 |
·小结 | 第75-76页 |
第七章 总结和展望 | 第76-78页 |
·总结 | 第76页 |
·展望 | 第76-78页 |
参考文献 | 第78-82页 |
致谢 | 第82-83页 |
个人简历、在读期间研究成果以及发表的学术论文 | 第83页 |