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

徐 倩 林俊亭

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

0 引 言

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

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

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

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

1 RSSP-Ⅱ協議的MASL層功能概述

1.1 RSSP-Ⅱ協議的層次結構

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

圖1 RSSP-Ⅱ協議的層次結構

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

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

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

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

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

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

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

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

1.2 密鑰層級及其功能說明

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

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

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

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

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

1.3 對等實體認證流程

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

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

圖4 CPN模型示意圖

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

1.4 消息源驗證

消息源驗證用于保證傳送過程中信息的完整性,即消息未被篡改、重放或延遲等。主叫方進行消息源認證加密。輸入消息m、會話密鑰Ks、源地址SA和目的地址DA。依次生成消息“m”,“DA|m”,“l|DA|m”,其中:l為“DA|m”的長度,p為填充數據,p和原字符串構成“l|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網基本理論

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.2 頂層模型的描述

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

圖5 顏色集的聲明

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

圖6 頂層CPN模型

2.3 子模塊模型的描述

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

圖7 Entity1子模塊

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

圖8 Entity 2子模塊

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

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

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

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

(1) 領域無關屬性即模型的基本屬性。合理的CPN模型要求能夠合理解釋死標記,不發生死鎖、活鎖等現象。當到達某個標記時,若進入活鎖狀態,則無法退出,會進行產生無用信息的無限執行。死鎖現象是由于包含自鎖終端、死標記導致的模型意外中斷[16]。

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

3.1 CPN模型基本屬性驗證

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

圖9 統計信息的截圖

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

圖10 其他屬性信息的截圖

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

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

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

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

3.2 領域相關屬性的驗證

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

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

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

圖11 屬性1的驗證語句及結果圖

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

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

圖12 屬性2的驗證語句及結果圖

圖13 屬性3的驗證語句及結果圖

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

驗證屬性3語句同語句1。結果表明,所構造的模型滿足設計規范,能夠完成MASL的功能。

4 結 語

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

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