基于ATL逻辑的公平多方不可否认协议的分析与改进

摘要：

为了克服传统时序逻辑以封闭系统方式分析协议的缺点,引入一种基于博弈的ATL逻辑形式化分析方法。利用该方法分析了一个公平的多方不可否认协议,发现该协议存在不满足抗合谋性的缺陷,并提出了两种改进方案,使用Mocha模型检测工具以ATL公式和Invariant Checking相结合的方式对两种改进方案进行有效验证,结果表明改进后的协议满足不可否认性和抗合谋性。

关键词：不可否认性、形式化分析、公平性、博弈、Mocha

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

资助基金：国家自然科学基金项目200960963023号;贵州大学引进人才科研基金项目2008005号

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

页数：共6页

页码：21-25,31