Abstract:

We present a simplified Petri net model to analyse cryptographic protocols based on a kind of security protocol language proposed by Federico. Suffici ent 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 proto col in detail according to the secrecy of key, nounee and responders＇ identity. The analysis of cryptographic protocols is greatly simplified because o of the proposed Petri net model.

Key words: Petri net, event, secrecy property