电子支付协议的博弈逻辑模型与形式化分析  

Formal Analysis of Electronic Payment Protocols Based on Game Logic

作　　者：文静华[1] 张梅[1] 张焕国[2] 

机构地区：[1]贵州财经学院信息学院,贵州贵阳550004 [2]武汉大学计算机学院,湖北武汉4300724

出　　处：《微电子学与计算机》2007年第9期113-115,共3页Microelectronics & Computer

基　　金：国家自然科学基金项目(40261009);贵阳市科学技术发展基金项目(20072111)

摘　　要：提出用一种新的基于博弈逻辑ATL(Alternating-time Temporal Logic)的电子支付协议建模与分析方法。新方法克服了传统时序逻辑把协议看成封闭系统进行分析的缺点,可以成功地对电子商务中的对抗与合作行为进行描述。利用新方法对Bolignano协议进行了严格的形式化分析,发现该协议不能满足公平性要求。A new logical method based on game to model and analyze electronic payment protocols is proposed in this paper. Strict formal analysis for Bolignano protocol is made by this new method, and Bolignano protocol is discovered non-fairness.

关 键 词：电子支付协议 公平性 形式化分析 ATL 

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