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

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

作　　者：汪学明[1] 翁立晨[1] 

机构地区：[1]贵州大学计算机科学与信息学院,贵州贵阳550025

出　　处：《信息安全与技术》2011年第9期21-25,31,共6页

基　　金：国家自然科学基金项目(2009)60963023号;贵州大学引进人才科研基金项目(2008)005号

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

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

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]