Formal analysis of e-commerce protocols based on game
Jinghua Wen · Journal of Communications · 2006
A new logical method based on game to analyze e-commerce protocols was proposed, the shortcoming of tra-ditional temporal logic that regards protocols as close system to analyze had been overcame. The adversarial and col-laboration 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 Zhou-Gollmann protocol was made by the new method. These works indicate that the alternating-time temporal logic (ATL) logic based on game is more suit-able to describe and analyze complex e-commerce protocols than traditional CTL.