基于著色Petri網的鐵路時間同步協議建模及安全性分析

蘭麗，張友鵬

?

基于著色Petri網的鐵路時間同步協議建模及安全性分析

蘭麗1, 3，張友鵬2

(1. 蘭州交通大學 電子與信息工程學院，甘肅 蘭州 730070； 2. 蘭州交通大學 自動化與電氣工程學院，甘肅 蘭州 730070；3. 蘭州交通大學 光電技術與智能控制教育部重點實驗室，甘肅 蘭州 730070)

針對Autokey模型的鐵路時間同步協議安全性問題，提出利用著色Petri網對協議進行安全性分析。剖析Autokey模型的鐵路時間同步協議序列及其執行流程；重點針對其認證階段，分別構建正常認證和加入中間人入侵的著色Petri網模型，分析中間人入侵時協議認證過程的不安全狀態，建立模型狀態方程；應用逆向狀態分析法對鐵路時間同步協議認證過程的安全性進行分析，得到中間人在認證階段攻擊協議的實施序列。研究結果表明：基于Autokey模型的鐵路時間同步協議的認證過程是不安全的。

鐵路時間同步協議；中間人；著色Petri網；安全性分析

統一、精確的時間是保證鐵路正常、安全運營的基礎。隨著我國鐵路大規模提速改造，對鐵路運輸安全和運輸服務提出了更高的要求。鐵路時間同步網是鐵路運輸指揮、作業生產、經營服務及管理等業務的正常運轉和安全的重要技術支撐網絡之一，其作用就是為鐵路各業務系統提供統一的定時基準信號。目前，鐵路時間同步網采用NTP v4協議作為其時間同步關鍵協議，NTP v4采用基于Autokey模型的協議序列來確保時間同步數據交互時的安全性。但是，近年來針對NTP的網絡攻擊越加頻繁，已造成數以億計的經濟損失[1]。刁造翔 等[2]提出通過ARP欺騙的方法可以偽造服務器，使客戶端與錯誤的服務器進行時間同步，以達到攻擊者任意操控客戶端時間的目的。Malhotra[3]詳細分析了利用NTP的速率限制機制KoD(Kiss-Or-Death)進行DOS攻擊。朱越凡等[4]提出利用NTP協議構建隱蔽通道，攜帶秘密信息可穿透網絡監測設備。基于Autokey模型的協議序列主要分為2個階段：認證和對時。對服務器和客戶端合法準確進行認證是正確對時的基礎。由于NTP協議基于UDP，不提供安全性檢查，其不可靠的無連接服務極易被攻擊者利用。攻擊者若利用協議自身漏洞侵入鐵路時間同步網絡，后果不堪設想。因此，基于Autokey模型的NTP協議序列能否提供安全的認證機制以保證鐵路各級時間節點準確安全的對時亟待研究。著色Petri網(Colored Petri Net，CPN)是從經典的Petri網發展來的一種高級網系統，其將經典Petri網系統中的托肯賦予一定的顏色以代表不同的實物，大大減少了庫所和變遷的數目[5]。本文將著色Petri網引入鐵路時間同步協議安全性分析，采用逆向狀態分析法對協議不安全狀態進行可達性分析，最終確定到達不安全狀態的攻擊路徑，從而實現對鐵路時間同步協議安全性的分析。

1 基于Autokey模型的NTP協議序列

1.1 協議描述

根據RFC5906，Autokey報文格式如圖1所示，用于生成MAC的對稱摘要秘鑰是通過Autokey協議模型來實現其協商過程，對稱摘要秘鑰的協商在NTP數據包的擴展域中完成。

圖1 基于Autokey模型的NTP報文格式

基于Autokey模型的NTP協議認證過程[6?9]，如圖2所示，具體步驟如下：

1) 初始關聯。客戶端和服務器端交換對稱摘要密鑰主機名。Autokey模型支持私有證書(Private Certificate，PC)和可信證書 (Trusted Certificate，TC)，默認使用TC。

2) 交換證書。客戶端發送證書請求報文，服務器回復報文中包含證書，客戶端獲取服務器端的公鑰PKB。

3) 客戶端向服務器請求cookie。客戶端利用從服務器獲得的cookie，驗證服務器端身份及數據包的完整性。

圖2 基于Autokey模型的NTP協議認證過程

4) 客戶端請求時間同步。如圖3所示，客戶端發送時間同步請求報文syns_Request(記錄時間1)，服務器端接收到時間請求報文后，構造時間同步回復報文Syns_Response(記錄時間1，2和3)，客戶端收到回復報文(記錄時間4)，計算NTP消息的周期時延delay=1+2=(4?1)?(3?2)和時間偏差=((2?1)+(4?3))/2，最后依據于delay和調節本地時間。其中，1是客戶端發送時間同步請求報文的時間，2是服務器端接收到時間同步請求報文的時間，3是服務器發出時間同步回復報文的時間，4是客戶端接收到時間同步回復報文的時間。

圖3 NTP協議時間同步過程

在以上4個步驟中，步驟3的作用是利用從步驟2中獲取的服務器端公鑰PKB驗證服務器的合法性和數據包的完整性，步驟4利用從步驟3獲取的cookie驗證時間請求報文的完整性，因此這2步是基于Autokey模型的NTP序列認證過程的核心步驟，因此，本文主要針對這2個核心步驟進行分析。這2個步驟詳細執行過程分析如下：

步驟1 客戶端發送包含有客戶端公鑰PKA的cookie請求報文cookie_Request。

步驟2 服務器接收到cookie_Request報文后，首先按照式(1)計算cookie，其中ClientIP為客戶端IP地址，ServerIP為服務器IP地址，Server Seed是一個32位隨機值。然后利用客戶端傳過來的公鑰PKA將計算出的cookie加密得到{cookie}PKA，將之放在擴展域中，用服務器私鑰SKB對cookie加密得到簽名{cookie}SKB，服務器將{cookie}PKA和{cookie}SKB作為cookie_Response發送給客 戶端。

步驟3 客戶端接收到服務器端發送來的cookie_Response報文，先利用在證書交換階段獲取的服務器公鑰PKB驗證服務器簽名，再使用自己的私鑰SKA解密得到cookie，這樣客戶端就從服務器端獲取了秘密值cookie。在這個過程中客戶端雖然驗證了服務器的可靠性，但服務器卻并未驗證客戶端的可靠性。

步驟4 客戶端A發送時間請求報文syns_ Request，報文中包含keyID、MACasyn及時間同步請求報文NTP packet。客戶端利用從服務器端獲取的cookie和自行選擇的keyID，利用式(2)一起計算出對稱摘要密鑰，即Autokey。再利用式(3)將計算出的Autokey與NTP packet一起計算得出MACasyn。

其中：src_ip為源IP地址；dst_ip為目的IP地址；keyID為密鑰ID。

1.2 協議漏洞分析

在Autokey模型中，cookie是服務器識別客戶端的唯一標識。在此過程中，服務器利用式(1)計算出cookie，為保證cookie的完整性和真實性，采用客戶端公鑰對cookie進行加密，并且用服務器私鑰進行簽名。盡管采取簽名措施來驗證服務器的真實性，但是，服務器卻并未驗證客戶端的真實性，因此，攻擊者可以利用這一點通過偽造IP冒充合法的客戶端，使用自己的公鑰加密密鑰給服務器端發送一個cookie請求，服務器端收到請求后計算出cookie，同時利用攻擊者的公鑰加密，服務器私鑰簽名，將加密后的cookie發送給客戶端，攻擊者截獲服務器發送給客戶端的cookie應答報文，利用攻擊者自己的私鑰解密，獲取了發送給客戶端的cookie。這使得客戶端和服務器身份認證的關鍵信息被攻擊者獲取，攻擊者由此可以偽裝成合法的客戶端和服務器作為“中間人”，通過在一級時間節點和二級時間節點的通信路徑中插入自己的主機，使“中間人”成為一、二級時間節點相互通信的一個中繼，進而實施“中間人”攻擊。需要時間同步的客戶端將“中間人”誤以為是合法服務器，導致客戶端接受被中間人操控的時間信息，從而使客戶端與錯誤時間信息同步。

本文的研究對象為基于Autokey模型的鐵路時間同步協議，由于其時序要求嚴格，報文交互機制較為復雜，如果根據攻擊者的能力正向分析協議的不安全狀態，可能的情形非常多。利用著色Petri網對其建模進行逆向分析，能有效克服傳統的可達樹等方法，在可達性分析方面的動態分析能力不足、狀態空間爆炸的缺陷。

2 基于著色Petri網的協議不安全狀態分析

2.1 相關概念

一個著色Petri網被定義為一個6元組：

2.2 基于CPN的鐵路時間同步協議不安全狀態分析方法

基于CPN的鐵路時間同步協議不安全狀態分析方法具體步驟如下：

1) 根據鐵路時間同步協議執行流程，建立其正常工作過程的著色網模型；

2) 確定中間人攻擊者可能修改的變量；

3) 構建中間人攻擊下的鐵路時間同步協議著色網模型；

4) 根據協議攻擊模型確定協議初始狀態0和不安全的終止狀態M及關聯矩陣T；

5) 建立模型狀態方程：

其中：M為不安全終止狀態；0為初始狀態，為著色網模型的關聯矩陣；為該狀態方程的一個非負整數解。

6) 根據非齊次線性方程組解得判定定理，判斷方程(5)是否有解。若系數矩陣T，與其增廣矩陣(T,M)秩相同，則有解；若不相同，則無解。

7) 解狀態方程(5)，若有解，則給出變遷發生序列即攻擊路徑，說明該不安全狀態可達；否則，說明該不安全狀態不可達。

3 鐵路時間同步協議CPN模型

3.1 NTP協議正常認證過程的CPN模型

鐵路時間同步網共分3級，1級時間節點位于鐵路總公司調度中心，2級時間節點位于各鐵路局，3級時間節點位于各站、段、所[10]。節點之間采用NTP協議的主從模式傳輸時間同步信息，協議規定，下一級時間必須從上一級獲取，根據NTP協議認證執行流程，建立鐵路時間同步網1，2級時間同步節點在正常認證過程的CPN模型，如圖4 所示。

圖4中，2級時間節點為客戶端，一級時間節點為服務器端，各節點的庫所中均含有各自相關的顏色托肯，在圖中均標注于各庫所之上，以下為了敘述方便，使用代表2級時間節點，代表1級時間節點。

各庫所代表的顏色集={1,2,…,9,10}，其元素具體為：

1=利用PKA生成的cookie_Request消息，2=cookie，3={cookie}PKA，4=D{{cookie}PKA, {cookie}SKB}，5=D{keyID,MACasyn,NTP報文}，6= D{MACr_asyn,NTP回復報文}，7=AC(通過)，8=RE (拒絕)，9={cookie}SKB，10=keyID。其中D{?}代表將括號中的數據元素進行組包。

圖4 基于Autokey模型的NTP協議正常認證過程CPN模型

3.2 NTP協議認證過程收到中間人攻擊的CPN 模型

NTP協議認證過程受到中間人攻擊的具體步驟如下：

步驟1 客戶端向中間人發送包含有客戶端公鑰PKA的cookie請求報文cookie_Request，中間人截獲此報文，存儲客戶端公鑰PKA。同時，中間人偽裝成客戶端，用自己的公鑰PKM給服務器發送一個cookie請求報文cookie_Request′。

步驟2 服務器接收到中間人發來的cookie請求報文cookie_Request′后，首先按式(1)計算cookie。然后按照中間人發送來的公鑰PKM，并且利用服務器私鑰SKB對cookie加密得到簽名{cookie}SKB，服務器將{cookie}PKM和{cookie}SKB構成的cookie應答報文cookie_Response′一并發送給中間人。

步驟3 中間人截獲cookie_Response′，利用中間人自己的私鑰SKM解密，獲得此次同步請求客戶端的cookie。中間人利用在步驟1獲得的客戶端公鑰PKA加密cookie，得到{cookie}PKA和截獲的cookie應答報文cookie_Response′中的{cookie}SKB重組成cookie_Response一并發送給客戶端。

步驟4 客戶端接收到中間人發送來的cookie_ Response，利用在證書交換階段獲取的服務器公鑰PKA驗證服務器簽名，再使用客戶端自己的私鑰SKA解密得到cookie，這樣客戶端也得到cookie。

步驟5 客戶端發送時間請求報文syns_ Request，報文中包含keyID，時間同步請求報文NTP packet和MACasyn。中間人截獲報文并轉發給服務器，同時保存keyID。

步驟7 中間人截獲syns_Response，利用步驟5中截獲的keyID和步驟3中獲得的cookie，按照式(2)重新計算Autokey，中間人篡改時間回復報文中NTP packet′的時間信息，將篡改時間信息后的NTP packetM′與Autokey計算得到MACr_asyn_c，將MACr_asyn_c和NTP packetM′重新組包成syns_ Response′發送給客戶端。

步驟8 客戶端接收到syns_ Responsei′，首先按照式(2)計算Autokey，再利用式(3)計算MACr_asyn_c′，比較MACr_asyn_c′和MACr_asyn_c一致，客戶端認為與中間人擁有共享的cookie，并且用于應答MAC的密鑰ID與本次請求報文中的密鑰ID一致，于是客戶端按照篡改的NTP報文中的時間校正本地時間，中間人達到任意操縱客戶端時間的目的。

根據上述攻擊步驟，建立1和2級時間節點之間NTP協議認證過程加入中間人入侵的著色Petri網模型，如圖5所示。圖5中，顏色集={1,2,…16}，各庫所所代表的顏色集元素具體為：1=利用PKA生成的cookie_Request消息，2=cookie，3= {cookie}PKA，4=D{{cookie}PKA,{cookie}SKB},5= D{keyID,MACasyn,NTP報文}，6= D{MACr_asyn, NTP回復報文}，7=AC(通過)，8=RE(拒絕)，9= {cookie} SKB，10=PKA，11=中間人利用PKM生成的cookie請求cookie_Request′，12={cookie}PKM，13=D {{cookie}PKM,{cookie}SKB}，14= Autokey，15=D {MACr_asyn_c，篡改的NTP回復報文}，16=keyID。

圖5 加入中間人入侵的認證過程CPN模型

圖5加入中間人節點，該節點通過t2截獲節點發送給節點的cookie請求報文，保存PKA后偽裝成客戶端IP，以中間人自己的PKM發送偽造的cookie請求報文8(即cookie_Request′)給節點。節點接收到偽造的cookie請求，以為是節點發送的cookie請求，于是計算cookie，同時以中間人公鑰PKM和節點自己的私鑰SKB加密，將加密后的信息{cookie}PKM和{cookie}SKB經t9重新組包后以偽造的cookie響應報文(即cookie_Response′)形式發送至中間人節點。中間人通過t11截獲并解析，獲得，節點身份認證的關鍵信息cookie庫所2，中間人經t12利用前面保存的PKA將cookie加密為{cookie}PKA，再通過t13將{cookie}PKA和{cookie} SKB重新組包以cookie響應報文(即cookie_ Response)形式發送至節點。節點誤以為這個被中間人處理過的cookie_Response報文是從節點發送過來的，進行正常驗證解析，然后發送keyID，MACasyn和NTP報文構成的時間請求報文(即syns_Request)。中間人經變遷t20截獲并保存keyID，然后轉發該報文至節點。節點接收解析后發送時間同步回復報文(即syns_Response)，中間人通過t26截獲該報文，篡改其中NTP回復報文中的時間信息2和3，再將篡改后的NTP報文利用已經截獲的cookie重新計算出MACr_asyn_c，并將MACr_asyn_c和篡改后的NTP報文經t27重新組包為6以篡改后的時間響應報文(即syns_ Response′)的形式發送至節點。節點接收到篡改后的時間響應報文，利用已經泄露的cookie計算驗證，誤以為時間響應報文是從節點發送來的，因此會根據報文中被篡改的時間信息校正本地時間，中間人達到任意操控節點時間的目的。

表1 2級時間節點庫所關聯逆子矩陣

將以上16個顏色集元素統一用符號1~16表示。根據圖5所示著色Petri網模型，可得到該模型的關聯矩陣，為了便于分析計算，這里列出其關聯逆矩陣，且未列出全0行和全0列。根據所屬庫所分類，將整個逆矩陣拆分為4個逆子矩陣，分別為2級時間節點庫所子矩陣、1級時間節點庫所子矩陣、中間人節點子矩陣和1~8子矩陣，如表1~4所示。

表2 1級時間節點庫所關聯逆子矩陣

表3 中間人節點庫所關聯逆子矩陣

表4 ch1~ch8庫所關聯逆子矩陣

4 協議認證過程不安全狀態可達性分析

該模型中初始狀態0=[0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0]T為一個36維列向量，其各列分別代表1~9，1~4，1~9，5~8，1~10共36個庫所的初始狀態。

分析中間人對NTP協議認證過程的攻擊步驟，協議認證過程中在中間人攻擊下的不安全終止狀態=[0 0 AC 0 0 0 AC 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 AC 0 0 0 0]T。

將初始狀態0和不安全終止狀態代入式(5)，在圖5模型中，系數矩陣T的秩為31 ，增廣矩陣(T,M)的秩也為31，兩者相同，因此方程有解。

進一步解得=[1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1]T，由此非負整數解可以確定攻擊者的攻擊實施序列為：=t1t2t3t4t5t6t7t8t9t10t11t12t13t14t15t16t17t18t19t20t21t22t23t24t25t26t27t28t29t30。

至此可以確定該不安全終止狀態M由初始狀態可達，針對NTP協議認證過程中cookie請求的攻擊可以實現。

5 結論

1) 基于Autokey模型的NTP協議認證過程中的cookie請求階段，入侵者可偽裝成中間人對協議進行攻擊，通過偽造、截獲、轉發4個關鍵庫所1~4的信息，入侵者用自己的公鑰給一級時間節點發送cookie請求，進而獲得1和2級時間節點進行身份認證的關鍵信息cookie，使得2級時間節點誤以為中間人是1級時間節點，進而接受中間人發送的篡改后的時間同步報文，最終入侵者成功實現操縱2級時間節點同步時間的目的。

2) 造成這一安全風險的主要原因是由于客戶端身份驗證缺失，使得惡意節點可以利用此漏洞成功冒充客戶端進行攻擊。在Autokey模型的NTP協議認證過程中的cookie交換過程中可以引入雙向認證機制以有效降低攻擊者利用此漏洞對鐵路時間同步協議進行攻擊成功的概率。

[1] Rudman L, Irwin B. Characterization and analysis of NTP amplification based DDos attacks[C]// Information Security for South Africa (ISSA), 2015. IEEE, 2015: 1?5.

[2] 刁造翔, 章小寧, 王淑君, 等. 局域網條件下的NTP偽造服務器攻擊技術[J]. 電子信息對抗技術, 2016, 31(6): 63?68. DIAO Zaoxiang, ZHANG Xiaoning, WANG Shujun. et al. The vulnerability of NTP under forged server attack[J]. Electronic Information Warfare Technology, 2016, 31(6): 63?68.

[3] Malhotra A. Attacking the network time protocol[C]// The Network and Distributed System Security Symposium. San Diego: 2016: 1?15.

[4] 朱越凡, 馬迪, 王偉, 等. 一種NTP協議隱蔽通道[J]. 計算機系統應用, 2017, 26(5): 119?125. ZHU Yuefan, MA Di, WANG Wei. et al. Covert channel based on NTP protocol[J]. Computer Systems Applications, 2017, 26(5): 119?125.

[5] 沈佳駿. IEEE1588精確時鐘同步協議脆弱性分析[D]. 杭州: 浙江大學, 2015: 29?32. SHEN Jiajun. Vulnerability analysis of IEEE 1588 precise time protocol[D]. Hangzhou: Zhejiang University, 2015: 29?32.

[6] Mills D, Dalaware U, Haberman B. Network time protocol version 4: Autokey specification[R]. IETF RFC 5906, 2010.

[7] Mills D, Martin J, Burbank J, et al. Network time protocol version 4: Protocol and algorithms specification [R]. 2010.

[8] Dowling B, Stebila D, Zaverucha G. ANTP: Authenticated NTP implementation specification[R]. Microsoft Research Technical Report, MSR-TR-2015-19, 2015.

[9] R?ttger S, Adamek J, Milius S. Analysis of the ntp autokey procedures[R]. Technische Universit?t Braunschweig, 2012: 9?11.

[10] 張友鵬, 張珊, 王鋒, 等. 一種改進型網絡時間協議在TDCS/CTC系統的應用研究[J]. 鐵道學報, 2015, 37(10): 75?82. ZHANG Youpeng, ZHANG Shan, WANG Feng, et al. Research on application of improved NTP protocol in TDCS/CTC system[J]. Journal of the China Railway Society, 2015, 37(10): 75?82.

Modeling and security analysis of railway time synchronization protocol based on colored petri nets

LAN Li1, 3, ZHANG Youpeng2

(1. School of Electronic and Information Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China; 2. School of Automatic & Electrical Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China; 3. Key Laboratory of Opto-technology and Intelligent Control, Ministry of Education, Lanzhou Jiaotong University, Lanzhou 730070, China)

In view of the security of railway time synchronization protocol based on Autokey model, this paper proposed analyzing the protocol security based on colored Petri nets. Firstly, the sequence of railway time synchronization protocol based on Autokey model and its execution process were analyzed deeply. Secondly, focusing on its authentication stage, the model of the normal authentication and the authentication under the man-in-the-middle invasion were constructed respectively based on the colored Petri nets. The unsafe state of protocol authentication process during the middleman intrusion is analyzed, and the model state equation was established. Finally, the security of railway time synchronization protocol was analyzed by reversed state analysis, the implementation sequence of the man-in-the-middle attack protocol during the authentication phase was obtained. The results show that the authentication process of railway time synchronization protocol based on Autokey model is unsafe.

railway time synchronization protocol; man-in-the-middle; colored Petri nets; security analysis

10.19713/j.cnki.43?1423/u.2019.04.033

U285.5+5

A

1672 ? 7029(2019)04 ? 1089 ? 08

2018?06?26

國家自然科學基金資助項目(51567014)；中國鐵路總公司科技研究開發計劃課題資助項目(2015X007-H)；光電技術與智能控制教育部重點實驗室(蘭州交通大學)開放課題資助項目(KFKT2018-12)

蘭麗(1978?)，女，寧夏平羅人，副教授，博士研究生，從事交通信息技術研究；E?mail：lanli_laoshi@mail.lzjtu.cn

(編輯 蔣學東)