基于着色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

(编辑 蒋学东)