| 基于ATL的公平电子商务协议形式化分析 |
| |
| 引用本文： | 文静华, 李祥, 张焕国, 梁敏, 张梅. 基于ATL的公平电子商务协议形式化分析[J]. 电子与信息学报, 2007, 29(4): 901-905. doi: 10.3724/SP.J.1146.2005.01088 |
| |
| 作者姓名： | 文静华 李祥 张焕国 梁敏 张梅 |
| |
| 作者单位： | 贵州大学计算机软件与理论研究所,贵阳,550025;武汉大学计算机学院,武汉,430072;贵州财经学院信息学院,贵阳,550004;贵州大学计算机软件与理论研究所,贵阳,550025;武汉大学计算机学院,武汉,430072;贵州财经学院信息学院,贵阳,550004 |
| |
| 基金项目： | 国家自然科学基金
,
贵州省科学技术基金 |
| |
| 摘 要： | 针对传统时序逻辑LTL,CTL及CTL*等把协议看成封闭系统进行分析的缺点,Kremer博士(2003)提出用一种基于博弈的ATL(Alternating-time Temporal Logic)方法分析公平电子商务协议并对几个典型的协议进行了公平性等方面的形式化分析。本文讨论了ATL逻辑及其在电子商务协议形式化分析中的应用,进一步扩展了Kremer博士的方法,使之在考虑公平性等特性的同时能够分析协议的安全性。最后本文用新方法对Zhou等人(1999)提出的 ZDB协议进行了严格的形式化分析,结果发现该协议在非保密通道下存在两个可能的攻击：保密信息泄露和重放攻击。
|
| 关 键 词： | 电子商务协议 公平性 安全性 形式化分析 ATL |
| 文章编号： | 1009-5896（2007）04-0901-05 |
| 收稿时间： | 2005-08-30 |
| 修稿时间： | 2006-01-11 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《电子与信息学报》浏览原始摘要信息 |
|
点击此处可从《电子与信息学报》下载免费的PDF全文 |
|
