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

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

Analysis and Improvement of A Fair Multi-party Non-repudiation Protocol Based on ATL Logic

In order to overcome shortcomings of the traditional way of temporal logic to analyze a protocol as a closed system,a game-based formal analysis method of ATL logic is introduced.By this way a fair multi non-repudiation protocol is analyze and find that the protocol exist a flaw which does not meet the anti-collusion,and proposed two improved protocol.By use of the Mocha model checking tool with the combination of ATL formulas and Invariant Checking,two kinds of improved protocol are effective verificated and results show that the improved protocol can meet the non-repudiation and anti-collusion resistance.