乐观公平交换协议的形式化分析技术研究

摘要

乐观公平交换协议是一类典型的安全协议,用于在两个或多个主体之间安全、高效地进行电子交易。与其它安全协议相比,乐观公平交换协议在结构上较为复杂,从而更容易存在安全缺陷,同时也为其形式化分析带来了挑战。
　　本文主要研究了乐观公平交换协议的形式化分析技术,所取得的主要研究结果有:
　　(1)深入剖析了IETF(Internet Engineering Task Force)的IPSEC工作组提交的IKEv2协议草案;在对协议进行形式建模,以及应用CTL对相应的安全性质进行形式描述的基础上,借助SMV分析了协议的认证性、秘密性、和完整性,发现了两个攻击;对这两个攻击所产生的影响进行了讨论。
　　(2)针对乐观公平交换协议,提出了一种基于有限状态机的分析模型;应用该模型,借助SMV分析了GJM电子合同签订协议,检测出由V.Shmatikov首先发现的缺陷;分析了ASW电子合同签订协议,指出在协议实现过程中应该注意的问题;分析了FPH挂号电子邮件协议,发现该协议存在安全缺陷。
　　(3)针对所发现的安全缺陷,对FPH挂号电子邮件协议进行了改进;应用上述模型,对改进后的协议进行模型检测分析,分析结果表明协议达到了安全要求。
　　(4)对C.W.Hao给出的协议运行模型及协议规格和分析框架进行扩充和改进,给出了一个较为完整的安全协议规格及验证系统;应用该系统,对ASW电子合同签订协议进行了规格,对其公平性进行了逻辑推证。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 概述

§1.1 研究背景及意义

§1.2 国内外研究现状

§1.3 研究内容

§1.4 论文安排

第二章 乐观公平交换协议

§2.1 安全协议与安全性质

§2.2乐观公平交换协议的特点

§2.3 若干典型的乐观公平交换协议

§2.4 小结

第三章 IKEv2协议的模型检测分析

§3.1 模型检测及SMV系统

§3.2 分析密钥分配和认证协议的基本思路

§3.3 IKEv2协议简介

§3.4 IKEv2协议的模型检测分析

§3.5 小结

第四章 乐观公平交换协议的模型检测分析

§4.1 乐观公平交换协议的一种分析模型

§4.2 GJM电子合同签订协议的模型检测分析

§4.3 ASW电子合同签订协议的模型检测分析

§4.4 FPH挂号电子邮件协议的模型检测分析

§4.5 FPH挂号电子邮件协议的改进及其模型检测分析

§4.6 小结

第五章 乐观公平交换协议的逻辑分析研究

§5.1 引言

§5.2 新的安全协议规格及验证系统

§5.3 ASW协议的规格及公平性证明

§5.4 小结

第六章 结论

参考文献

致谢

附：在读期间发表的论文