CTCT-4级安全通信协议的形式化建模与验证

摘要

CTCS-4级列车运行控制系统是基于无线通信GSM-R传输信息的系统，而GSM-R系统是一种开放传输系统，它不能满足列控系统这种安全苛求系统的需求。主要根据GSM-R系统现有的安全威胁和应该采取的安全措施，引用一种改进的NSSK安全协议来保障车载设备与RBC间安全通信，并利用形式化建模语言CSP和模型检测工具FDR对其建模和验证。%The CTCS-4 is based on the wireless communication system GSM-R, while GSM-R is an open transmission system, it does not meet the demands of the train control system which is a safety critical system. In this paper, based on the existing security threats of the GSM-R and the safety measures should be adopted, an improved NSSK security protocol is used to protect the secure communications between the vehicle equipment and the RBC. Also modeling and verification the security protocol within the framework of CSP and its model-checking tool FDR.