In the protocol development process, the complex of protocol procedure and application scene usually leads to logical loopholes, which consequentially cause logical conflicts in the protocol. The security and reliability have a great influence on protocol development. Therefore,the analysis and verification on security has always been the focus and difficulty of protocol design.As a method of formal verification of security protocols, the CSP(Communicational Sequential Processess) method has become a hot research topic currently. The CSP method has been proved to be very useful to reduce the time of formal analysis and verification. In addition,With the extensively use of Wireless Sensor Networks(WSNs), the security problem of WSN has been increasingly prominent. In order to detect safety problems of the protocol in the design stage and ensure the correctness of requirement logic, the CSP method is proposed to apply to the analysis and verification of WSN security protocols.Based on the study of the security problems of WSN security protocols, a method based on CSP is proposed to describe the WSN security protocols. In the beginning, a description method extended on CSP language embedded in PAT is proposed to describe the behavior of WSN security protocols quickly. Then, according to the mobility of WSN node, a model extends Dolev-Yao model by adding the mobility of node is proposed to formal describe attacker model.After that, the LTL is proposed to describe the properties which WSN security protocols have to meet. Finally, the WSN security protocols and WBAN security protocols are modeled and verified using our method embedded in PAT, which reflects the usability and efficiency of our method. |