CTCS-4級安全通信協(xié)議的形式化建模和驗證.pdf

1、CTCS-4級是完全基于無線通信的列車運行控制系統(tǒng)，通過GSM-R接收指揮中心與RBC間的行車和授權(quán)信息。列車控制系統(tǒng)的安全運行與GSM-R網(wǎng)絡(luò)密切相關(guān)，CTCS-4級安全通信協(xié)議負(fù)責(zé)管理GSM-R無線網(wǎng)的注冊和安全連接，是實現(xiàn)車地間安全通信的重要環(huán)節(jié)。而GSM-R系統(tǒng)是一種開放傳輸系統(tǒng)，它不能滿足列控系統(tǒng)這種安全苛求系統(tǒng)的需求。因此對CTCS-4級安全協(xié)議的形式化研究變的非常重要。
　　在大的分布式環(huán)境中，安全協(xié)議所處的通信環(huán)境

2、是錯綜復(fù)雜的，也是非常不安全的。這就給攻擊者破壞安全協(xié)議提供了機會，它們可以對合法信息進行任意的截取、重放和篡改。安全協(xié)議最重要的安全性質(zhì)包括:認(rèn)證性、秘密性、完整性和不可否認(rèn)性。而判斷一個安全協(xié)議是不是安全可靠的，就是通過檢查安全協(xié)議的這些性質(zhì)是否被攻擊者破壞。目前存在多種協(xié)議模型，而CSP方法已被證明是一種表述安全目標(biāo)的行為和性質(zhì)的非常有效的框架。CSP框架能非常容易地包含很多不同結(jié)構(gòu)、機制和安全性質(zhì)，與一般的形式分析方法相比，它能

3、全面、深刻地檢測到安全協(xié)議中細(xì)微的漏洞。
　　GSM-R是由UIC國際鐵路聯(lián)盟支持開發(fā)的歐洲鐵路移動通信系統(tǒng)，它具有高可靠性、穩(wěn)定性和安全性的特點。本文首先分析了GSM-R的國內(nèi)外研究現(xiàn)狀和GSM-R的特點，發(fā)現(xiàn)GSM-R系統(tǒng)還存在一定的安全漏洞，其安全模型并不安全。應(yīng)該采取身份鑒別技術(shù)和利用加密安全碼鑒別身份的安全措施來保障車地間的安全通信。認(rèn)證協(xié)議是保障網(wǎng)絡(luò)安全的基礎(chǔ)，可以解決網(wǎng)絡(luò)中的實體身份認(rèn)證和密鑰分配問題，NSSK協(xié)議是

4、最早最經(jīng)典的認(rèn)證密碼協(xié)議，但是它存在重放攻擊和假基站攻擊等安全威脅。本文分析了消息重放攻擊及其對策和經(jīng)典NSSK協(xié)議的安全特性，提出了一種改進的加密認(rèn)證協(xié)議NSSK協(xié)議，并用形式化描述語言CSP和模型檢測工具FDR對NSSK協(xié)議進行建模和驗證。然后根據(jù)GSM-R系統(tǒng)現(xiàn)有的安全威脅、應(yīng)該采取的安全措施和車地端到端通信框架，引入改進的加密認(rèn)證協(xié)議NSSK協(xié)議，并用形式化描述語言CSP對通信框架進行建模和驗證，實驗結(jié)果表明改進的加密認(rèn)證協(xié)議N