不可否认协议形式化分析的SVO逻辑方法

Formal analysis of non-repudiation protocols with SVO logic

使用SVO逻辑对Zhou-Gollmann的公平不可否认协议的一个改进协议进行了形式化分析.在分析该协议的过程中,分析了使用SVO逻辑分析不可否认协议时存在的一些问题,这是分析过程无法发现Zhou-Gollmann不可否认协议的原因.这些问题包括协议目标的确定,协议时限性的描述与分析,协议初始假设集的确定等.分析协议时,不仅需要证明协议的最终目标,还需要证明中间目标.通过对SVO逻辑的语法进行扩展,使其具有显式的时间描述能力,从而能够分析不可否认协议的时限性.

A new improvement of Zhou-Gollmann＇s fair non-repudiation protocol is analyzed with SVO logic. Some problems in the analysis of non-repudiation protocols using SVO logic, which are the causes why the flaw of Zhou-Gollmann＇s fair non-repudiation cannot be discovered, are discussed. These problems include determination of protocol goals, analysis of timeliness property of protocols and premise set establishment. In the analysis, both the final goals and the intermediary goals need to be proved. By extending the syntax of SVO logic, a time description method is added into it and, thus the timeliness of non-repudiation protocols can be analyzed.