We propose an approach for the formal modeling and analysis of security properties of cryptographic protocols.Our methodology is based on the idea of backward state analysis and the reachability analysis for Petri nets.By performing the state analysis

we can find out potential insecure states during the run of protocols and determine if these insecure states are reachable by using the state reachability analysis.An example shows that this approach is efficacious.