Abstract: Proposed in this paper is an approach for the formal modeling and analysis of security properties of cryptographic protocols The methodology is based on the idea of backward state analysis and the reachability analysis for Petri nets By performing the state analysis, potential insecure states can be found and it can be determined whether these insecure states are reachable An example shows that this approach is efficacious