计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2005年
9期
1571-1577
,共7页
不可否认%有色Petri网%建模%形式化分析
不可否認%有色Petri網%建模%形式化分析
불가부인%유색Petri망%건모%형식화분석
Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用.作为一种特殊的安全协议,不可否认协议虽然已得到了多种形式化方法的分析,但还没有人使用Petri网来分析它们.以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其他形式化方法无法描述的协议性质.使用该方法分析Zhou和Gollmann于1996年提出的一个公平不可否认协议,可以发现该协议的一个许多其他形式化方法不能发现的已知缺陷.
Petri網是一種描述及分析併髮行為的工具,在安全協議的形式化分析中得到瞭廣汎的應用.作為一種特殊的安全協議,不可否認協議雖然已得到瞭多種形式化方法的分析,但還沒有人使用Petri網來分析它們.以一般安全協議的Petri網分析方法為基礎,提齣瞭使用Petri網分析不可否認協議的建模及分析方法,該方法可以描述併分析一些其他形式化方法無法描述的協議性質.使用該方法分析Zhou和Gollmann于1996年提齣的一箇公平不可否認協議,可以髮現該協議的一箇許多其他形式化方法不能髮現的已知缺陷.
Petri망시일충묘술급분석병발행위적공구,재안전협의적형식화분석중득도료엄범적응용.작위일충특수적안전협의,불가부인협의수연이득도료다충형식화방법적분석,단환몰유인사용Petri망래분석타문.이일반안전협의적Petri망분석방법위기출,제출료사용Petri망분석불가부인협의적건모급분석방법,해방법가이묘술병분석일사기타형식화방법무법묘술적협의성질.사용해방법분석Zhou화Gollmann우1996년제출적일개공평불가부인협의,가이발현해협의적일개허다기타형식화방법불능발현적이지결함.
