CTCS-4级是完全基于无线通信的列车运行控制系统,通过GSM-R接收指挥中心与RBC间的行车和授权信息。列车控制系统的安全运行与GSM-R网络密切相关,CTCS-4级安全通信协议负责管理GSM-R无线网的注册和安全连接,是实现车地间安全通信的重要环节。而GSM-R系统是一种开放传输系统,它不能满足列控系统这种安全苛求系统的需求。因此对CTCS-4级安全协议的形式化研究变的非常重要。在大的分布式环境中,安全协议所处的通信环境是错综复杂的,也是非常不安全的。这就给攻击者破坏安全协议提供了机会,它们可以对合法信息进行任意的截取、重放和篡改。安全协议最重要的安全性质包括：认证性、秘密性、完整性和不可否认性。而判断一个安全协议是不是安全可靠的,就是通过检查安全协议的这些性质是否被攻击者破坏。目前存在多种协议模型,而CSP方法已被证明是一种表述安全目标的行为和性质的非常有效的框架。CSP框架能非常容易地包含很多不同结构、机制和安全性质,与一般的形式分析方法相比,它能全面、深刻地检测到安全协议中细微的漏洞。GSM-R是由UIC国际铁路联盟支持开发的欧洲铁路移动通信系统,它具有高可靠性、稳定性和安全性的特点。本文首先分析了GSM-R的国内外研究现状和GSM-R的特点,发现GSM-R系统还存在一定的安全漏洞,其安全模型并不安全。应该采取身份鉴别技术和利用加密安全码鉴别身份的安全措施来保障车地间的安全通信。认证协议是保障网络安全的基础,可以解决网络中的实体身份认证和密钥分配问题,NSSK协议是最早最经典的认证密码协议,但是它存在重放攻击和假基站攻击等安全威胁。本文分析了消息重放攻击及其对策和经典NSSK协议的安全特性,提出了一种改进的加密认证协议NSSK协议,并用形式化描述语言CSP和模型检测工具FDR对NSSK协议进行建模和验证。然后根据GSM-R系统现有的安全威胁、应该采取的安全措施和车地端到端通信框架,引入改进的加密认证协议NSSK协议,并用形式化描述语言CSP对通信框架进行建模和验证,实验结果表明改进的加密认证协议NSSK实现了车地端到端认证,避免了重放攻击和假基站攻击。