[01275790]基于形式化方法的电子商务多主体交互机制研究及应用

项目依据浙江省自然科学基金项目，为适应不同电子商务协议具有的不同规定而导致不同的复杂性、不同的开销、不同的安全和不同的风险，针对电子商务协议具有的博弈特征和并发分布性特点，建立基于动态博弈理论为基础结合进程演算模型的电子商务协议形式化框架，在该框架下形式化定义电子商务协议的安全性质，分析验证电子商务协议的正确性和安全性，并辅助规范说明和设计电子商务协议。

电子商务协议形式化研究已成为热点前沿研究，但该领域尚有诸多急待解决的问题：（1）电子商务协议运行在一个十分复杂的公开环境中，攻击者处处存在，即使参与协议的主体也可能是不诚实的。而目前的研究对协议所做的基本假设过严， 使研究不能接近实际情况。

（2）对电子商务协议的安全性目标难以界定，存在各种不同的观点，对特定安全性质如原子性、匿名性等属性研究工作还很少。

（3）如何将形式化方法用于协议规范说明和设计阶段，使之不仅仅用于分析已有协议的安全性，从而可以极小的代价尽可能早地发现错误，这方面的工作还相当少。

本成果以动态博弈理论为基础结合进程演算模型建立电子商务协议形式化框架，精确描述了电子商务协议，并在统一的框架下形式化定义电子商务协议的安全性要求，分析验证电子商务协议的正确性和安全性，规范说明和辅助设计了电子商务协议具体实现的内容。

具体包括：

（1）研究电子商务系统的体系结构，明确电子商务系统中买卖双方、银行和为各方所信任的第三方等主体之间的交互关系；

（2）以动态博弈理论为基础，结合项目申请者博士学位论文中提出的GSPM模型，构建一个适合于电子商务协议的形式化框架，形式化定义电子商务协议的安全性要求；

（3）为各种电子商务协议形式化建模，用模型检测方法验证电子商务协议是否存在漏洞，并规范说明和辅助设计电子商务协议；

（4）研究新型计算模式云计算下SLA协议，主要从云服务的角度分析IaaS协商协议，云服务拍卖机制等。

其主要创新点包括：

（1）利用博弈理论工具，建立了安全交换协议的博弈论模型，并研究了两个重要的性质---非否认性和公平性，利用该模型对一种认证电子邮件协议---MD机制进行了分析。

进一步根据不完全信息扩展博弈理论，建立了电子商务公平交换的协议博弈以及其博弈树，给出了一个线性时间算法，同时利用该模型在分析ASW协议时发现了其中的瑕疵。

基于博弈理论和电子商务协议的特点，从比公平性稍弱的理性角度对电子商务协议进行了博弈建模，在理性情况下，博弈某一方不遵守协议并不会给他带来更高的收益，即他没有动力去违反协议，并用理性的观点对电子商务协议进行分析。

对于小额微支付协议，发现保证交易双方公平性需要的支出高于微支付交易本身的金额，从而保证公平性不太适用此种情况提出理性交换协议的必要性，并利用博弈理论中纳什均衡的概念形式化定义了理性交换协议。

根据GSPM模型和博弈理论对认证协议进行了形式化分析，证明了该方法的有效性，并对NSPK协议进行了实例研究。针对云服务SLA协议，通过博弈研究如何实现任务的分解以避免违例。利用WSLA，研究了IaaS协商协议的设计。同时通过机制设计理论，分析了自利的个体间如何行为，并根据激励相容的性质研究合理的机制。

本项目与电子商务产业结合，满足了电子商务企业的实际需求，产生了较大的经济及社会效益，取得相关知识产权及优秀科研成果、优秀论文奖等。

项目为电子商务的发展奠定了强大的技术基础，具有很好的发展前景和推广价值。