RSSP-Ⅱ协议消息鉴定层的形式化描述及验证

徐 倩 林俊亭

(兰州交通大学自动化与电气工程学院 甘肃 兰州 730070)

0 引 言

针对数据传输中可能产生的重复、重排序、插入、延迟、删除、损坏和伪装等威胁,依据欧洲列车控制系统的Subset-037[1]、Subset-098[2]标准,中国铁路总公司制定了RSSP协议,以规定信号安全设备进行安全信息交互的功能结构和协议。其中,RSSP-Ⅰ适用于封闭式传输系统,如我国客运专线的列控中心外围系统接口间;RSSP-Ⅱ[3]适用于开放式传输系统,如无线闭塞中心、临时限速服务器的外围系统接口间。RSSP-Ⅱ逐步向地铁应用,如互联互通基于通信列车控制系统(Communication-based Train Control, CBTC)的车载控制器与控制中心之间接口[4]。

协议工程是形式化的协议开发过程,能够保证协议的设计开发质量,包括协议形式化描述、形式化验证、协议实现和协议一致性测试[5-6]。目前常用的协议形式化描述技术包括有限状态机模型、Petri网模型以及通用认证协议规范语言(Common Authentication Protocol Specification Language, CAPSL)等。传统方法是最终代码实现后而通过调试来测试协议的可能漏洞,而形式化描述技术优势在于避免了自然语言描述协议存在的二义性问题,也避免了迭代测试固有的繁重工作量[7]。

文献[9]依据安全层状态转移图,建立赋时有色Petri网模型,再通过模型仿真验证了安全连接建立时间符合EuroRadio安全通信协议规范要求。文献[10]提出了China-Radio列控安全信息传输系统,是在双网冗余结构的无线局域网基础之上增加安全通信协议,也是依据状态转换图建立CPN模型,利用模型检验查找了非安全状态编号、路径, 验证功能安全性。文献[11]分析了RSSP-Ⅱ安全应用中间子层序列号、时间戳机制,建立了相应CPN模型。这些文献主要是分析所建立的安全链路的性能,而没有对消息鉴定层进行验证。文献[12]提出用通信顺序进程(Communicating Sequential Processes,CSP)对经典认证密码协议NSSK协议进行形式化描述和验证。文献[13]利用CSP对RSSP-Ⅱ的密钥服务流程和对等实体认证进行了建模。CSP没有程序结构,不具有可执行性,需要再借助Haskell 作为函数式语言实现仿真,相对有图形化建模、时态逻辑检验的CPN方法而言,验证过程与结果较为抽象、繁琐。

这些研究提供了利用CPN方法研究RSSP-Ⅱ的可行性、其他形式化方法在RSSP-Ⅱ的应用,针对RSSP-Ⅱ协议的消息鉴定层仍存在的研究不足。本文基于CPN理论及模型检验方法,在分析会话密钥生成、对等实体认证、消息源认证等协议流程后建立了CPN模型,刻画静态结构、动态行为。依次验证模型本身的正确性、基本行为属性、特定属性,保障RSSP-Ⅱ协议开发过程的质量,推广RSSP-Ⅱ在CBTC的应用。

1 RSSP-Ⅱ协议的MASL层功能概述

1.1 RSSP-Ⅱ协议的层次结构

如图1所示,RSSP-Ⅱ协议位于通信层、应用层之间且由下到上包含的层次及其功能如下:

图1 RSSP-Ⅱ协议的层次结构

(1) 冗余适配管理层(Adaptation &redundancy management Layer, ALE) :提供数据多路传输的管理,完成MASL 与传输控制协议之间的链路配置和必要时协议数据单元的重传。

(2) 消息鉴定安全层:预防损坏、伪造和篡改等威胁。当前主要措施是为通信报文附加消息鉴别码(Message Authentication Code, MAC) 和连接标识符(源和目的地标识符),实现消息的真实性、消息的完整性,以及访问保护。MASL层为本文研究对象。

(3) 安全应用中间层(Safety Application Intermediate, SAI) :预防延迟、重排序、删除、重复等威胁。当前措施主要是为通信数据包添加序列号实现序列错误防护,增加三重时间戳或者执行周期,实现消息时效性防护。

通信进程可分为以下4个部分。本文研究的MASL层的协议流程在前两个阶段。

(1) 建立安全连接:传输安全地址信息给通信功能模块;执行对等实体认证进程。

(2) 安全数据传输:常规数据的消息源认证进程;传输层提供服务原语进程。

(3) 释放安全连接:发送释放连接的通知消息即可释放整个安全连接。

(4) 错误处理:根据不同错误情况,通过安全报告标识报告等措施给下层安全用户。

1.2 密钥层级及其功能说明

如图2所示,MASL 层应用了三级密钥。

图2 各密钥功能说明示意图

(1) 3级传输密钥(Transmission Key, KTRANS):对密钥管理中心(Key Management Center, KMC)和通信系统之间的密钥管理通信进行保护。每个KMC与信号安全设备实体的关系需要一个KTRANS。KTRANS1、KTRANS2分别对KMC与信号安全设备之间所交互消息、KMAC的值进行认证和校验。

(2) 2级验证密钥(Key of Message Authentication Code, KMAC): KMC事先分配KMAC给信号安全设备,使用相同KMAC设备之间才能建立安全连接。

(3) 1级会话密钥(Key of Section MAC, KSMAC):验证信号安全设备间通过安全连接传输的数据,仅在本次安全连接期间有效。

1.3 对等实体认证流程

对等实体认证用于在建立安全连接过程中,确认通信实体的身份是否真实、合法、唯一。MASL层间传输的数据称为安全-协议数据单元(Safety Protocol Data Unit, SaPDU),AU1 SaPDU、AU2 SaPDU、AU3 SaPDU分别表示对等认证协议中第一次、第二次、第三次消息。Text为各SaPDU规定格式及内容,p为补足64位整数倍的填充数据。过程描述如图3所示。

图3 对等实体认证流程示意图

图4 CPN模型示意图

设备1提出与设备2的建立安全连接通信请求,密钥管理中心将分配给设备1、2验证密钥KSMAC。设备1生成一个随机数R1,自身保存并作为AU1 SaPDU的一部分发往设备2。设备2收到后,生成随机数R2,利用R1、R2和验证密钥K12通过3-DES加密算法,生成会话密钥Ks,设备2生成AU2 SaPDU并发送给设备1。设备1收到AU2 SaPDU后,用R1、R2、K12生成会话密钥Ks,并利用Ks检验AU2 SaPDU的正确性。若正确,则设备1用Ks加密 AU3 SaPDU并发送给设备2,最后设备2用Ks检验AU3 SaPDU。通过以上对等实体认证,设备1、设备2确认彼此拥有相同的会话密钥Ks,并推断有相同的KMAC,完成身份验证。

1.4 消息源验证

消息源验证用于保证传送过程中信息的完整性,即消息未被篡改、重放或延迟等。主叫方进行消息源认证加密。输入消息m、会话密钥Ks、源地址SA和目的地址DA。依次生成消息“m”,“DA|m”,“l|DA|m”,其中:l为“DA|m”的长度,p为填充数据,p和原字符串构成“l|DA|m|p”新消息字符串。由 CBC_MAC算法和会话密钥Ks进行MAC计算:

MAC(m)=CBC_MAC(Ks,l|DA|m|p)

同理,被叫方进行验证解密,生成MAC′(m)。如果MAC′(m)=MAC(m),且m方向标志正确,说明消息没有被篡改,传输消息m。

2 消息鉴定层功能的CPN模型

2.1 有色Petri网基本理论

有色Petri网是一种离散事件建模语言,由库所、变迁、弧构成网状模型,将Petri网理论与函数式编程语言CPN ML(Meta Language,元语言)结合,适用于构建并发系统的模型及分析其属性[14]。

(1) 库所(Place) 表示系统可能的状态,主要属性有库所名、颜色集(数据类型)、初始标记等。初始标记(marking)代表了该库所初始状态时的令牌(token)值,是一个与库所颜色集相同的令牌多重集。

(2) 变迁(Transition)表示引发系统状态改变的事件,主要属性有变迁名、守卫函数、延时函数和代码段。变迁的触发受到守卫函数和弧表达式的制约。

(3) 指向变迁的弧表明触发的前提条件表示变迁的激发需要从库所消耗相应的令牌(token);指向库所的弧表明变迁触发的结果表示变迁的激发需要转移相应的令牌。

CPN-Tools嵌套的ASK-CTL工具包,是CTL的一种拓展,ASK-CTL语句由布尔运算符、原子命题、路径量运算符、推导路径量运算符等组成。

(1) 布尔运算量:TT,FF:布尔值常量,val TT: True; NOT、AND、OR分别同布尔操作符、∧、∨。

(2) 原子命题:节点函数NF,参数为一个字符串、一个取状态空间节点返回布尔类型的函数,用以搜索单一状态或状态空间全部子集,即NF:string*(Node->bool)->A。弧函数AF,与NF类似,用以搜索单一变迁或变迁集合的全部子集;AF:string*(Arc->bool)->A。

(3) 路径量运算符:所有路径中, 至少有一条路径中的所有状态均为真,则操作符为真,即EXIST_UNTIL(A1,A2),A1→A2。

所有路径中, 全部路径中所有状态均为真,则返回值为真;FORALL_UNTIL(A1,A2),A1→A2。

(4) 推导路径运算量(以状态公式为例)。

① 如果从当前状态可以到A所处的状态时,则POS返回值为真,POS(A)=EXIST_UNTIL(TT,A)。POS作为变迁公式时类似。

② 如果从当前状态可以到达所有可达状态,A均为真,则INV返回值为真,INV(A)=NOT(POS(NOT(A)))。

③ 如果从当前状态,有限步数内A最终为真,则EV返回值为真EV(A)=FORALL_UNTIL(TT,A)。

④ 如果存在一条路径,其中任意状态A符合,则ALONG返回值为真,路径是无限或终止于死状态,ALONG(A)=NOT(EV(NOT(A)))。

2.2 顶层模型的描述

如图5所示,按照RSSP-Ⅱ规范中各SaPDU的格式[3]设计了本文所需的颜色集。模型中变量的类型与其相连接的库所需要保持一致,因此可根据颜色集进行变量的声明,而不再单独展开。

图5 颜色集的声明

根据第2节的分析,利用CPN-Tools建立分层CPN模型以刻画MASL层功能的静态结构及动态行为。分层机制使得用户可以按不同抽象层次建模。如图6所示,以设备1与设备2通信过程为例,可代表无线闭塞中心与列车、列车自动监控中心与列车的通信过程。以替代变迁表示交互对象,在下一级模型中替代变迁的输入库所将带有IN套接字,输出库所将带有Out套接字。KMC向Entity 1、Entity 2分配验证密钥,该过程由库所KMAC list分别到变迁KMC1、KMC2表示。变迁上的守卫函数只允许给定令牌通过。仿真后,库所KMAC1、KMAC2储存了各自KMAC,从而进入Entity 1、Entity 2子模块。

图6 顶层CPN模型

2.3 子模块模型的描述

如图7所示,当库所KMAC1上有令牌,则激活变迁Peer_entity_authentication,将开始执行实体对等认证流程进行身份验证。库所Request for Ks获得令牌,表示系统转变为获取会话密钥Ks的状态。由变迁Generate R1与库所R1进行交互,获取随机数。以库所R1的初始标记作为预先设置的随机数。模型获得R1,库所Obtain R1显示获取到的随机数。随机数R1与Text1结合,执行Combin_AU1变迁以生成AU1 SaPDU,显示在库所Obtain AU1 SaPDU上,格式为(text1,r1)。变迁Send AU1 SaPDU激活,向设备2发送AU1 SaPDU,进入Entity 2子模块。

图7 Entity1子模块

如图8所示,设备2获取到AU1 SaPDU后,激活变迁Extract R1,其输出弧的函数#2(text1,r1)用于提取随机数R1。与该过程同时进行的是,库所KMAC2上有令牌,同R1获取方式产生了随机数R2。综上已获取到KMAC2、R1、R2,将激活变迁Generate Ks2,生成会话密钥Ks2。再通过Ks2对数据加密,加密后数据格式设为(Ks2,data1),将作为数据的MAC码。结合MAC码、R2值、Text2,激活变迁Combin_AU2,生成AU2 SaPDU。与生成AU1 SaPDU的过程相同,库所Obtain AU2 SaPDU上有令牌,再激活变迁Send AU2 SaPDU,向设备1发送AU2 SaPDU,进入Entity1子模块。

图8 Entity 2子模块

如图7所示,提取了R2,获取R1、KMAC2,激活变迁Generate Ks1,依次生成会话密钥Ks1、包含Text4的AU3 SaPDU,再进入Entity 2模块。如图8所示,设备2对AU3 SaPDU检验,模型默认设置检验通过,库所Peer_entity_ authentication_results上的令牌作为是否完成实体对等认证的标志。此后,设备2的MASL层向SAI层发送Sa-Connect.indication原语,SAI层处理后反馈Sa-Connect.request原语。变迁MASL Process表示MASL收到SAI层信息后进行处理,至库所Start to generate AR,系统变为产生AR SaPDU的状态,结合Text6与已生成的MAC码,至库所Obtain AR,以令牌表示生成的AR SaPDU,发送给设备1。

进入Entity1模块后,收到AR SaPDU表示安全通信链接已建立,开始发送应用数据,包含在DT SaPDU,需要进行数据加密,该过程由变迁Message encryption表示,生成的DT SaPDU由库所DT SaPDU上的令牌表示。令牌流入Entity 2模块,需要进行消息解密,检查MAC码,最终消息源验证结果显示在库所Message_source_authentication _results上。

3 MASL功能安全性的形式化验证

通过CPN-Tools的仿真工具,可观察到令牌在网络中流动,独立测试模型的不同部分及对模型进行全面测试。但形式化验证认为仿真只能执行有限步数,适用于发现模型明显的错误。而对于刻画安全苛求系统的模型,无法证明错误不存在,因而需要具有严格数学语法、语义的模型检验等形式化验证方法,详尽地检查所有可能的状态[15]。系统属性可分为两类:

(1) 领域无关属性即模型的基本属性。合理的CPN模型要求能够合理解释死标记,不发生死锁、活锁等现象。当到达某个标记时,若进入活锁状态,则无法退出,会进行产生无用信息的无限执行。死锁现象是由于包含自锁终端、死标记导致的模型意外中断[16]。

(2) 领域相关属性是结合模型特定领域知识,进行基于逻辑的模型检验,检查特定的功能。CPN-Tools可通过ASK-CTL工具包进行查询,根据判定结果返回值来确定协议的安全属性是否实现[17]。

3.1 CPN模型基本属性验证

统计信息如图9所示,包含状态空间与强直通分量图(Strongly connected component,Scc)的节点、弧的数量。节点表示可达标记,弧表示发生的绑定元素,节点与弧形成的交替序列称为有向路径。如果两个状态空间节点相互可达,则划分到同一个Scc图中。本文构建模型的状态空间及其Scc图节点、弧数量一致,表明没有自循环,系统模型无活锁。

图9 统计信息的截图

库所包含的令牌数量都是有界的,因此本文不再对报告中有界性进行安全分析。其他属性如图10所示。

图10 其他属性信息的截图

(1) 家态性描述模型是否包含家态标记(可以从任何可达标记到达的标记)。结果表明家态标记是220节点,是状态空间的最后一个节点,是合理的。

(2) 活性提供死标记、死变迁和活变迁的信息。死标记是模型终止状态,此时没有变迁能够再被激活,模型至少需要一个死标记使得模型正常终止,如果多于1个则需要进行合理性分析。

所构造的模型只有一个死标记,且死标记与家态标记均为第220个节点,是模型的最后一个节点,因此表明模型能够正常终止,不存在意外中断的情况,不包含死锁。没有死变迁实例(始终无法激活的变迁,通常由于模型设计缺陷而造成),表示所有的变迁都能被激活,模型不存在冗余设计缺陷。活变迁实例指从任何可达标记总能找到包含该变迁的发生序列。由于有死标记,而死标记不包含任何变迁,因此本文所构造的模型不存在活变迁是合理的。

(3) 公平性指出公平变迁,该变迁是指在所有无限发生序列中无限地发生。由于本文所构造的模型不是循环执行,因此不存在无限发生序列。

3.2 领域相关属性的验证

从RSSP-Ⅱ规范中提取功能属性,可分为3类属性期望状态最终会达到、可能会发生一些状态、不期望的状态不会发生。以下3个属性作为例证。

属性1设备1、设备2总会获得来自KMC的KMAC1、KMAC2。

验证属性1的语句用到了推导路径运算量EV,所有路径的状态都为真时,则返回值为真;原子命题中的 节点函数NF。由图11可知,属性1验证结果正确。

图11 属性1的验证语句及结果图

属性2Ks1与Ks2的生成有先后,可以验证Ks1、Ks2并非同时产生。

如图12所示,验证属性2的语句中由于随机数的不确定使得库所Ks1、Ks2的令牌无法确定,因此用[]表示。用到了INV(M)。验证结果false表示上式不能成立,这与Ks1与Ks2不能同时生成则不满足INV条件的事实一致。

图12 属性2的验证语句及结果图

图13 属性3的验证语句及结果图

属性3验证MASL功能时表现为能够完成对等实体认证、消息源验证。

验证属性3语句同语句1。结果表明,所构造的模型满足设计规范,能够完成MASL的功能。

4 结 语

(1) 形式化描述过程:有色Petri网能够描述离散事件系统的静态结构、动态行为。基于协议流程分析,本文按照自上而下的原则建模,所建立的CPN模型刻画了密钥服务、对等实体认证、消息源认证的流程。在建模过程中,借助CPN-Tools可观察仿真结果,本文模型已通过了语法检测,没有建模错误。

(2) 模型检验过程:模型检验是常用的形式化验证手段,通过遍历检查所有状态空间来自动化地验证该模型是否满足给定的属性。本文先从状态空间报告中获取CPN模型的基本属性,证明了反映设计规范的模型并没有死锁、活锁、冗余等设计缺陷。从RSSP-Ⅱ规范中获取MASL具体功能属性,编写ASK-CTL查询语句,进行验证。本文以三个属性的ASK-CTL语句为例,证明逻辑推理满足预期,满足MASL加密性、认证性的功能安全性的需求,下一步工作为根据CPN模型生成代码框架,基于模型的形式化开发过程能够保障RSSP-Ⅱ协议的开发质量。