Quantum key distribution protocols are already proved to be unconditionally secure, however, the complexity of the existed proving versions makes it a difficult way to further spread into the security proving of other quantum cryptography protocols. To address this problem, a new method of security analysis of QKD protocols is introduced. Based on the equivalence attack model of QKD protocols which is refered to Biham's proving, the protocol is divided into two parts: the body and the attack, then a Petri-net model of BB84 is obtained, and a security analysis is followed. The formal annlysis of QKD protocols bωed on Petri-net can improve the efficiency of security analysis. Because of its simpleness and unification, it becomes more easy to apply this method to other quantum cryptography protocols