10.3969/j.issn.1674-9456.2011.09.005
基于ATL逻辑的公平多方不可否认协议的分析与改进
为了克服传统时序逻辑以封闭系统方式分析协议的缺点,引入一种基于博弈的ATL逻辑形式化分析方法。利用该方法分析了一个公平的多方不可否认协议,发现该协议存在不满足抗合谋性的缺陷,并提出了两种改进方案,使用Mocha模型检测工具以ATL公式和Invariant Checking相结合的方式对两种改进方案进行有效验证,结果表明改进后的协议满足不可否认性和抗合谋性。
不可否认性、形式化分析、公平性、博弈、Mocha
TP31(计算技术、计算机技术)
国家自然科学基金项目200960963023号;贵州大学引进人才科研基金项目2008005号
2012-04-21(万方平台首次上网日期,不代表论文的发表时间)
共6页
21-25,31