一种可靠的多方不可否认协议的逻辑分析方法  

Reliable Logic Analysis Method of Multi-party Non-repudiation Protocol

作　　者：苑博奥 刘军 YUAN Bo-ao;LIU Jun(College of Command Information Systems,Army Engineering University of PLA,Nanjing 210007,China)

机构地区：[1]陆军工程大学指挥信息系统学院,南京210007

出　　处：《计算机科学》2018年第7期143-149,共7页Computer Science

摘　　要：多方不可否认协议需要满足不可否认性、公平性和时限性三大安全目标,但是现有的对多方不可否认协议的形式化分析方法大多是对两方协议分析方法的简单扩展,单一方法不能完整覆盖所有的安全目标分析;同时,对单一安全目标的分析能力有限,分析结果不可靠。首先,综合比较现有的分析技术,选定SVO逻辑进行扩展,显式引入时间因素,给出对应的语法定义和时间演算公理。然后,对改进逻辑的语义模型进行介绍,并证明了逻辑系统的可靠性,使得改进后的逻辑系统支持对多方不可否认协议三大安全目标的分析。最后,选取一个典型的多方不可否认协议,分别对其时限性和公平性进行分析,发现了其中存在的时限性和公平性缺陷,并给出了对应的攻击方法。其中,公平性缺陷是首次被发现。Multi-party non-repudiation protocol needs to meet three main security goals of non-repudiation,fairness and timeliness,but the existing formal analysis methods for multi-party non-repudiation proctocol are just simple extensions of those applied to two-party protocols.At the same time,each method can not cover all three security goals and has limited ability to analyze one goal with result unreliable.In this paper,the existing analysis methods were compared and the SVO logic was chosen for further study.Time factor was introduced in the logic system with relevant syntax definition and deduction axioms brought in explicitly.Then,the semantic model of the improved logic was stated and the soundness of logic system was proved,causing that the improved logic system can support the analysis of all three security goals of multi-party non-repudiation protocol.In the end,a typical multi-party non-repudiation protocol was analyzed with the improved logic and the defects of timeliness and fairness were found with corresponding attacks stated.Among the defects,the defect of fairness was discovered for the first time.

关 键 词：多方不可否认协议 SVO逻辑 时限性 公平性 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]