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

The description and analysis for cryptographic protocols based on the π-nets

作　　者：曹木亮[1] 吴智铭[1] 杨根科[1] 

机构地区：[1]上海交通大学自动化系,上海,200030 上海交通大学自动化系,上海,200030 上海交通大学自动化系,上海,200030

出　　处：《系统仿真学报》2005年第z1期78-81,共4页Journal of System Simulation

基　　金：国家自然科学基金 (60074011)

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

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

分 类 号：TP302.7[自动化与计算机技术—计算机系统结构]