基于Petri网的密码协议分析  

Analysis of Cryptographic Protocols Based on Petri Nets

作　　者：王剑[1] 唐朝京[1] 张权[1] 张森强[1] 

机构地区：[1]国防科技大学电子科学与工程学院,湖南长沙410073

出　　处：《计算机工程与科学》2006年第2期24-27,共4页Computer Engineering & Science

基　　金：国家863计划资助项目(863-307-7-5)

摘　　要：在Federico提出的一种密码协议进程语言的基础上,建立了便于进行密码协议分析的简化Petri网模型,给出了协议满足秘密性的充要条件,并以NS公钥协议为例,用Petri网模型,结合归纳方法和串空间分析方法从密钥、新鲜数和协议主体三个方面的秘密性分析了该协议的秘密性,简化了协议秘密性的分析。We present a simplified Petri net model to analyse cryptographic protocols based on a kind of security protocol language proposed by Federico. Sufficient and necessary conditions to achieve the security of cryptographic protocols are given in the paper. With the proposed Petri net model, we prove the security of the NS authentication protocol which incorporates the inductive method and the strand space model, and describe the security of the NS protocol in detail according to the secrecy of key, nounee and responders＇ identity. The analysis of cryptographic protocols is greatly simplified because of the proposed Petri net model.

关 键 词：PETRI网 事件 秘密性 

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