基于ATL的公平电子商务协议形式化分析

摘要：

针对传统时序逻辑LTL,CTL及CTL*等把协议看成封闭系统进行分析的缺点,Kremer博士(2003)提出用一种基于博弈的ATL(Alternating-time Temporal Logic)方法分析公平电子商务协议并对几个典型的协议进行了公平性等方面的形式化分析.本文讨论了ATL逻辑及其在电子商务协议形式化分析中的应用,进一步扩展了Kremer博士的方法,使之在考虑公平性等特性的同时能够分析协议的安全性.最后本文用新方法对Zhou等人(1999)提出的ZDB协议进行了严格的形式化分析,结果发现该协议在非保密通道下存在两个可能的攻击:保密信息泄露和重放攻击.

关键词：电子商务协议、公平性、安全性、形式化分析、ATL

所属期刊栏目：29

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金40261009;贵州省科学技术基金20052111

在线出版日期：2007-05-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：901-905