电子商务协议交易相关安全属性的形式化验证

电子商务协议是否达到设计者预期的安全目标直接关系着整个电子商务活动的安全性，因此电子商务协议安全性的分析研究近年来成为安全协议研究和电子商务研究领域的交叉热点。目前对电子商务协议的形式化分析仍主要集中在常规安全属性，如保密性和认证性的验证上。而对电子商务环境下交易相关安全属性，尤其是匿名性、公平性和原子性的支持不够。因此本申请项目以电子商务协议交易相关安全属性的形式化验证为主要研究内容，对交易相关安全属性进行抽象建模，对定理证明方法中的串空间理论进行扩展，使之适用于电子商务协议的形式化验证。探讨定理证明方法与模型检测方法的有效结合，开发出基于串空间的电子商务协议自动化综合验证工具。本项目致力于提高现有电子商务协议的安全性，辅助电子商务新协议的开发并最终促成公众接受基于这些协议的应用，为我国电子商务的进一步推广和普及提供技术支持。

本项目以电子商务协议交易相关安全属性的形式化验证为主要内容，根据不可否认性、公平性、匿名性和原子性的特点对串空间理论进行扩展，使其可以应用于交易相关安全属性的形式化验证。不可否认性研究中，我们对串空间理论的认证测试定理进行改进，使其能以主体向仲裁机构提交的消息片段还原关键过程，从而证明协议是否满足发送方或接收方的不可否认性。公平性研究中，我们借鉴有效市场假设提出最大利益法则，定义协议公平数据集来描述双方在各阶段掌握的信息，通过状态的变迁和互斥来描述主体可能的行为，计算目标公平数据表达式来判断主体掌握信息是否等价。匿名性研究中，借鉴其他学者扩展的串空间原语对电子投票协议匿名性进行了验证，指出数据匿名性实际上是保密性的一种。原子性研究中，我们认为原子性是电子商务“商品流”和“资金流”的一致性在“信息流”上的体现，用串空间原语将货币原子性、商品原子性、确认发送原子性描述出来，并对比了五种常用电子商务协议的原子性。项目执行期间出版《现代支付系统概论》教材1本，其中支付安全部分与本项目研究成果相关；发表期刊论文1篇，会议论文5篇，其中4篇被EI检索，并开发出安全协议自动验证软件一套，此外仍有两篇期刊论文在审稿中。人才培养上，培养硕士研究生7名，其中1名已毕业，3人将于2014年4月答辩。团队青年教师也得到锻炼并获得2011“四川省青年科技创新团队”资助。在国际交流与合作上，项目组邀请美国德州理工大学林漳希教授做为技术顾问，还邀请了加拿大纽芬兰纪念大学陈远筑教授、美国马里兰大学周丽娜教授等来我校进行交流并举办“光华讲坛”，承办了国际会议ICMeCG'2010的E-commerce Security论坛。项目组成员2人应邀赴美访问德州理工大学和莱特州立大学进行短期学术交流并做报告。国内合作研究方面，项目组与支付宝公司平台技术部建立了长期合作关系，多次卓有成效的交流为项目研究搜集到来自一线的需求和反馈；承办电子支付与电子商务研讨会1次，举办安全协议小型研讨会3次；与同济大学等高校同行进行学术交流十余次。在本项目研究的基础上，项目负责人做为主研人员参与了同济大学蒋昌俊副校长主持的国家自然科学基金可信软件重大专项项目“可信网络交易软件系统试验环境与示范应用”的申报工作并取得成功，项目号91218301。我方承担网络交易及支付流程及用户行为的安全性研究子课题的研究工作，进展顺利。