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

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.