RSSP-Ⅱ協(xié)議消息鑒定層的形式化描述及驗證

徐 倩 林俊亭

(蘭州交通大學自動化與電氣工程學院 甘肅 蘭州 730070)

0 引 言

針對數(shù)據(jù)傳輸中可能產(chǎn)生的重復、重排序、插入、延遲、刪除、損壞和偽裝等威脅,依據(jù)歐洲列車控制系統(tǒng)的Subset-037[1]、Subset-098[2]標準,中國鐵路總公司制定了RSSP協(xié)議,以規(guī)定信號安全設(shè)備進行安全信息交互的功能結(jié)構(gòu)和協(xié)議。其中,RSSP-Ⅰ適用于封閉式傳輸系統(tǒng),如我國客運專線的列控中心外圍系統(tǒng)接口間;RSSP-Ⅱ[3]適用于開放式傳輸系統(tǒng),如無線閉塞中心、臨時限速服務器的外圍系統(tǒng)接口間。RSSP-Ⅱ逐步向地鐵應用,如互聯(lián)互通基于通信列車控制系統(tǒng)(Communication-based Train Control, CBTC)的車載控制器與控制中心之間接口[4]。

協(xié)議工程是形式化的協(xié)議開發(fā)過程,能夠保證協(xié)議的設(shè)計開發(fā)質(zhì)量,包括協(xié)議形式化描述、形式化驗證、協(xié)議實現(xiàn)和協(xié)議一致性測試[5-6]。目前常用的協(xié)議形式化描述技術(shù)包括有限狀態(tài)機模型、Petri網(wǎng)模型以及通用認證協(xié)議規(guī)范語言(Common Authentication Protocol Specification Language, CAPSL)等。傳統(tǒng)方法是最終代碼實現(xiàn)后而通過調(diào)試來測試協(xié)議的可能漏洞,而形式化描述技術(shù)優(yōu)勢在于避免了自然語言描述協(xié)議存在的二義性問題,也避免了迭代測試固有的繁重工作量[7]。

文獻[9]依據(jù)安全層狀態(tài)轉(zhuǎn)移圖,建立賦時有色Petri網(wǎng)模型,再通過模型仿真驗證了安全連接建立時間符合EuroRadio安全通信協(xié)議規(guī)范要求。文獻[10]提出了China-Radio列控安全信息傳輸系統(tǒng),是在雙網(wǎng)冗余結(jié)構(gòu)的無線局域網(wǎng)基礎(chǔ)之上增加安全通信協(xié)議,也是依據(jù)狀態(tài)轉(zhuǎn)換圖建立CPN模型,利用模型檢驗查找了非安全狀態(tài)編號、路徑, 驗證功能安全性。文獻[11]分析了RSSP-Ⅱ安全應用中間子層序列號、時間戳機制,建立了相應CPN模型。這些文獻主要是分析所建立的安全鏈路的性能,而沒有對消息鑒定層進行驗證。文獻[12]提出用通信順序進程(Communicating Sequential Processes,CSP)對經(jīng)典認證密碼協(xié)議NSSK協(xié)議進行形式化描述和驗證。文獻[13]利用CSP對RSSP-Ⅱ的密鑰服務流程和對等實體認證進行了建模。CSP沒有程序結(jié)構(gòu),不具有可執(zhí)行性,需要再借助Haskell 作為函數(shù)式語言實現(xiàn)仿真,相對有圖形化建模、時態(tài)邏輯檢驗的CPN方法而言,驗證過程與結(jié)果較為抽象、繁瑣。

這些研究提供了利用CPN方法研究RSSP-Ⅱ的可行性、其他形式化方法在RSSP-Ⅱ的應用,針對RSSP-Ⅱ協(xié)議的消息鑒定層仍存在的研究不足。本文基于CPN理論及模型檢驗方法,在分析會話密鑰生成、對等實體認證、消息源認證等協(xié)議流程后建立了CPN模型,刻畫靜態(tài)結(jié)構(gòu)、動態(tài)行為。依次驗證模型本身的正確性、基本行為屬性、特定屬性,保障RSSP-Ⅱ協(xié)議開發(fā)過程的質(zhì)量,推廣RSSP-Ⅱ在CBTC的應用。

1 RSSP-Ⅱ協(xié)議的MASL層功能概述

1.1 RSSP-Ⅱ協(xié)議的層次結(jié)構(gòu)

如圖1所示,RSSP-Ⅱ協(xié)議位于通信層、應用層之間且由下到上包含的層次及其功能如下:

圖1 RSSP-Ⅱ協(xié)議的層次結(jié)構(gòu)

(1) 冗余適配管理層(Adaptation &redundancy management Layer, ALE) :提供數(shù)據(jù)多路傳輸?shù)墓芾?完成MASL 與傳輸控制協(xié)議之間的鏈路配置和必要時協(xié)議數(shù)據(jù)單元的重傳。

(2) 消息鑒定安全層:預防損壞、偽造和篡改等威脅。當前主要措施是為通信報文附加消息鑒別碼(Message Authentication Code, MAC) 和連接標識符(源和目的地標識符),實現(xiàn)消息的真實性、消息的完整性,以及訪問保護。MASL層為本文研究對象。

(3) 安全應用中間層(Safety Application Intermediate, SAI) :預防延遲、重排序、刪除、重復等威脅。當前措施主要是為通信數(shù)據(jù)包添加序列號實現(xiàn)序列錯誤防護,增加三重時間戳或者執(zhí)行周期,實現(xiàn)消息時效性防護。

通信進程可分為以下4個部分。本文研究的MASL層的協(xié)議流程在前兩個階段。

(1) 建立安全連接:傳輸安全地址信息給通信功能模塊;執(zhí)行對等實體認證進程。

(2) 安全數(shù)據(jù)傳輸:常規(guī)數(shù)據(jù)的消息源認證進程;傳輸層提供服務原語進程。

(3) 釋放安全連接:發(fā)送釋放連接的通知消息即可釋放整個安全連接。

(4) 錯誤處理:根據(jù)不同錯誤情況,通過安全報告標識報告等措施給下層安全用戶。

1.2 密鑰層級及其功能說明

如圖2所示,MASL 層應用了三級密鑰。

圖2 各密鑰功能說明示意圖

(1) 3級傳輸密鑰(Transmission Key, KTRANS):對密鑰管理中心(Key Management Center, KMC)和通信系統(tǒng)之間的密鑰管理通信進行保護。每個KMC與信號安全設(shè)備實體的關(guān)系需要一個KTRANS。KTRANS1、KTRANS2分別對KMC與信號安全設(shè)備之間所交互消息、KMAC的值進行認證和校驗。

(2) 2級驗證密鑰(Key of Message Authentication Code, KMAC): KMC事先分配KMAC給信號安全設(shè)備,使用相同KMAC設(shè)備之間才能建立安全連接。

(3) 1級會話密鑰(Key of Section MAC, KSMAC):驗證信號安全設(shè)備間通過安全連接傳輸?shù)臄?shù)據(jù),僅在本次安全連接期間有效。

1.3 對等實體認證流程

對等實體認證用于在建立安全連接過程中,確認通信實體的身份是否真實、合法、唯一。MASL層間傳輸?shù)臄?shù)據(jù)稱為安全-協(xié)議數(shù)據(jù)單元(Safety Protocol Data Unit, SaPDU),AU1 SaPDU、AU2 SaPDU、AU3 SaPDU分別表示對等認證協(xié)議中第一次、第二次、第三次消息。Text為各SaPDU規(guī)定格式及內(nèi)容,p為補足64位整數(shù)倍的填充數(shù)據(jù)。過程描述如圖3所示。

圖3 對等實體認證流程示意圖

圖4 CPN模型示意圖

設(shè)備1提出與設(shè)備2的建立安全連接通信請求,密鑰管理中心將分配給設(shè)備1、2驗證密鑰KSMAC。設(shè)備1生成一個隨機數(shù)R1,自身保存并作為AU1 SaPDU的一部分發(fā)往設(shè)備2。設(shè)備2收到后,生成隨機數(shù)R2,利用R1、R2和驗證密鑰K12通過3-DES加密算法,生成會話密鑰Ks,設(shè)備2生成AU2 SaPDU并發(fā)送給設(shè)備1。設(shè)備1收到AU2 SaPDU后,用R1、R2、K12生成會話密鑰Ks,并利用Ks檢驗AU2 SaPDU的正確性。若正確,則設(shè)備1用Ks加密 AU3 SaPDU并發(fā)送給設(shè)備2,最后設(shè)備2用Ks檢驗AU3 SaPDU。通過以上對等實體認證,設(shè)備1、設(shè)備2確認彼此擁有相同的會話密鑰Ks,并推斷有相同的KMAC,完成身份驗證。

1.4 消息源驗證

消息源驗證用于保證傳送過程中信息的完整性,即消息未被篡改、重放或延遲等。主叫方進行消息源認證加密。輸入消息m、會話密鑰Ks、源地址SA和目的地址DA。依次生成消息“m”,“DA|m”,“l(fā)|DA|m”,其中:l為“DA|m”的長度,p為填充數(shù)據(jù),p和原字符串構(gòu)成“l(fā)|DA|m|p”新消息字符串。由 CBC_MAC算法和會話密鑰Ks進行MAC計算:

MAC(m)=CBC_MAC(Ks,l|DA|m|p)

同理,被叫方進行驗證解密,生成MAC′(m)。如果MAC′(m)=MAC(m),且m方向標志正確,說明消息沒有被篡改,傳輸消息m。

2 消息鑒定層功能的CPN模型

2.1 有色Petri網(wǎng)基本理論

有色Petri網(wǎng)是一種離散事件建模語言,由庫所、變遷、弧構(gòu)成網(wǎng)狀模型,將Petri網(wǎng)理論與函數(shù)式編程語言CPN ML(Meta Language,元語言)結(jié)合,適用于構(gòu)建并發(fā)系統(tǒng)的模型及分析其屬性[14]。

(1) 庫所(Place) 表示系統(tǒng)可能的狀態(tài),主要屬性有庫所名、顏色集(數(shù)據(jù)類型)、初始標記等。初始標記(marking)代表了該庫所初始狀態(tài)時的令牌(token)值,是一個與庫所顏色集相同的令牌多重集。

(2) 變遷(Transition)表示引發(fā)系統(tǒng)狀態(tài)改變的事件,主要屬性有變遷名、守衛(wèi)函數(shù)、延時函數(shù)和代碼段。變遷的觸發(fā)受到守衛(wèi)函數(shù)和弧表達式的制約。

(3) 指向變遷的弧表明觸發(fā)的前提條件表示變遷的激發(fā)需要從庫所消耗相應的令牌(token);指向庫所的弧表明變遷觸發(fā)的結(jié)果表示變遷的激發(fā)需要轉(zhuǎn)移相應的令牌。

CPN-Tools嵌套的ASK-CTL工具包,是CTL的一種拓展,ASK-CTL語句由布爾運算符、原子命題、路徑量運算符、推導路徑量運算符等組成。

(1) 布爾運算量:TT,FF:布爾值常量,val TT: True; NOT、AND、OR分別同布爾操作符、∧、∨。

(2) 原子命題:節(jié)點函數(shù)NF,參數(shù)為一個字符串、一個取狀態(tài)空間節(jié)點返回布爾類型的函數(shù),用以搜索單一狀態(tài)或狀態(tài)空間全部子集,即NF:string*(Node->bool)->A?；『瘮?shù)AF,與NF類似,用以搜索單一變遷或變遷集合的全部子集;AF:string*(Arc->bool)->A。

(3) 路徑量運算符:所有路徑中, 至少有一條路徑中的所有狀態(tài)均為真,則操作符為真,即EXIST_UNTIL(A1,A2),A1→A2。

所有路徑中, 全部路徑中所有狀態(tài)均為真,則返回值為真;FORALL_UNTIL(A1,A2),A1→A2。

(4) 推導路徑運算量(以狀態(tài)公式為例)。

① 如果從當前狀態(tài)可以到A所處的狀態(tài)時,則POS返回值為真,POS(A)=EXIST_UNTIL(TT,A)。POS作為變遷公式時類似。

② 如果從當前狀態(tài)可以到達所有可達狀態(tài),A均為真,則INV返回值為真,INV(A)=NOT(POS(NOT(A)))。

③ 如果從當前狀態(tài),有限步數(shù)內(nèi)A最終為真,則EV返回值為真EV(A)=FORALL_UNTIL(TT,A)。

④ 如果存在一條路徑,其中任意狀態(tài)A符合,則ALONG返回值為真,路徑是無限或終止于死狀態(tài),ALONG(A)=NOT(EV(NOT(A)))。

2.2 頂層模型的描述

如圖5所示,按照RSSP-Ⅱ規(guī)范中各SaPDU的格式[3]設(shè)計了本文所需的顏色集。模型中變量的類型與其相連接的庫所需要保持一致,因此可根據(jù)顏色集進行變量的聲明,而不再單獨展開。

圖5 顏色集的聲明

根據(jù)第2節(jié)的分析,利用CPN-Tools建立分層CPN模型以刻畫MASL層功能的靜態(tài)結(jié)構(gòu)及動態(tài)行為。分層機制使得用戶可以按不同抽象層次建模。如圖6所示,以設(shè)備1與設(shè)備2通信過程為例,可代表無線閉塞中心與列車、列車自動監(jiān)控中心與列車的通信過程。以替代變遷表示交互對象,在下一級模型中替代變遷的輸入庫所將帶有IN套接字,輸出庫所將帶有Out套接字。KMC向Entity 1、Entity 2分配驗證密鑰,該過程由庫所KMAC list分別到變遷KMC1、KMC2表示。變遷上的守衛(wèi)函數(shù)只允許給定令牌通過。仿真后,庫所KMAC1、KMAC2儲存了各自KMAC,從而進入Entity 1、Entity 2子模塊。

圖6 頂層CPN模型

2.3 子模塊模型的描述

如圖7所示,當庫所KMAC1上有令牌,則激活變遷Peer_entity_authentication,將開始執(zhí)行實體對等認證流程進行身份驗證。庫所Request for Ks獲得令牌,表示系統(tǒng)轉(zhuǎn)變?yōu)楂@取會話密鑰Ks的狀態(tài)。由變遷Generate R1與庫所R1進行交互,獲取隨機數(shù)。以庫所R1的初始標記作為預先設(shè)置的隨機數(shù)。模型獲得R1,庫所Obtain R1顯示獲取到的隨機數(shù)。隨機數(shù)R1與Text1結(jié)合,執(zhí)行Combin_AU1變遷以生成AU1 SaPDU,顯示在庫所Obtain AU1 SaPDU上,格式為(text1,r1)。變遷Send AU1 SaPDU激活,向設(shè)備2發(fā)送AU1 SaPDU,進入Entity 2子模塊。

圖7 Entity1子模塊

如圖8所示,設(shè)備2獲取到AU1 SaPDU后,激活變遷Extract R1,其輸出弧的函數(shù)#2(text1,r1)用于提取隨機數(shù)R1。與該過程同時進行的是,庫所KMAC2上有令牌,同R1獲取方式產(chǎn)生了隨機數(shù)R2。綜上已獲取到KMAC2、R1、R2,將激活變遷Generate Ks2,生成會話密鑰Ks2。再通過Ks2對數(shù)據(jù)加密,加密后數(shù)據(jù)格式設(shè)為(Ks2,data1),將作為數(shù)據(jù)的MAC碼。結(jié)合MAC碼、R2值、Text2,激活變遷Combin_AU2,生成AU2 SaPDU。與生成AU1 SaPDU的過程相同,庫所Obtain AU2 SaPDU上有令牌,再激活變遷Send AU2 SaPDU,向設(shè)備1發(fā)送AU2 SaPDU,進入Entity1子模塊。

圖8 Entity 2子模塊

如圖7所示,提取了R2,獲取R1、KMAC2,激活變遷Generate Ks1,依次生成會話密鑰Ks1、包含Text4的AU3 SaPDU,再進入Entity 2模塊。如圖8所示,設(shè)備2對AU3 SaPDU檢驗,模型默認設(shè)置檢驗通過,庫所Peer_entity_ authentication_results上的令牌作為是否完成實體對等認證的標志。此后,設(shè)備2的MASL層向SAI層發(fā)送Sa-Connect.indication原語,SAI層處理后反饋Sa-Connect.request原語。變遷MASL Process表示MASL收到SAI層信息后進行處理,至庫所Start to generate AR,系統(tǒng)變?yōu)楫a(chǎn)生AR SaPDU的狀態(tài),結(jié)合Text6與已生成的MAC碼,至庫所Obtain AR,以令牌表示生成的AR SaPDU,發(fā)送給設(shè)備1。

進入Entity1模塊后,收到AR SaPDU表示安全通信鏈接已建立,開始發(fā)送應用數(shù)據(jù),包含在DT SaPDU,需要進行數(shù)據(jù)加密,該過程由變遷Message encryption表示,生成的DT SaPDU由庫所DT SaPDU上的令牌表示。令牌流入Entity 2模塊,需要進行消息解密,檢查MAC碼,最終消息源驗證結(jié)果顯示在庫所Message_source_authentication _results上。

3 MASL功能安全性的形式化驗證

通過CPN-Tools的仿真工具,可觀察到令牌在網(wǎng)絡(luò)中流動,獨立測試模型的不同部分及對模型進行全面測試。但形式化驗證認為仿真只能執(zhí)行有限步數(shù),適用于發(fā)現(xiàn)模型明顯的錯誤。而對于刻畫安全苛求系統(tǒng)的模型,無法證明錯誤不存在,因而需要具有嚴格數(shù)學語法、語義的模型檢驗等形式化驗證方法,詳盡地檢查所有可能的狀態(tài)[15]。系統(tǒng)屬性可分為兩類:

(1) 領(lǐng)域無關(guān)屬性即模型的基本屬性。合理的CPN模型要求能夠合理解釋死標記,不發(fā)生死鎖、活鎖等現(xiàn)象。當?shù)竭_某個標記時,若進入活鎖狀態(tài),則無法退出,會進行產(chǎn)生無用信息的無限執(zhí)行。死鎖現(xiàn)象是由于包含自鎖終端、死標記導致的模型意外中斷[16]。

(2) 領(lǐng)域相關(guān)屬性是結(jié)合模型特定領(lǐng)域知識,進行基于邏輯的模型檢驗,檢查特定的功能。CPN-Tools可通過ASK-CTL工具包進行查詢,根據(jù)判定結(jié)果返回值來確定協(xié)議的安全屬性是否實現(xiàn)[17]。

3.1 CPN模型基本屬性驗證

統(tǒng)計信息如圖9所示,包含狀態(tài)空間與強直通分量圖(Strongly connected component,Scc)的節(jié)點、弧的數(shù)量。節(jié)點表示可達標記,弧表示發(fā)生的綁定元素,節(jié)點與弧形成的交替序列稱為有向路徑。如果兩個狀態(tài)空間節(jié)點相互可達,則劃分到同一個Scc圖中。本文構(gòu)建模型的狀態(tài)空間及其Scc圖節(jié)點、弧數(shù)量一致,表明沒有自循環(huán),系統(tǒng)模型無活鎖。

圖9 統(tǒng)計信息的截圖

庫所包含的令牌數(shù)量都是有界的,因此本文不再對報告中有界性進行安全分析。其他屬性如圖10所示。

圖10 其他屬性信息的截圖

(1) 家態(tài)性描述模型是否包含家態(tài)標記(可以從任何可達標記到達的標記)。結(jié)果表明家態(tài)標記是220節(jié)點,是狀態(tài)空間的最后一個節(jié)點,是合理的。

(2) 活性提供死標記、死變遷和活變遷的信息。死標記是模型終止狀態(tài),此時沒有變遷能夠再被激活,模型至少需要一個死標記使得模型正常終止,如果多于1個則需要進行合理性分析。

所構(gòu)造的模型只有一個死標記,且死標記與家態(tài)標記均為第220個節(jié)點,是模型的最后一個節(jié)點,因此表明模型能夠正常終止,不存在意外中斷的情況,不包含死鎖。沒有死變遷實例(始終無法激活的變遷,通常由于模型設(shè)計缺陷而造成),表示所有的變遷都能被激活,模型不存在冗余設(shè)計缺陷?；钭冞w實例指從任何可達標記總能找到包含該變遷的發(fā)生序列。由于有死標記,而死標記不包含任何變遷,因此本文所構(gòu)造的模型不存在活變遷是合理的。

(3) 公平性指出公平變遷,該變遷是指在所有無限發(fā)生序列中無限地發(fā)生。由于本文所構(gòu)造的模型不是循環(huán)執(zhí)行,因此不存在無限發(fā)生序列。

3.2 領(lǐng)域相關(guān)屬性的驗證

從RSSP-Ⅱ規(guī)范中提取功能屬性,可分為3類屬性期望狀態(tài)最終會達到、可能會發(fā)生一些狀態(tài)、不期望的狀態(tài)不會發(fā)生。以下3個屬性作為例證。

屬性1設(shè)備1、設(shè)備2總會獲得來自KMC的KMAC1、KMAC2。

驗證屬性1的語句用到了推導路徑運算量EV,所有路徑的狀態(tài)都為真時,則返回值為真;原子命題中的 節(jié)點函數(shù)NF。由圖11可知,屬性1驗證結(jié)果正確。

圖11 屬性1的驗證語句及結(jié)果圖

屬性2Ks1與Ks2的生成有先后,可以驗證Ks1、Ks2并非同時產(chǎn)生。

如圖12所示,驗證屬性2的語句中由于隨機數(shù)的不確定使得庫所Ks1、Ks2的令牌無法確定,因此用[]表示。用到了INV(M)。驗證結(jié)果false表示上式不能成立,這與Ks1與Ks2不能同時生成則不滿足INV條件的事實一致。

圖12 屬性2的驗證語句及結(jié)果圖

圖13 屬性3的驗證語句及結(jié)果圖

屬性3驗證MASL功能時表現(xiàn)為能夠完成對等實體認證、消息源驗證。

驗證屬性3語句同語句1。結(jié)果表明,所構(gòu)造的模型滿足設(shè)計規(guī)范,能夠完成MASL的功能。

4 結(jié) 語

(1) 形式化描述過程:有色Petri網(wǎng)能夠描述離散事件系統(tǒng)的靜態(tài)結(jié)構(gòu)、動態(tài)行為?；趨f(xié)議流程分析,本文按照自上而下的原則建模,所建立的CPN模型刻畫了密鑰服務、對等實體認證、消息源認證的流程。在建模過程中,借助CPN-Tools可觀察仿真結(jié)果,本文模型已通過了語法檢測,沒有建模錯誤。

(2) 模型檢驗過程:模型檢驗是常用的形式化驗證手段,通過遍歷檢查所有狀態(tài)空間來自動化地驗證該模型是否滿足給定的屬性。本文先從狀態(tài)空間報告中獲取CPN模型的基本屬性,證明了反映設(shè)計規(guī)范的模型并沒有死鎖、活鎖、冗余等設(shè)計缺陷。從RSSP-Ⅱ規(guī)范中獲取MASL具體功能屬性,編寫ASK-CTL查詢語句,進行驗證。本文以三個屬性的ASK-CTL語句為例,證明邏輯推理滿足預期,滿足MASL加密性、認證性的功能安全性的需求,下一步工作為根據(jù)CPN模型生成代碼框架,基于模型的形式化開發(fā)過程能夠保障RSSP-Ⅱ協(xié)議的開發(fā)質(zhì)量。