串空间理论在电子商务协议形式化分析中的应用

摘要

电子商务协议是保障电子商务安全的一种重要手段。非否认性和公平性是电子商务协议的重要性质，但相对于认证协议和密钥分配协议的保密性和认证性，电子商务协议及其非否认性和公平性的形式化研究还不够充分。 论文对串空间模型的丛理论、诚实理论和认证测试理论进行深入的研究，并在此基础上探讨了将串空间模型应用于电子商务协议安全性形式化分析的方法。为了能反映电子商务协议中加密、签名、完整性保护等多种安全机制，扩展了密码原语，以满足分析复杂安全协议的需要。根据电子商务协议主体利益目标不一致、攻击主要来自内部的特点，扩展了攻击模型，对主体处理消息的能力进行了形式化的定义。为了解决电子商务协议中协议主体动态确定，协议执行路径不唯一确定的问题，扩展了串空间中结点间的因果依赖关系，来描述协议随着协议步骤的不断执行而使协议执行结果发生改变的内在逻辑关联。 论文应用扩展的串空间模型对安全电子支付协议SET的安全性进行了较为全面的分析，首次应用形式化的分析方法对SET的保密性、认证性及完整性进行了严格的论证。同时由于SET协议无法满足交易公平性的缺陷，提出了SET协议的一个改进版本，该版本能满足数字商品交易的公平性。

目录

文摘

英文文摘

声明

第1章绪论

1.1安全协议形式化分析

1.1.1安全协议的基本概念

1.1.2安全协议形式化分析

1.2国内外研究现状

1.3本文工作

1.4论文组织结构

第2章串空间模型

2.1串空间模型基础

2.1.1串空间模型的基本概念

2.1.2自由假设

2.1.3攻击者

2.1.4正确性概念

2.1.5实例分析

2.2理想与诚实

2.2.1理想与诚实

2.2.2应用理想与诚实分析Yahalom协议

2.3认证测试方法

2.3.1认证测试基本概念

2.3.2应用认证测试方法分析Yahalom协议

2.3.3 Yahalom协议改进

2.3.4认证协议的设计原则

2.4本章小结

第3章电子商务协议

3.1电子商务协议的基本概念

3.1.1电子商务协议的安全属性

3.1.2电子商务协议的基本结构

3.1.3电子商务协议的分类

3.2典型的电子商务协议

3.2.1安全电子交易协议SET

3.2.2 KM(Kremer Markowitch)协议

3.3本章小结

第4章串空间模型扩展

4.1电子商务协议的特点

4.1.1非否认性

4.1.2公平性

4.2串空间模型扩展

4.2.1密码原语的扩展

4.2.2攻击模型的扩展

4.2.3因果依赖关系的扩展

4.3实例分析

4.4本章小结

第5章SET协议的串空间模型分析

5.1 SET协议的串空间模型分析

5.1.1 SET协议支付过程的形式化模型

5.1.2 SET协议支付过程的串空间模型分析

5.2 SET协议的改进版本

5.3本章小结

第6章总结与展望

致谢

参考文献

发表论文