基于Petri网的密码协议分析

Analysis of Cryptographic Protocols Based on Petri Nets

在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.