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

摘要：

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

关键词：Petri网、π-网、密码协议、鉴别

所属期刊栏目：17

分类号：TP302.7(计算技术、计算机技术)

资助基金：国家自然科学基金60074011

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

页数：共4页

页码：78-81