公平的电子合同签署协议的博弈分析与改进  

Game-based analysis and improvement of fair contract signing protocol

作　　者：翁立晨[1] 汪学明[1] 

机构地区：[1]贵州大学计算机科学与信息学院,贵州贵阳550025

出　　处：《计算机工程与设计》2010年第24期5347-5350,5362,共5页Computer Engineering and Design

基　　金：国家自然科学基金项目(60963023);贵州大学引进人才科研基金项目((2008)005号)

摘　　要：为了克服传统时序逻辑以封闭系统方式分析协议的缺点,根据电子合同签署协议的特点引入一种基于博弈的ATL逻辑形式化分析方法。利用该方法分析了一个公平的电子合同签署协议,发现该协议存在不满足公平性和时限性的缺陷。通过向协议中添加额外的时间控制信息和Abort子协议对该协议进行了改进,并使用Mocha模型检测工具以ATL公式和In-variant Checking相结合的方式对改进协议的公平性和时限性进行有效地验证。实验结果表明,改进后的协议满足公平性和时限性。In order to overcome the shortcoming of traditional temporal logic that regards protocols as close system to analyze,an ATL analysis method based on game logic is introduced based on the characteristic of electronic contract signing protocol.This method is ap-plied to formal analyzing a fair contract signing protocol,and some defects are found which don’t satisfy the timeliness and the fairness.An improvement protocol is proposed which fixe the flaw by adding extra time limit information and an abort sub-protocol into protocol message and adopting Mocha to validate the fairness and the timeliness of the protocol by ATL formula and invariant checking.It is found that the improvement protocol satisfy the timeliness and the fairness.

关 键 词：电子合同签署 形式化分析 时限性 公平性 博弈 MOCHA 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]