密码协议的π-网形式化描述和分析

摘要：

π-网是一类模块化的、具有代数演算功能的高级Petri网.通过引入项、buffer库所和解密变迁等建模元素,本文在π-网中建立了密钥管理和加密信息的传输机制,形成了密码协议的Petri网形式化模型,而且对于任意的一个密码协议,都可以将其模块化,本文还提出了密码协议的鉴别性和安全性的验证机制.通过对Needham-Schroeder协议的实例分析,对密码协议的密钥交换和鉴别性,以及协议存在的漏洞,进行了有效的形式化描述和分析。

关键词： Petri网 π-网 密码协议 鉴别性 密钥管理 形式化模型

作者: 曹木亮 吴智铭 杨根科

作者单位: 上海交通大学自动化系,上海,200030

会议类型: 国内会议

会议名称: 第十次全国Petri网学术年会暨形式化方法学术讨论会

会议地点: 江苏镇江

会议语种:中文

页码: 78-81

在线出版日期: 2005-10-01（万方平台首次上网日期，不代表论文的发表时间）