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

Formal analysis of e-commerce protocols based on game

提出用一种新的基于博弈的逻辑方法分析电子商务协议,克服了传统时序逻辑把协议看成封闭系统进行分析的缺点。新方法可以成功地对电子商务中的对抗与合作行为进行描述,能够分析协议的保密性、安全性、非否认性及公平性等。最后用新方法对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.