蘭麗，張友鵬

?

基于著色Petri網(wǎng)的鐵路時間同步協(xié)議建模及安全性分析

蘭麗1, 3，張友鵬2

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

針對Autokey模型的鐵路時間同步協(xié)議安全性問題，提出利用著色Petri網(wǎng)對協(xié)議進(jìn)行安全性分析。剖析Autokey模型的鐵路時間同步協(xié)議序列及其執(zhí)行流程；重點針對其認(rèn)證階段，分別構(gòu)建正常認(rèn)證和加入中間人入侵的著色Petri網(wǎng)模型，分析中間人入侵時協(xié)議認(rèn)證過程的不安全狀態(tài)，建立模型狀態(tài)方程；應(yīng)用逆向狀態(tài)分析法對鐵路時間同步協(xié)議認(rèn)證過程的安全性進(jìn)行分析，得到中間人在認(rèn)證階段攻擊協(xié)議的實施序列。研究結(jié)果表明：基于Autokey模型的鐵路時間同步協(xié)議的認(rèn)證過程是不安全的。

鐵路時間同步協(xié)議；中間人；著色Petri網(wǎng)；安全性分析

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

1 基于Autokey模型的NTP協(xié)議序列

1.1 協(xié)議描述

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

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

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

1) 初始關(guān)聯(lián)?？蛻舳撕头?wù)器端交換對稱摘要密鑰主機名。Autokey模型支持私有證書(Private Certificate，PC)和可信證書 (Trusted Certificate，TC)，默認(rèn)使用TC。

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

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

圖2 基于Autokey模型的NTP協(xié)議認(rèn)證過程

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

圖3 NTP協(xié)議時間同步過程

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

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

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

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

步驟4 客戶端A發(fā)送時間請求報文syns_ Request，報文中包含keyID、MACasyn及時間同步請求報文NTP packet?？蛻舳死脧姆?wù)器端獲取的cookie和自行選擇的keyID，利用式(2)一起計算出對稱摘要密鑰，即Autokey。再利用式(3)將計算出的Autokey與NTP packet一起計算得出MACasyn。

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

1.2 協(xié)議漏洞分析

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

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

2 基于著色Petri網(wǎng)的協(xié)議不安全狀態(tài)分析

2.1 相關(guān)概念

一個著色Petri網(wǎng)被定義為一個6元組：

2.2 基于CPN的鐵路時間同步協(xié)議不安全狀態(tài)分析方法

基于CPN的鐵路時間同步協(xié)議不安全狀態(tài)分析方法具體步驟如下：

1) 根據(jù)鐵路時間同步協(xié)議執(zhí)行流程，建立其正常工作過程的著色網(wǎng)模型；

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

3) 構(gòu)建中間人攻擊下的鐵路時間同步協(xié)議著色網(wǎng)模型；

4) 根據(jù)協(xié)議攻擊模型確定協(xié)議初始狀態(tài)0和不安全的終止?fàn)顟B(tài)M及關(guān)聯(lián)矩陣T；

5) 建立模型狀態(tài)方程：

其中：M為不安全終止?fàn)顟B(tài)；0為初始狀態(tài)，為著色網(wǎng)模型的關(guān)聯(lián)矩陣；為該狀態(tài)方程的一個非負(fù)整數(shù)解。

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

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

3 鐵路時間同步協(xié)議CPN模型

3.1 NTP協(xié)議正常認(rèn)證過程的CPN模型

鐵路時間同步網(wǎng)共分3級，1級時間節(jié)點位于鐵路總公司調(diào)度中心，2級時間節(jié)點位于各鐵路局，3級時間節(jié)點位于各站、段、所[10]。節(jié)點之間采用NTP協(xié)議的主從模式傳輸時間同步信息，協(xié)議規(guī)定，下一級時間必須從上一級獲取，根據(jù)NTP協(xié)議認(rèn)證執(zhí)行流程，建立鐵路時間同步網(wǎng)1，2級時間同步節(jié)點在正常認(rèn)證過程的CPN模型，如圖4 所示。

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

各庫所代表的顏色集={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回復(fù)報文}，7=AC(通過)，8=RE (拒絕)，9={cookie}SKB，10=keyID。其中D{?}代表將括號中的數(shù)據(jù)元素進(jìn)行組包。

圖4 基于Autokey模型的NTP協(xié)議正常認(rèn)證過程CPN模型

3.2 NTP協(xié)議認(rèn)證過程收到中間人攻擊的CPN 模型

NTP協(xié)議認(rèn)證過程受到中間人攻擊的具體步驟如下：

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

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

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

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

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

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

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

根據(jù)上述攻擊步驟，建立1和2級時間節(jié)點之間NTP協(xié)議認(rèn)證過程加入中間人入侵的著色Petri網(wǎng)模型，如圖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回復(fù)報文}，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回復(fù)報文}，16=keyID。

圖5 加入中間人入侵的認(rèn)證過程CPN模型

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

表1 2級時間節(jié)點庫所關(guān)聯(lián)逆子矩陣

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

表2 1級時間節(jié)點庫所關(guān)聯(lián)逆子矩陣

表3 中間人節(jié)點庫所關(guān)聯(lián)逆子矩陣

表4 ch1~ch8庫所關(guān)聯(lián)逆子矩陣

4 協(xié)議認(rèn)證過程不安全狀態(tài)可達(dá)性分析

該模型中初始狀態(tài)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個庫所的初始狀態(tài)。

分析中間人對NTP協(xié)議認(rèn)證過程的攻擊步驟，協(xié)議認(rèn)證過程中在中間人攻擊下的不安全終止?fàn)顟B(tài)=[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。

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

進(jìn)一步解得=[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，由此非負(fù)整數(shù)解可以確定攻擊者的攻擊實施序列為：=t1t2t3t4t5t6t7t8t9t10t11t12t13t14t15t16t17t18t19t20t21t22t23t24t25t26t27t28t29t30。

至此可以確定該不安全終止?fàn)顟B(tài)M由初始狀態(tài)可達(dá)，針對NTP協(xié)議認(rèn)證過程中cookie請求的攻擊可以實現(xiàn)。

5 結(jié)論

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

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

[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] 刁造翔, 章小寧, 王淑君, 等. 局域網(wǎng)條件下的NTP偽造服務(wù)器攻擊技術(shù)[J]. 電子信息對抗技術(shù), 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協(xié)議隱蔽通道[J]. 計算機系統(tǒng)應(yīng)用, 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精確時鐘同步協(xié)議脆弱性分析[D]. 杭州: 浙江大學(xué), 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] 張友鵬, 張珊, 王鋒, 等. 一種改進(jìn)型網(wǎng)絡(luò)時間協(xié)議在TDCS/CTC系統(tǒng)的應(yīng)用研究[J]. 鐵道學(xué)報, 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

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

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

(編輯 蔣學(xué)東)