论文题目: 公平交换协议分析方法研究
论文类型: 博士论文
论文专业: 应用数学,数据安全
作者: 邢育红
导师: 李大兴
关键词: 公平交换协议,形式化分析,公平性,可行性,可追究性,适时中止性
文献来源: 山东大学
发表年度: 2005
论文摘要: 随着Internet的日益发展与普及,电子商务已成为基于Internet的现代经济活动的主要形式之一。电子商务交易中通常涉及到互不信任的交易方。电子商务活动的主要问题之一就是在任意两个互不信任的主体之间以一种公平的方式来交换电子数据。公平性和可行性成为这类电子商务协议的基本要求。公平交换协议可以使得参与交换的双方以公平的方式交换信息,这样,要么任何一方都可以得到对方的信息,要么双方都得不到对方的信息。 安全协议的设计是一个众所周知的难题,常因一些细微的问题产生缺陷。一个安全协议是否能达到设计者所期望的安全目标,需要对其进行严格的形式化分析。目前已有众多分析认证协议的形式化分析方法。公平交换协议是更为复杂的安全协议,它不仅需要满足认证协议的安全需求,还要考虑认证协议中未涉及到的若干安全性质,例如公平性、适时中止性、可追究性等。分析认证协议的方法不再直接适用于分析公平交换协议。 目前已有一些分析公平交换协议的形式化方法,其中有将分析认证协议的方法稍做扩展,使之适用于分析公平交换协议的,如Paulson的归纳法[87],Schneider的CSP方法[85],Vitaly Shmatikov和John Mitchell的Mur φ[89]等;有将一般协议检测工具用于分析公平交换协议的,如Boyd和Kearny提出了用协议规范演示工具Possum分析公平交换协议[88],Steve Kremer使用ATS模型检测工具Mocha检测协议[92]等。这些方法有的不涉及协议的分支(branch),有的不能分析协议的可追究性。目前对公平交换协议的分析是一个新的领域,一些方法、技术还有待于完善。 本文主要研究公平交换协议的分析方法,包括对公平交换协议要满足的主要特性:公平性、可行性、适时中止性、可追究性的分析。
论文目录:
目录
中文摘要
ABSTRACT
本文所用的符号
第一章 引言
1.1 安全协议的概念及分类
1.2 安全协议的安全性质
1.3 对安全协议进行形式化分析的意义
1.4 我们的研究内容
1.5 本文的结构
第二章 安全协议的形式化分析方法介绍
2.1 基于推理的方法
2.1.1 BAN逻辑
2.1.2 GNY逻辑
2.1.3 AT逻辑
2.1.4 SVO逻辑
2.2 基于攻击的自动化工具
2.2.1 基于CSP的模型检测工具FDR
2.2.2 Mur φ验证系统
2.2.3 Interrogator
2.2.4 NRL协议分析器
2.3 基于证明的方法
2.3.1 humanreadable证明法
2.3.2 Paulson归纳法
2.3.3 Schneider秩函数
2.3.4 串空间
2.3.5 Attacks限定法
2.4 总结
第三章 公平交换协议及其形式化分析方法
3.1 公平交换协议的演变
3.1.1 逐步交换协议
3.1.2 使用在线可信第三方(TTP)的公平交换协议
3.1.3 使用离线可信第三方的公平交换协议
3.2 公平交换协议要满足的特性
3.3 已有公平交换协议形式化分析方法介绍
3.3.1 CSP工具
3.3.2 归纳方法
3.3.3 Possum animation工具
3.3.4 Mur φ
3.3.5 Mocha
3.3.6 OFMC
3.4 总结
第四章 一种分析公平交换协议的新方法
4.1 对协议的目标及协议中传递的消息进行形式化描述
4.1.1 对协议的目标及协议中传递的消息进行形式化描述的方法
4.1.2 消息验证
4.1.3 对协议的目标及协议中传递的消息进行形式化描述的意义
4.2 协议结构
4.3 丛的搜索
4.3.1 丛的约简
4.3.2 寻找可能存在的丛的步骤
4.4 可行性分析
4.5 丛的公平性分析
4.6 适时中止性
4.7 总结
第五章 对两个挂号电子邮件协议的分析
5.1 对ASW挂号电子邮件协议的分析
5.1.1 协议简介
5.1.2 协议传递消息和协议目标的形式化描述
5.1.3 寻找所有可能存在的丛
5.1.4 协议的可行性分析
5.1.5 丛的公平性分析
5.1.6 适时中止性分析
5.1.7 关于检测效率
5.1.8 与已有分析结果的比较
5.2 ZDB协议的形式化分析
5.2.1 协议简介
5.2.2 协议传递消息及交易方目标的形式化描述
5.2.2.1 协议传递消息的形式化描述
5.2.2.2 交易方目标的形式化描述
5.2.3 搜索可能存在的丛
5.2.4 几点讨论
5.2.5 修改
5.3 总结
第六章 对两个合同签订协议的分析
6.1 MICALI协议的形式化分析
6.1.1 协议简介
6.1.2 协议传递消息和交易方目标的形式化描述
6.1.3 搜索可能存在的丛
6.1.4 丛的公平性分析
6.1.5 可行性分析
6.1.6 适时中止性分析
6.1.7 结论
6.2 BWZZ协议的形式化分析
6.2.1 协议简介
6.2.2 协议传递消息及交易方目标的形式化描述
6.2.3 搜索可能存在的丛
6.2.4 丛的公平性分析
6.2.5 可行性分析
6.2.6 适时中止性分析
6.2.7 结论
6.3 总结
第七章 自动分析算法
7.1 自动分析算法的思路
7.2 自动分析算法的初始输入
7.3 关键算法描述
第八章 公平交换协议的可追究性分析
8.1 方法介绍
8.1.1 逻辑构件：
8.1.2 公理系统
8.2 改进与扩展
8.3 可追究性分析之例
8.3.1 ASW协议的可追究性分析
8.3.2 ZDB协议的可追究性分析
8.4 总结
第九章 基于串空间模型的公平交换协议的形式化分析
9.1 基于串空间模型的公平交换协议形式化分析
9.1.1 串空间基本概念介绍
9.1.2 串空间方法扩展及交换协议公平性的形式化描述
9.2 ASOKAN-SHOUP-WAIDNER协议公平性的形式化分析
9.2.1 协议的目的
9.2.2 ASW协议的串空间模型
9.2.3 ASW协议的形式化分析
9.2.4 小结
9.3 RSA-CEMD协议分析及基于串空间模型的形式化证明
9.3.1 RSA-CEMD协议介绍
9.3.2 对RSA-CEMD协议的分析
9.3.3 对RSA-CEMD协议的修改
9.3.4 修改后RSA-CEMD协议的公平性分析
9.3.5 小结
9.4 总结
第十章 总结
10.1 本论文所做工作总结
10.2 将来的研究方向
参考文献
致谢
攻读学位期间完成的论文
博士期间参加科研项目情况
学位论文评阅及答辩情况表
发布时间: 2006-05-30
参考文献
- [1].基于e-Cash的电子商务交易协议研究[D]. 王茜.大连理工大学2003
- [2].电子商务协议形式化方法及模型检测技术的研究与应用[D]. 文静华.贵州大学2006
- [3].两种安全协议形式化理论的研究[D]. 赵华伟.山东大学2006
- [4].安全协议及其BAN逻辑分析研究[D]. 杨世平.贵州大学2007
- [5].协议安全测试理论和方法的研究[D]. 陈伟琳.中国科学技术大学2008
相关论文
- [1].用于公平交换的若干协议和规范的研究与应用[D]. 沈炜.浙江大学2003
- [2].安全协议形式化分析理论与方法[D]. 范红.中国人民解放军信息工程大学2003
- [3].安全协议形式化验证技术的研究与实现[D]. 李梦君.国防科学技术大学2005
- [4].安全协议分析的形式化理论与方法[D]. 王焕宝.合肥工业大学2006
- [5].一种分析和设计安全协议的新逻辑[D]. 缪祥华.西南交通大学2006
- [6].电子商务协议形式化方法及模型检测技术的研究与应用[D]. 文静华.贵州大学2006
- [7].两种安全协议形式化理论的研究[D]. 赵华伟.山东大学2006
- [8].安全协议的形式化方法及其应用的研究[D]. 华东明.中国科学院研究生院（计算技术研究所）2005
- [9].串空间理论及其在安全协议分析中的应用研究[D]. 龙士工.贵州大学2007
- [10].电子商务中的公平交换协议研究[D]. 刘景伟.西安电子科技大学2007