论文部分内容阅读
摘 要：随着时间同步技术在民用航空领域的广泛发展，能够实时地保证NTP协议的安全运行变得至关重要。由于NTP协议自身具备一定的安全缺陷，因此，对NTP协议的安全机制进行分析是十分必要的。首先，考虑到NTP协议的无连接特性，使用CPN tools软件建立NTP协议在正常工作模式下的有色Petri网模型，并分析协议在进行时间同步过程中存在的漏洞。然后，在NTP协议正常工作模型的基础上，加入入侵者节点，构建NTP协议受到入侵的有色Petri网模型。最后，使用状态空间询问法获取模型的不安全节点并生成入侵序列。结果表明，NTP协议的服务器身份验证过程是不安全的。
关键词：安全性;时间同步协议;漏洞;CPN tools
国民用航空时间同步网采用NTP协议，并按照“服务器/客户端”的模式进行时间同步。由于NTP协议是一种无连接性的协议[1]，其在进行时间同步时数据源端和终端不需要提前建立连接，因此，NTP协议自身就存在一定的安全隐患，使得其更容易遭受来自第三者的入侵[2]。目前，针对NTP协议的安全防护，最新一版的NTP协议标准提出了使用Autokey模型自动向服务器与客户端分发对称摘要秘钥的安全机制[3]。但是，在该安全机制下，NTP协议在其服务器身份验证的过程中依然存在安全漏洞，入侵者一旦通过了身份验证，便有可能同时取得NTP服务器与客户端双方的信任。在此情况下，入侵者可以对整个时间同步网发动攻击：一方面，入侵者可以截获传输信道上的报文，并发送虚假的时间信息，造成同步网设备的时间信息紊乱;另一方面，入侵者还可以发动攻击消耗网络内的资源，并最终导致时间同步网系统的瘫痪。因此，在使用NTP协议时，有必要对其安全性进行分析。
有色Petri网作为一种图形化语言的建模工具，非常适用于针对通信、同步以及资源共享等种类系统的建模。因此，本文将有色Petri网引入NTP协议的安全性分析，基于CPN Tools，首先建立NTP协议正常工作时的有色Petri网模型，分析协议存在的漏洞和安全隐患;然后构建加入了入侵者的NTP协议有色Petri网模型，并通过仿真分析入侵的可达性。
1 有色Petri网定义
有色Petri网是一个满足以下条件的六元组：
式中：C是一个非空的有限类型集，称为颜色集，在有色Petri网中，一个颜色集可以包含一个或多个令牌;P是一个有限集合，称为库所集，在有色Petri网模型中，库所集表征了模型可以存在的所有状态;T是一个有限集合，称为变迁集，它规定了模型中所有颜色集的活动规则;F是有向弧的集合;W表示了一个映射，该映射可以对每条有向弧赋予一个k维非负整数向量，即F→{0，1，...}k;M也表示一个映射，该映射可以对每个库所赋予一个k维非负整数向量，即P→{0，1，...}k。
2 NTP协议描述
NTP协议具有三种工作模式，分别为主从模式、广播模式和对称模式。我国民用航空时间同步网采用了NTP协议的主从工作模式，通过服务器與客户端之间的往返NTP报文来确定两地时钟的差值和报文在网络中传输的延时。NTP协议的同步精度能够达到毫秒级，目前已可以满足我国民用航空时间同步网对时间同步精度的要求。
3时间同步网协议的有色Petri网建模
3.1 NTP协议在正常工作模式下的有色Petri网建模
在时间同步网中，一级时间节点作为服务器，向作为客户端的二级时间节点发送时间信息。事实上，在进行时间同步之前，客户端需要先对服务器的身份进行验证，只有当身份验证通过后，服务器和客户端之间才会开始进行时间同步。该验证过程如下：
其中，A表示服务器，B表示客户端，J表示可信的第三方证书发布机构，Kx（Y）表示对数据Y使用X的公钥进行加密，A和B分别为服务器和客户端的主体标识。当服务器A需要同客户端B进行时间同步时，A首先生成一个自己的秘钥KAJ，使用第三方机构J的公钥KJPB加密后连同主体标识B一起发送给J。J收到该消息后，用相对应的私钥KJPR解密此消息，取得A的秘钥KAJ，然后将主体标识A发送至B。B收到A的主体标识以后，生成对应秘钥KAB同时再次用KJPB加密，并将此加密信息连同主体标识A一起发送给J。J收到该消息后，再次用相对应的私钥KJPR解密此消息并获取KAB，并使用之前从A处获得的秘钥KAJ对KAB进行加密，然后将消息返回给A。这样，A便能够得到B生成的秘钥KAB，进而完成与B的身份验证。
因此，使用CPN Tools建立时间同步网NTP协议在正常工作时的有色Petri网模型如图1所示：
图1中，替代变迁T1表示服务器主体A，在NTP协议的身份验证过程中，服务器A会首先产生一个MI类令牌，该令牌会发送给J，从而告知J服务器A是身份验证的发起者。替代变迁T2表示第三方认证机构J，在身份验证过程中，T2会消耗一个MI类型的令牌并发送一个I类型的令牌。替代变迁T3表示客户端主体B，在身份验证过程中，B会消耗一个I型令牌，并产生一个M型令牌。
根据第三方认证机构J的行为，建立其CPN模型如图2所示：
3.2 NTP协议漏洞分析
NTP协议属于无连接性协议，在进行数据传输之前源端和终端不会提前建立连接。NTP协议在进行时间同步之前，NTP服务器会对自己接收到的所有同步请求报文一一做出回应。因此，不论发送请求报文的客户端是否合法，它都会收到由NTP服务器发送过来验证信息。一旦在该网络中出现了入侵者，凭借从NTP服务器得到的验证信息，入侵者可以通过伪装自己的真实身份骗取其它合法客户端的信任。在这种情况下，入侵者可以以服务器的身份向该网络中的所有客户端发送虚假的时间信息，以达到对网络的破坏效果。
3.3 NTP协议受到入侵的有色Petri网建模 在入侵模型中，入侵者节点将由替代变迁T4表示。入侵者节点可以完成对其他节点之间通信的控制，因此，入侵者节点能够将其他节点之间的通信信息拦截并储存起来，并可以在适当的情况下调用。
在图3所示模型的基础上，加入入侵者节点，由替代变迁T4表示入侵者节点，可以得出加入入侵者的NTP协议CPN顶层模型如图3所示。由图3可知，入侵者模型由4个子进程构成，每一个子进程都分别模拟了入侵者针对所拦截的令牌颜色类型所发生的一些可能的行为。
4 协议不安全状态的可达性分析
对NTP协议而言，当其进行服务器身份验证时，应该保证会话秘钥Kab的保密性。即在整个验证过程中，只有服务器、客户端以及第三方认证机构知道该会话秘钥。因此，对于入侵者而言，一旦入侵者能够获取该会话秘钥，就表明入侵者能够完成对协议的入侵。在该模型中，一旦含有秘钥协议Kab的令牌到达了入侵者的融合集库所中，则可以认定该状态为协议的不安全状态，从而证明了入侵是可达的。
为了确定协议的不安全状态，首先需要找到模型中的不安全节点。在CPN Tools中，可以利用状态空间询问的方法来找到目标节点，在本模型中，需要通过状态空间询问来找到融合集库所OF中含有令牌cK（Kab）的节点。为此，状态空间询问可以采用如下语言进行：
根据模型生成的状态空间报告，该模型由19297个节点和22479个弧构成。在执行上式所示的函数时，可以得到一个返回的节点列表，列表中包含一个节点为19260。为此，将第19260号节点设为终止节点，使用CPN Tools生成由初始狀态（1号节点）到终止状态（19260号节点）的路径。
根据图5所示的入侵发生序列，可以对入侵者的入侵步骤做如下描述：
其中，I（A）表示I冒充A，“I（A）→J： X”表示I冒充A向J发送消息X，“J→I（A）： X”表示I截取J发送给A的消息X。KI为入侵者生成的秘钥。其它标识的含义同3.1章节。该入侵步骤表明，入侵者最终可以解密消息KI（KAB），并得到KAB，进而成功冒充服务器A与客户端B进行会话。
5 结 论
本文基于有色Petri网，结合CPN Tools软件，提出了一种针对时间同步网的NTP协议安全性分析方法。
基于状态空间询问的方法分析NTP协议受到入侵有色Petri网模型，可以获取NTP协议模型中的不安全节点，进而生成入侵发生序列，从而确定了模型不安全状态的可达性。
通过分析入侵发生序列，可以得到入侵者入侵NTP协议的详细步骤，该入侵步骤表明：入侵者能够利用NTP协议在进行服务器身份验证过程中存在的漏洞，获取服务器以及客户端的密钥，进而获取客户端的信任，实现对NTP协议的入侵。
参考文献：
[1] Y Bekeneva， N Shipilov， K Borisenko. Simulation of DDoS-attacks and Protection Mechanisms Against Them[J]. IEEE Faculty of Computer Science and Technology，2015：49-55.
[2] Vaithiyanathan， Gracelin Sheeba， Enda Elizabeth. A Novel method for Detection and Elimination of Modification Attack and TTL attack in NTP[C]. International Conference on Recent Trends in Information， Telecommunication and Computing，2010：60-64.
[3] D Mills， U Dalaware， B Haberman. Network Time Protocol Version 4： Autokey Specification [S]. IETF RFC 5906， June 2010.
作者简介：
张昊磊（1990-）男，汉，籍贯：甘肃酒泉，职务职称：助理工程师，学历：硕士研究生，单位： 民航甘肃空管分局 技术保障部自动化室，研究方向：时间同步网。
（民航甘肃空管分局 技术保障部自动化室，甘肃 兰州 730070）
关键词：安全性;时间同步协议;漏洞;CPN tools
国民用航空时间同步网采用NTP协议，并按照“服务器/客户端”的模式进行时间同步。由于NTP协议是一种无连接性的协议[1]，其在进行时间同步时数据源端和终端不需要提前建立连接，因此，NTP协议自身就存在一定的安全隐患，使得其更容易遭受来自第三者的入侵[2]。目前，针对NTP协议的安全防护，最新一版的NTP协议标准提出了使用Autokey模型自动向服务器与客户端分发对称摘要秘钥的安全机制[3]。但是，在该安全机制下，NTP协议在其服务器身份验证的过程中依然存在安全漏洞，入侵者一旦通过了身份验证，便有可能同时取得NTP服务器与客户端双方的信任。在此情况下，入侵者可以对整个时间同步网发动攻击：一方面，入侵者可以截获传输信道上的报文，并发送虚假的时间信息，造成同步网设备的时间信息紊乱;另一方面，入侵者还可以发动攻击消耗网络内的资源，并最终导致时间同步网系统的瘫痪。因此，在使用NTP协议时，有必要对其安全性进行分析。
有色Petri网作为一种图形化语言的建模工具，非常适用于针对通信、同步以及资源共享等种类系统的建模。因此，本文将有色Petri网引入NTP协议的安全性分析，基于CPN Tools，首先建立NTP协议正常工作时的有色Petri网模型，分析协议存在的漏洞和安全隐患;然后构建加入了入侵者的NTP协议有色Petri网模型，并通过仿真分析入侵的可达性。
1 有色Petri网定义
有色Petri网是一个满足以下条件的六元组：
式中：C是一个非空的有限类型集，称为颜色集，在有色Petri网中，一个颜色集可以包含一个或多个令牌;P是一个有限集合，称为库所集，在有色Petri网模型中，库所集表征了模型可以存在的所有状态;T是一个有限集合，称为变迁集，它规定了模型中所有颜色集的活动规则;F是有向弧的集合;W表示了一个映射，该映射可以对每条有向弧赋予一个k维非负整数向量，即F→{0，1，...}k;M也表示一个映射，该映射可以对每个库所赋予一个k维非负整数向量，即P→{0，1，...}k。
2 NTP协议描述
NTP协议具有三种工作模式，分别为主从模式、广播模式和对称模式。我国民用航空时间同步网采用了NTP协议的主从工作模式，通过服务器與客户端之间的往返NTP报文来确定两地时钟的差值和报文在网络中传输的延时。NTP协议的同步精度能够达到毫秒级，目前已可以满足我国民用航空时间同步网对时间同步精度的要求。
3时间同步网协议的有色Petri网建模
3.1 NTP协议在正常工作模式下的有色Petri网建模
在时间同步网中，一级时间节点作为服务器，向作为客户端的二级时间节点发送时间信息。事实上，在进行时间同步之前，客户端需要先对服务器的身份进行验证，只有当身份验证通过后，服务器和客户端之间才会开始进行时间同步。该验证过程如下：
其中，A表示服务器，B表示客户端，J表示可信的第三方证书发布机构，Kx（Y）表示对数据Y使用X的公钥进行加密，A和B分别为服务器和客户端的主体标识。当服务器A需要同客户端B进行时间同步时，A首先生成一个自己的秘钥KAJ，使用第三方机构J的公钥KJPB加密后连同主体标识B一起发送给J。J收到该消息后，用相对应的私钥KJPR解密此消息，取得A的秘钥KAJ，然后将主体标识A发送至B。B收到A的主体标识以后，生成对应秘钥KAB同时再次用KJPB加密，并将此加密信息连同主体标识A一起发送给J。J收到该消息后，再次用相对应的私钥KJPR解密此消息并获取KAB，并使用之前从A处获得的秘钥KAJ对KAB进行加密，然后将消息返回给A。这样，A便能够得到B生成的秘钥KAB，进而完成与B的身份验证。
因此，使用CPN Tools建立时间同步网NTP协议在正常工作时的有色Petri网模型如图1所示：
图1中，替代变迁T1表示服务器主体A，在NTP协议的身份验证过程中，服务器A会首先产生一个MI类令牌，该令牌会发送给J，从而告知J服务器A是身份验证的发起者。替代变迁T2表示第三方认证机构J，在身份验证过程中，T2会消耗一个MI类型的令牌并发送一个I类型的令牌。替代变迁T3表示客户端主体B，在身份验证过程中，B会消耗一个I型令牌，并产生一个M型令牌。
根据第三方认证机构J的行为，建立其CPN模型如图2所示：
3.2 NTP协议漏洞分析
NTP协议属于无连接性协议，在进行数据传输之前源端和终端不会提前建立连接。NTP协议在进行时间同步之前，NTP服务器会对自己接收到的所有同步请求报文一一做出回应。因此，不论发送请求报文的客户端是否合法，它都会收到由NTP服务器发送过来验证信息。一旦在该网络中出现了入侵者，凭借从NTP服务器得到的验证信息，入侵者可以通过伪装自己的真实身份骗取其它合法客户端的信任。在这种情况下，入侵者可以以服务器的身份向该网络中的所有客户端发送虚假的时间信息，以达到对网络的破坏效果。
3.3 NTP协议受到入侵的有色Petri网建模 在入侵模型中，入侵者节点将由替代变迁T4表示。入侵者节点可以完成对其他节点之间通信的控制，因此，入侵者节点能够将其他节点之间的通信信息拦截并储存起来，并可以在适当的情况下调用。
在图3所示模型的基础上，加入入侵者节点，由替代变迁T4表示入侵者节点，可以得出加入入侵者的NTP协议CPN顶层模型如图3所示。由图3可知，入侵者模型由4个子进程构成，每一个子进程都分别模拟了入侵者针对所拦截的令牌颜色类型所发生的一些可能的行为。
4 协议不安全状态的可达性分析
对NTP协议而言，当其进行服务器身份验证时，应该保证会话秘钥Kab的保密性。即在整个验证过程中，只有服务器、客户端以及第三方认证机构知道该会话秘钥。因此，对于入侵者而言，一旦入侵者能够获取该会话秘钥，就表明入侵者能够完成对协议的入侵。在该模型中，一旦含有秘钥协议Kab的令牌到达了入侵者的融合集库所中，则可以认定该状态为协议的不安全状态，从而证明了入侵是可达的。
为了确定协议的不安全状态，首先需要找到模型中的不安全节点。在CPN Tools中，可以利用状态空间询问的方法来找到目标节点，在本模型中，需要通过状态空间询问来找到融合集库所OF中含有令牌cK（Kab）的节点。为此，状态空间询问可以采用如下语言进行：
根据模型生成的状态空间报告，该模型由19297个节点和22479个弧构成。在执行上式所示的函数时，可以得到一个返回的节点列表，列表中包含一个节点为19260。为此，将第19260号节点设为终止节点，使用CPN Tools生成由初始狀态（1号节点）到终止状态（19260号节点）的路径。
根据图5所示的入侵发生序列，可以对入侵者的入侵步骤做如下描述：
其中，I（A）表示I冒充A，“I（A）→J： X”表示I冒充A向J发送消息X，“J→I（A）： X”表示I截取J发送给A的消息X。KI为入侵者生成的秘钥。其它标识的含义同3.1章节。该入侵步骤表明，入侵者最终可以解密消息KI（KAB），并得到KAB，进而成功冒充服务器A与客户端B进行会话。
5 结 论
本文基于有色Petri网，结合CPN Tools软件，提出了一种针对时间同步网的NTP协议安全性分析方法。
基于状态空间询问的方法分析NTP协议受到入侵有色Petri网模型，可以获取NTP协议模型中的不安全节点，进而生成入侵发生序列，从而确定了模型不安全状态的可达性。
通过分析入侵发生序列，可以得到入侵者入侵NTP协议的详细步骤，该入侵步骤表明：入侵者能够利用NTP协议在进行服务器身份验证过程中存在的漏洞，获取服务器以及客户端的密钥，进而获取客户端的信任，实现对NTP协议的入侵。
参考文献：
[1] Y Bekeneva， N Shipilov， K Borisenko. Simulation of DDoS-attacks and Protection Mechanisms Against Them[J]. IEEE Faculty of Computer Science and Technology，2015：49-55.
[2] Vaithiyanathan， Gracelin Sheeba， Enda Elizabeth. A Novel method for Detection and Elimination of Modification Attack and TTL attack in NTP[C]. International Conference on Recent Trends in Information， Telecommunication and Computing，2010：60-64.
[3] D Mills， U Dalaware， B Haberman. Network Time Protocol Version 4： Autokey Specification [S]. IETF RFC 5906， June 2010.
作者简介：
张昊磊（1990-）男，汉，籍贯：甘肃酒泉，职务职称：助理工程师，学历：硕士研究生，单位： 民航甘肃空管分局 技术保障部自动化室，研究方向：时间同步网。
（民航甘肃空管分局 技术保障部自动化室，甘肃 兰州 730070）