计算机工程与应用Issue(4)：81-85,5.DOI:10.3778/j.issn.1002-8331.1203-0784
CTCT-4级安全通信协议的形式化建模与验证
Formal modeling and verification of CTCS-4 security protocol
摘要
Abstract
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.关键词
GSM-R/安全协议/通讯顺序进程(CSP)/故障/偏差/精炼检测器(FDR)Key words
GSM-R/security protocol/Communicating Sequential Process(CSP)/Failures Divegences Refinement checker(FDR)分类
信息技术与安全科学引用本文复制引用
胡晓辉,陈慧丽,石广田,陈永..CTCT-4级安全通信协议的形式化建模与验证[J].计算机工程与应用,2014,(4):81-85,5.基金项目
国家自然科学基金（No.61163009）。 （）
