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

• 作者: 张梅 张焕国 文静华 李祥 梁敏
• 来源期刊: 电子与信息学报
• 学科: 工学
• 关键词: 电子商务协议 公平性 安全性 形式化分析 ATL
• 年，卷（期）: 2007,（4）
• 所属期刊栏目: 论文
• 页码范围: 901-905
• 页数: 5页
• 分类号: TP309
• 字数: 5425字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张焕国	武汉大学计算机学院	244	4083	31.0	56.0
2	梁敏	贵州财经学院信息学院	12	44	3.0	6.0
3	李祥	贵州大学计算机软件与理论研究所	91	551	13.0	19.0
4	文静华	贵州大学计算机软件与理论研究所	58	334	10.0	15.0
10	张梅	贵州财经学院信息学院	43	257	9.0	14.0