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

• 作者: 汪学明 翁立晨
• 来源期刊: 信息安全与技术
• 学科: 工学
• 关键词: 不可否认性 形式化分析 公平性 博弈 Mocha
• 年，卷（期）: 2011,（9）
• 所属期刊栏目: 技术探讨
• 页码范围: 21-25,31
• 分类号: TP31
• 字数: 5627字
• 语种: 中文
• DOI: 10.3969/j.issn.1674-9456.2011.09.005

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	汪学明	贵州大学计算机科学与信息学院	71	197	7.0	8.0
2	翁立晨	贵州大学计算机科学与信息学院	3	3	1.0	1.0