摘要： 研究ATL逻辑及其在电子商务协议形式化分析中的应用，对Kremer提出的方法进行扩展，使之在考虑公平等特性的同时能够分析协议的安全性。用该方法对周明天等人提出的FNORP协议及其变种进行了严格的形式化分析，结果表明基于博弈的ATL逻辑比传统的CTL更适合于描述和分析复杂电子商务协议。

关键词: 电子商务协议, 公平性, 安全性, 形式化分析, ATL逻辑

Abstract: This paper studies ATL logical and its applications in formal analysis of E-commerce protocols, and extends Dr Kremer’s approach to analyze security of protocols besides fairness. Strict formal analysis is made for FNORP protocol proposed by Zhou Mingtian etc. and is variations with this new method. The results indicate that the ATL logic based on game is more suitable to describe and analyze complex E-commerce protocols than traditional CTL.

Key words: e-commerce protocols, fairness, security, formal analysis, ATL

中图分类号: 

• TP309