不可否认协议的Petri网建模与分析

Modeling and Analysis of Non-Repudiation Protocols by Using Petri Nets

Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用.作为一种特殊的安全协议,不可否认协议虽然已得到了多种形式化方法的分析,但还没有人使用Petri网来分析它们.以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其他形式化方法无法描述的协议性质.使用该方法分析Zhou和Gollmann于1996年提出的一个公平不可否认协议,可以发现该协议的一个许多其他形式化方法不能发现的已知缺陷.

Since Petri nets is a mature and widely-used tool for the description and analysis of concurrent actions, it has been widely used in many fields in computer science, including security protocols. As a special kind of security protocol, non-repudiation protocols have been analyzed with many formal methods in recent years. However, there is no published research on using Petri nets to analyze non-repudiation protocols. For the advantage of Petri nets, it is attractive to adopt it to analyze non-repudiation protocols. Techniques used in normal security protocols, however, are not all suitable for non-repudiation protocols. Therefore, a Petri nets based modeling and analysis approach is given, which can describe and analyze some non-repudiation properties that can not be described by some other methods. A fair non-repudiation protocol proposed by J. Zhou and D. Gollmann in 1996 is modeled and analyzed on CPN tools using this method and, a known flaw of the protocol that has not been discovered by many other formal methods is discovered.