关键词: 无线传感器网络，模型检验，SPINS协议，SPIN工具，Promela

Abstract: Model checking has been successfully applied to design and analyze wired network security protocol. Comparcel with the wired network,wircless sensor network(WSN) also has the strict requirement on its security protocol.The vulnerabilities of WSN exist in communication environment and network node; those are great challenges for designing and analyzing a security protocol in WSN. This paper proposed an appropriate method to model and analyze security protocol in the WSN. Based on the method of wired network security protocol, with the thorough consideration of sensor network environmental factors and feature of sensor nodes,a general model was established and analyzed by our method. "hhe paper took WSN SPINS security protocol as an example to model and analyze via SPIN tool. "hhrough verifying the authentication and confidentiality of SPINS, we found flaws in the SPINS protocol. I}he work demonstrates the feasibility of using model checking to model and analyze security protocol in WSN, and expands the usage of model checking.

Key words: Wireless sensor network, Model checking, SPINS protocol, SPIN, Promcla