基于博弈的电子商务协议分析  

Formal analysis of e-commerce protocols based on game

作　　者：文静华[1] 张梅[1] 李祥[2] 

机构地区：[1]贵州财经学院信息学院,贵州贵阳550004 [2]贵州大学计算机软件与理论研究所,贵州贵阳550025

出　　处：《通信学报》2006年第3期73-78,共6页Journal on Communications

基　　金：贵州省科学技术基金资助项目(20052111);贵州省教育厅自然科学基金资助项目(2004219)~~

摘　　要：提出用一种新的基于博弈的逻辑方法分析电子商务协议,克服了传统时序逻辑把协议看成封闭系统进行分析的缺点。新方法可以成功地对电子商务中的对抗与合作行为进行描述,能够分析协议的保密性、安全性、非否认性及公平性等。最后用新方法对Zhou-Gollmann协议进行了严格的形式化分析。结果表明基于博弈的ATL逻辑比传统的基于计算树逻辑(CTL)更适合于描述和分析复杂电子商务协议。A new logical method based on game to analyze e-commerce protocols was proposed, the shortcoming of traditional temporal logic that regards protocols as close system to analyze had been overcame. The adversarial and collaboration in electronic commerce could be described correctly by the new method, and the privacy, security, non-repudiation, fairness could be analyzed. In the end, strict formal analysis for Zbeu-Gollmann protocol was made by the new method. These works indicate that the alternating-time temporal logic （ATL） logic based on game is more suitable to describe and analyze complex e-commerce protocols than traditional CTL.

关 键 词：电子商务协议 安全性 公平性 ATL 

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