Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra
Ailun Liu, Huibiao Zhu, Yuan Fei, Shuangqing Xiang, Gang Lu, Wanling Xie · 2017
The security protocol is proposed as a security solution for end-to-end communication between smart grid applications in the EU FP7 project C-DAX. Since the importance and widespread use of the security protocol, it is of great significance to formally analyze and verify relevant security properties of this security protocol. In this paper, we apply Communicating Sequential Processes (CSP) to model the security protocol. Further, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for the specification and relevant secure properties, e.g. reachability of the fake goal. Our modeling and verification show that a risk may exist in the security protocol.