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

蘭麗，張友鵬

?

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

蘭麗1, 3，張友鵬2

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

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

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

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

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

1.1 協(xié)議描述

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

圖1 基于Autokey模型的NTP報(bào)文格式

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

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

2) 交換證書?？蛻舳税l(fā)送證書請求報(bào)文，服務(wù)器回復(fù)報(bào)文中包含證書，客戶端獲取服務(wù)器端的公鑰PKB。

3) 客戶端向服務(wù)器請求cookie?？蛻舳死脧姆?wù)器獲得的cookie，驗(yàn)證服務(wù)器端身份及數(shù)據(jù)包的完整性。

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

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

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

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

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

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

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

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

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

1.2 協(xié)議漏洞分析

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

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

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

2.1 相關(guān)概念

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

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

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

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

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

3) 構(gòu)建中間人攻擊下的鐵路時(shí)間同步協(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)方程的一個(gè)非負(fù)整數(shù)解。

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

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

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

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

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

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

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

1=利用PKA生成的cookie_Request消息，2=cookie，3={cookie}PKA，4=D{{cookie}PKA, {cookie}SKB}，5=D{keyID,MACasyn,NTP報(bào)文}，6= D{MACr_asyn,NTP回復(fù)報(bào)文}，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請求報(bào)文cookie_Request，中間人截獲此報(bào)文，存儲客戶端公鑰PKA。同時(shí)，中間人偽裝成客戶端，用自己的公鑰PKM給服務(wù)器發(fā)送一個(gè)cookie請求報(bào)文cookie_Request′。

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

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

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

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

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

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

根據(jù)上述攻擊步驟，建立1和2級時(shí)間節(jié)點(diǎn)之間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報(bào)文}，6= D{MACr_asyn, NTP回復(fù)報(bào)文}，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ù)報(bào)文}，16=keyID。

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

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

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

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

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

表3 中間人節(jié)點(diǎn)庫所關(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為一個(gè)36維列向量，其各列分別代表1~9，1~4，1~9，5~8，1~10共36個(gè)庫所的初始狀態(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ù)解可以確定攻擊者的攻擊實(shí)施序列為：=t1t2t3t4t5t6t7t8t9t10t11t12t13t14t15t16t17t18t19t20t21t22t23t24t25t26t27t28t29t30。

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

5 結(jié)論

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

2) 造成這一安全風(fēng)險(xiǎn)的主要原因是由于客戶端身份驗(yàn)證缺失，使得惡意節(jié)點(diǎn)可以利用此漏洞成功冒充客戶端進(jìn)行攻擊。在Autokey模型的NTP協(xié)議認(rèn)證過程中的cookie交換過程中可以引入雙向認(rèn)證機(jī)制以有效降低攻擊者利用此漏洞對鐵路時(shí)間同步協(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]. 計(jì)算機(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精確時(shí)鐘同步協(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ò)時(shí)間協(xié)議在TDCS/CTC系統(tǒng)的應(yīng)用研究[J]. 鐵道學(xué)報(bào), 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é)基金資助項(xiàng)目(51567014)；中國鐵路總公司科技研究開發(fā)計(jì)劃課題資助項(xiàng)目(2015X007-H)；光電技術(shù)與智能控制教育部重點(diǎn)實(shí)驗(yàn)室(蘭州交通大學(xué))開放課題資助項(xiàng)目(KFKT2018-12)

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

(編輯 蔣學(xué)東)