不可否认协议形式化分析的Petri网方法
Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用,但目前还没有人使用Petri网来分析不可否认协议.本文以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其它形式化方法无法描述的协议性质.使用该方法分析J.Zhou和D.Gollmann的公平不可否认协议发现了它议的一个许多其它形式化方法不能发现的已知缺陷.
不可否认 有色Petri网建模 形式化分析 安全协议
黎波涛 罗军舟
东南大学计算机科学与工程系,南京,210096
国内会议
江苏镇江
中文
88-92
2005-10-01（万方平台首次上网日期，不代表论文的发表时间）