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

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

多方不可否认协议需要满足不可否认性、公平性和时限性三大安全目标,但是现有的对多方不可否认协议的形式化分析方法大多是对两方协议分析方法的简单扩展,单一方法不能完整覆盖所有的安全目标分析;同时,对单一安全目标的分析能力有限,分析结果不可靠。首先,综合比较现有的分析技术,选定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.