Security protocol is the key to ensure network security, in the existing technical conditions, there are many methods to analyze the security of protocol, but the attacker modeling method is not efficient, resulting in lower detection and analysis efficiency of protocols. Formal method is a means to verify protocol, which can effectively analyze the loopholes in the design of verification protocol. As one of the formalized methods, model detection has the characteristics of simplicity, efficient and high degree of automation, the model detector SPIN has a powerful detection capability. This paper uses SPIN to study security protocol, proposes a more efficient method to verify the security protocol of attacker model, firstly, analyze the attacker's behavior, acquire the attacker's initial knowledge base, update the attacker's knowledge base according to the decomposition rule and the synthetic rule; secondly, formalize the Promela semantic model of each honest subject and the attacker; finally, the model checker SPIN is used for verification. The experimental results show that the proposed method can reduce the complexity of the model, greatly reduce the number of state of the model, effectively avoid the state space explosion, and improves the verification efficiency.
