Abstract:

Nowadays, the increasing number of cyber security events in industry control system (ICS) are emerged. Railway Signalling System as a specific application of the industrial control system, including reliability and completeness, the transmission network security is also the stringent task to be focused on. This paper analysed the RSSP-II protocol as the security protocol for railway signalling system, the Communication Sequential Processes (CSP) method was introduced. CSP is one of the model checking method, this method using discrete event to describe the system, the process and its environment were described by algebraic operations in formal language. Each CSP process can be converted into equivalent state. The processes of the key service and peer entity authenticating are analysed through CSP. At last the model checking tool Casper-FDR was applied to verify the confidentiality and authenticity properties of the protocol. The result showed that the parameters are acceptable, and the reverse item number is 0, thus verified RSSP-II in key service and peer entity authenticating.

Key words: RSSP-II, communication protocol, security analysis, communicating sequential process method