Modeling and Verifying Intelligent Unit Transmission Protocol Using CSP Model Checker PAT

Intelligent unit transmission protocol is the link of communications among the intelligent units of smart power automation systems. The security of intelligent unit transmission protocol is the key to guarantee that the smart power automation systems achieving high speed, reliable and secure communication. Therefore, it is critical important for security analysis of intelligent unit transmission protocol. This paper introduced the characteristics of typical intelligent unit transmission protocol - manufacturing message specification(MMS). Proposed a method for security analysis of intelligent unit transmission protocols in the field of smart grid, that is modeling the protocol with communicating sequential processes(CSP), specifying the security properties with linear temporal logic(LTL) and using PAT, a CSP model checker, to verify whether the model caters for the secure properties. Taking MMS for example, we modeling and verifying its secrecy, authentication and deadlockfree ness in PAT. The results show the effectiveness, which provided support for further security analysis and enhancement of intelligence unit transmission protocol.