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

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

作　　者：黎波涛[1] 罗军舟[1] 

机构地区：[1]东南大学计算机科学与工程系,南京210096

出　　处：《计算机研究与发展》2005年第9期1571-1577,共7页Journal of Computer Research and Development

基　　金：江苏省"网络与信息安全"重点实验室基金项目(BM2003201);江苏省高技术研究基金项目(BG2004036)~~

摘　　要：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.

关 键 词：不可否认 有色PETRI网 建模 形式化分析 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]