TSNP：空间信息网中PCL安全高效的群组认证协议

李学峰 张俊伟 马建峰 刘 海

1(西安电子科技大学网络与信息安全学院 西安 710071)2(青海广播电视大学教育技术中心 西宁 810008) (jwzhang@xidian.edu.cn)



TSNP：空间信息网中PCL安全高效的群组认证协议

李学峰1,2张俊伟1马建峰1刘 海1

1(西安电子科技大学网络与信息安全学院 西安 710071)2(青海广播电视大学教育技术中心 西宁 810008) (jwzhang@xidian.edu.cn)

由于空间信息网络(space information network, SIN)具有高动态拓扑、卫星计算和通信资源受限等特点，当群组飞行器需要与卫星快速接入认证以实现信息连续收集或扩大观测范围时，已有协议方案不能完全满足SIN的特点和一些应用需求.为此，提出一种面向空间信息网,协议组合逻辑(protocol composition logic, PCL)安全的群组多用户快速认证协议(TSNP).基于对称加密体制、密钥分层的思想，TSNP允许群组内完成接入认证的节点向其他用户发送消息，通过计算使得群组内用户拥有与卫星通信的密钥，实现群组内用户高效安全认证或切换.通过PCL模型对TSNP各阶段协议安全属性进行分析，并使用并行和顺序组合方法证明TSNP能保障组合后协议的安全属性.实验结果表明:TSNP一方面减少了对地面管理中心的依赖程度，同时有效降低了卫星计算和通信开销.

空间信息网络；群组认证；协议组合逻辑；认证性；机密性

随着卫星通信技术的发展和人们对无线网络各种需求的激增，空间信息网络已备受关注.空间信息网络(space information network, SIN)[1]是以空间平台(如同步卫星或中、低轨道卫星、平流层气球和有人或无人驾驶飞机等)为载体，实时获取、传输和处理空间信息的网络系统.SIN在环境与灾难检测、紧急救助、全球定位、空间追踪和控制等领域有广泛的应用前景[2-5].

当群组飞行器需要接入卫星以扩大其在执行环境与灾难监测或空间追踪的范围时或者当群组飞行器因为超出某个卫星的覆盖范围时需要切换至其他卫星时，例如无人机群组，就需要一个安全的能支持认证、切换的协议来保证群组飞行器与卫星进行安全通信.这个协议主要完成2个任务：1)实现2个通信节点的身份认证，以防止非法节点假冒合法节点删除、篡改数据、占用网络资源；2)通过认证建立会话密钥，以便通过加密机制保护合法节点在网络上的通信，抵抗非法窃听.

由于SIN具有高度复杂性、动态性、开放性的特点，节点之间通信容易受到攻击者的截取、删除、篡改等安全威胁，各节点也容易受到来自敌手的攻击[6-9].例如，被动攻击者可以任意截获网络数据流、随意转发数据，同时也可对消息进行重放攻击，这样就威胁到数据的机密性以及带来非授权访问等安全威胁；主动攻击者可以截获节点间的数据流，选择性地对数据进行恶意删除或修改，同时利用节点间的链路进行假冒身份，侵入系统或发送伪造信号，此外合法的节点也会受到欺骗攻击等安全威胁.

为了确保SIN网络通信及节点免受攻击，需要认证机制保证空间信息网的通信安全，其目的是防止非授权节点接入和访问网络并阻止假冒攻击.认证协议不仅能为空间信息网中通信的节点进行身份确认并生成一个共享的秘密，建立一条安全的信道，而且还能使用组合证明的方式来证明其安全性，此外还要满足空间信息网的特点[8,10-13]：

1) 高动态拓扑，即网络拓扑结构变化频繁，卫星与卫星、卫星与节点之间的相互位置不断发生变化，这就要求卫星之间以及卫星与地面或飞行器随时切换以维持通信.

2) 计算资源和通信能力受限，由于卫星计算能力、存储器容量以及通信能力均受到宇航级芯片限制，因此设计的协议运算量和交互次数也受到限制，必须保证在不失安全性的基础上，构建简洁、高效的认证协议.公钥密码算法需要更多的计算开销，加之空间网络中数据流量较大，为了满足信息传输的实时性要求，可使用加解密速度快得多的对称密钥算法.

3) 节点之间通信往返时间长，由于空间信息网各节点(地面设备、卫星、飞行器)设备距离较远，他们之间的通信时延较大，因此设计的协议既要有安全性，同时也要保证速度和效率.设计的协议满足群组接入认证，以减少认证过程中的密码算法处理时间和通信开销，从而达到减少认证持续时间、提高认证效率.

4) SIN复杂性决定认证协议可能需要多阶段协议执行，这些协议组合后应能保证协议的安全属性.另外，由于SIN开放性，节点之间的通信数据容易被攻击者截取甚至篡改，合法的节点也容易受到伪装攻击，因此要考虑节点之间通信的安全性需求.

由于上述空间信息网的特点，对设计面向空间信息网的群组多用户快速认证协议带来了挑战.

相关工作：

1) 组合安全理论.基于逻辑的可组合安全模型PCL是协议组合理论的典型代表之一.

PCL是一种支持协议属性证明逻辑推导模型[14]，它由Cord演算、协议逻辑(语法和语义)、证明系统组成.PCL[15-16]是一个抽象了关于跟踪的参数，消除了关于攻击者明确推导的公理系统.因为在一个假设攻击者存在的情况下，对于任意协议的运行PCL完整的语义表明其公理和推导规则是正确的，这使得PCL证明简洁、易读.PCL已经分析并验证了许多重要的安全协议，如ISO-9798-3协议和STS协议族[14]、802.11i协议和TLS协议[17]、WAPI协议[18]、基于Diffie-Hellman协议[19]、基于NS(Needham-Schroeder, NS)协议[20]，使用PCL发现并改正一些协议中的安全缺陷.

在可证明组合安全方面：文献[14]利用PCL模型对ISO9798-3协议的密钥机密性和会话认证性进行了证明；文献[17]利用PCL模型找出了802.11i协议的缺陷，使用顺序组合证明方法证明了改进协议的安全属性；文献[20]利用PCL模型证明了NS协议族的安全属性.因此，设计的协议可证明安全，以验证其安全属性.

2) 认证及密钥交换.文献[21]基于DH困难假设提出了无线移动网络下的相互认证和密钥交换协议，该协议无安全性证明；文献[22]基于CDH假设提出了移动卫星通信系统认证密钥交换协议；文献[23]基于DDH假设提出了空间网络相互认证与密钥协商协议，提出了基于有证书的公钥系统模型；文献[24]基于CDH假设提出了基于身份的卫星通信认证及密钥交换协议；文献[25-26] 面向移动通信提出了基于群组的认证和密钥协商协议.

上述文献虽然面向无线移动网络或空间信息网提出了认证和密钥交换或协商协议，有一定的借鉴意义，但和前述空间信息网的特点相比，文献[21-24]一是没有考虑群组认证和密钥协议，二是没有考虑群组切换；文献[23-24]也没有考虑空间信息网的计算资源和通信能力以及认证效率等方面的因素；文献[25-26]未考虑群组切换、空间信息网的计算资源、通信能力等因素，另外基于Kerberos对称密码机制需要时钟同步，在SIN中很难实现.因此需要针对空间信息网的特点，设计高效、安全、群组多用户快速接入协议.

3) 安全切换.文献[27]依据地球同步轨道(geosynchronous earth orbit, GEO)卫星的特点，设计与地面管理中心(无线网络)进行垂直切换的决策方法，该方案未考虑安全性因素；文献[28]提出基于身份签名的快速认证方法，该方案对控制消息的机密性和完整性缺乏有效保护.文献[29]通过采用预认证和预配置的方法，提出了一种不与具体的移动性协议相关的快速切换框架，有效减少了切换延迟；文献[30]基于双线性配对函数提出了一个有效的安全切换方案，该方案未考虑群组安全切换.

上述文献讨论的安全切换方案，均未综合考虑前述SIN的特点.因此，需要一个能支持群组多用户快速安全切换的协议.

综上所述，本文根据空间信息网的特点提出支持群组多用户高效安全的认证协议.本文工作如下：

1) 基于对称密钥机制、密钥分层的思想面向空间信息网设计了支持群组高效、安全接入认证和切换协议-TSNP.

2) 使用PCL模型对各阶段协议进行形式化描述和安全性证明；对子协议组合并通过组合证明方法论证了组合后的协议具有密钥机密性和会话认证性.

3) 理论分析和实验结果显示TSNP协议减少了对地面管理中心的依赖程度，降低了卫星的计算和通信开销.

1 系统模型

1.1 系统模型

Fig. 1 System model.图1 系统模型

VariableDescriptionMGroundManagementCenterGUUsersofGroupSA,SBSatelliteGKSharedKeyofMandGUMSA,MSBSharedKeyofMandSatelliteukiKeyofGroupUserGMKMasterSessionKeyofGUandSatelliteUMKMasterSessionKeyofUserGroupandSatelliteGSKTemporarySessionKeyofGUandSatelliteUSKTemporarySessionKeyofUserGroupandSatelliteGIDIdentityofGroupMIDIdentityofMuidiIdentityofFirstCommunicationinGUrmGeneratedRandomNumberbyMrg,r'gGeneratedRandomNumberbyuidirSA,rSBGeneratedRandomNumberbySatellitePRF(·)PseudoRandomOperationHASH(·)HASHOperationMAC(·)MACiscomputedusingaHashfunctionEK(·)EncryptionOperationbyKey

1.2 敌手模型

1) 地面管理中心M是可信的，它与群组用户GU、卫星SA,SB共享的长期密钥不会泄露.

2) 信道被攻击者控制，整个网络通信环境是不可信的，攻击者可以对数据流进行修改或伪造数据.

3) 假设攻击者不能攻破底层的密码算法(PRF,HASH、分组加密算法)而获取相关密钥.

4) 假设攻击者不能攻陷地面管理中心M和卫星SA,SB.

1.3 安全目标

1) 认证性.系统模型中节点之间能够相互认证通信双方节点身份以防止攻击者进行仿冒或伪装攻击.

3) 顺序组合安全性.接入认证阶段子协议进行顺序组合后，能够确保组合后协议的安全属性，即满足组合后协议的密钥机密性和会话认证性.

4) 并行组合安全性.群组内用户产生各自的密钥被并行组合后，仍能够保证协议的安全属性，即群组内用户各自执行协议动作，相互并行操作不影响整个协议安全属性.

2 协议方案

2.1 认证协议

认证协议分为初始化阶段、接入认证阶段、群组成员密钥生成阶段.

1) 初始化阶段

地面管理中心M通过安全信道收集每个成员身份标识及密钥等信息，并进行存储.M与群组成员和卫星共享长期密钥(GK,uki,MSA,MSB).群组由若干个成员构成，每个成员的身份由GID和UID确定，每个成员都拥有对密钥(GK,UK),GK为组密钥，UK为成员密钥.初始化阶段完成后，地面管理中心M拥有群组中每个组成员的身份标识UID、组标识GID和每个成员的对密钥(GK,UK)以及与卫星共享的长期密钥MSA,MSB.M收集的相关信息用GP表示，GP={MID,GID,UID}.

2) 接入认证阶段

图2描述了TSNP认证协议接入认证阶段的过程，整个过程包括主会话密钥生成(记为TSNP.MKP)和临时会话密钥生成阶段(记为TSNP.SKP)，主会话密钥生成阶段负责生成GMK,umki，临时会话密钥生成阶段负责生成GSK,uski.密钥生成主要使用伪随机函数，计算公式如表2所示.

在消息传输过程中使用MAC来确保消息完整性，计算公式如表3所示.

主密钥生成步骤如下：

② 卫星SA收到Message1后，将Message2发送给地面管理中心M,其中Message2=(rg,GID,uidi,SIDA).

Fig. 2 Access authentication process of .图接入SA认证流程

GMKumkiuskiGSKPRF(GK‖rm‖MID‖rg‖GID‖SIDA)PRF(GMK‖uidi‖uki‖rg‖rm‖SIDA‖MID‖GID)PRF(umki‖rSA‖SIDA‖r'g‖uidi‖GID)PRF(GMK‖rSA‖r'g‖SIDA‖GID)

Table 3 Calculating Formula of MAC

③ 地面管理中心M收到Message2后，产生随机数rm，依次生成GMK,UMK.地面管理中心M计算MAC1并将Message3发送给卫星SA，其中Message3=(rm,MID,GID,uidi,SIDA,MAC1).

⑥ 卫星SA接收Message4，将其转发给地面管理中心M.

⑧ 卫星SA接收Message5，解密消息并存储.

临时密钥生成步骤如下：

3) 群组成员密钥生成阶段(记为TSNP.QKP)

Table 4 Calculating formula of MAC and Key

Fig..图向群组成员发送消息

2.2 切换协议

中Message9=(r″g,GID,uidi,SIDA,MAC9),Message10=(rSB,SIDB,SIDA,MAC10,MAC11),Message11=(r″g,SIDB,SIDA,MAC12,MAC13).

Fig. 4 Handoff process of TSNP.图4 TSNP切换

1) 主密钥预置阶段

因为空间信息网中卫星的位置可以预判，所以当卫星SA解密消息EMSA{GP,GMK,UMK}后，通过安全信道发送给卫星SB，这样卫星SB就拥有和群组用户GU通信会话主密钥.

2) 临时密钥生成阶段

此阶段临时密钥的生成与4.1节中临时密钥生成阶段的方式相同，此处不再赘述.

2.3 密钥层次

Fig. 5 Key Hierarchy.图5 密钥层次

1)GK,uki为长期共享密钥，在此层次中为底层密钥，在认证协议初始化阶段产生，它们负责导出其他层次密钥.

2)GMK,umki为主会话密钥，在TSNP协议主会话密钥阶段(MKP)生成，其中GMK由GK导出，umki由GMK和uki导出.

3)GSK,uski为临时会话密钥，在TSNP协议临时会话密钥阶段(SKP)生成，其中GSK由GMK导出，uski由umki导出.

4)GMK,GSK负责加密通信双方或群组成员的广播消息.umki,uski负责加密通信双方的消息.此外GMK,UMK还用于群组切换.

3 安全性及组合证明

TSNP协议方案包括认证和安全切换2个协议，2个协议又分成了不同的阶段执行相关操作以生成主会话密钥和临时会话密钥，由于安全切换协议与认证协议中的临时会话密钥阶段、群组内成员密钥生成阶段类似，因此本节将给出TSNP协议MKP,SKP,QKP三个阶段的形式化描述、安全属性、不变量、安全证明等.本节使用PCL模型对协议的安全性及组合进行证明，PCL预备知识见附录A.

3.1 主密钥生成阶段(TSNP.MKP)

3.1.1 协议形式化描述

uidi),MAC1)(MAC1MACGK(rm,MID,rg,

SIDA,uidi),MAC2),MAC2MACumki(rm,rg,

(rm,rg,MID,GID,uidi,SIDA))

3.1.2 前提条件

3.1.3 安全属性

1) TSNP.MKP会话认证性

2) TSNP.MKP密钥机密性

由于篇幅有限及证明过程可参照定理2的证明.协议不变量描述见附录B.

3.2 临时会话密钥生成阶段(TSNP.SKP)

3.2.1 协议形式化描述

((GID,uidi,rSA,SIDA),MAC6,MAC7)〉]SA.

MAC6,MAC7))(MAC6

3.2.2 前提条件

3.2.3 安全属性

1) TSNP.SKP会话认证性

2) TSNP.SKP密钥机密性

3.3 群组内成员密钥生成阶段(TSNP.QKP)

3.3.1 协议形式化描述

以第j个成员为例，协议形式化描述如下：

(MAC8.

3.3.2 前提条件

3.3.3 安全属性

1) TSNP.QKP会话认证性

2) TSNP.QKP密钥机密性

Has(Z,umkj)∧Has(Z,uskj)∧Has(Z,GSK))∧

协议不变量描述、证明过程与定理2类似，为节省篇幅，此处不再赘述.

3.4 组合TSNP协议

由于TSNP认证协议中的接入认证阶段由主会话密钥生成阶段、临时会话密钥生成阶段、群组内用户密钥生成阶段组成，3个阶段协议组合后，需要借助PCL顺序组合方法来保证组合后的协议满足密钥机密性和会话认证性，另外群组内用户密钥生成阶段需要使用并行组合方法以证明群组内用户各自执行协议而不影响其他用户协议的安全属性.

3.4.1 顺序组合

TSNP认证协议由TSNP.MKP,TSNP.SKP和TSNP.QKP协议顺序组合而成，TSNP认证协议的证明使用PCL中顺序组合证明方法.

φTSNP.MKP=φTSNP.MKP,auth∧φTSNP.MKP,sec,

φTSNP.SKP=φTSNP.SKP,auth∧φTSNP.SKP,sec,

φTSNP.QKP=φTSNP.QKP,auth∧φTSNP.QKP,sec.

证明. TSNP认证协议顺序组合的安全性证明有5个步骤：

1) 由3个阶段的安全性证明可得，TSNP.MKP,TSNP.SKP和TSNP.QKP可以满足协议安全属性：

φTSNP.QKP,sec.

2) 在更弱的前提假设下，协议安全属性依然可以得到保证，即：

3) 由于φTSNP.MKP的后置条件满足φTSNP.SKP的前提条件，同时φTSNP.SKP的前提条件满足φTSNP.QKP的后置条件，即φTSNP.MKP⊃θTSNP.SKP,θTSNP.SKP⊃φTSNP.QKP,所以应用顺序规则S1进行顺序组合.

4) 不变量ΓTSNP.MKP∪ΓTSNP.SKP∪ΓTSNP.QKP对于TSNP.MKP,TSNP.SKP和TSNP.QKP均成立，即：

5) 上述步骤说明TSNP.MKP,TSNP.SKP和TSNP.QKP的安全性在顺序组合后仍然可以保证，即

φTSNP.SKP.auth∧φTSNP.SKP,sec.

证毕.

3.4.2 并行组合

假设TSNP.QKPm,TSNP.QKPn(m,n≠i)是TSNP.QKP阶段任意2个子协议，子协议并行组合是2个协议线索并集.在并行组合下，为了保证每个协议安全属性被保留，因此要充分验证每个协议所代表的不变量.

证明. TSNP.QKP阶段任意2个子协议的并行组合安全性证明如下：

1) 证明TSNP.QKPm,TSNP.QKPn各自的安全属性

2) 确定证明中所使用不变量的集合ΓTSNP.QKPm,1∧ΓTSNP.QKPm,2和ΓTSNP.QKPn,1∧ΓTSNP.QKPn,2，从先前的步骤证明可以分解成2个部分:①使用诚实规则证明协议不变量;②不使用诚实规则，使用不变量作为假设证明协议的安全属性.

φTSNP.QKPm.auth∧φTSNP.QKPm,sec,

φTSNP.QKPn,sec.

3) 在更弱的前提下(子协议不变量的并集)，协议安全属性仍能够得到保证.

φTSNP.QKPm.auth∧φTSNP.QKPm,sec,

φTSNP.QKPn.auth∧φTSNP.QKPn,sec.

4)TSNP.QKPm,TSNP.QKPn不变量的并集能够持有2个协议:

φTSNP.QKPm.auth∧φTSNP.QKPm,sec,

φTSNP.QKPn.auth∧φTSNP.QKPn,sec.

证毕.

协议各阶段安全性证明、顺序组合及并行组合证明，说明TSNP协议已实现协议设计安全目标，即子协议密钥的机密性和会话的认证性，通过组合证明，得出TSNP协议具有密钥机密性和会话认证性.

3.5 进一步安全性分析

除了上述的基于PCL证明之外，结合图2对本文所提群组接入认证协议的安全属性进一步分析与说明.

1) 重放攻击

在TSNP中，随机数的使用可以有效地阻止重放攻击，协议中的每个阶段都有随机数的产生，如rg，rm，rSA等，重新使用之前的随机数不能产生有效的密钥.

2) 窃听

敌手可能在通信过程中窃听消息，从而删除或篡改消息.在TSNP中，参与通信双方的身份标识由地面管理中心统一控制，另外由于引入了MAC机制，因为TSNP可以抵抗窃听.

3) 中间人攻击

TSNP可以有效抵抗中间人攻击，敌手不能收集到真实的密钥信息，由于MAC机制存在，如果不能和地面管理中心产生的MAC值一致，则无法进行通信.

4) 前向攻击

在TSNP中，如果敌手获取了申请通信方目前的会话消息，但是之前的会话消息敌手无法获取.因为在会话中有新随机数的产生以及MAC校验，所以之前的秘密消息是不能被泄露的，因此TSNP具有前向安全性.

4 性能分析

Table 5 Two Protocols Comparison of the Computation and Communication of Overhead

实验对上述2个协议卫星SA的计算时延进行了对比，如图6所示.实验时，在单机上测试协议的计算时延，而不考虑发送消息时的传输时延.本机的硬件环境：CPU为i5，内存为4GB；软件环境：系统是Win7，测试语言是C++.

从表5和图6可以看出，与当前主流无线安全接入认证协议相比，在用户规模相同的前提下，TSNP协议的通信和计算效率具有优势，具体分析如下：

2) 计算量.考虑到SA计算资源受限，TSNP协议将计算量交由群内用户和卫星共同完成，希望通过降低卫星端的计算开销，提高TSNP协议的整体性能.由图6可知，当用户规模逐渐增大时，协议TSNP的计算时延明显小于协议IEEE80.211i+；表5表明，TSNP协议在SA和GU端的计算负载要明显低于IEEE802.11i+.

因此，TSNP有效降低了卫星的计算和通信开销，同时减少了对地面管理中心的依赖程度.

Fig. 6 The comparison of the computation delay.图6 2个协议SA计算时延对比

5 总 结

本文面向空间信息网提出了支持群组高效和安全的认证协议-TSNP.

在认证协议中又将协议分为3个阶段：1)初始化阶段地面管理中心分别与卫星和群组的用户共享长期密钥，并收集了群组中用户的相关信息GP；2)在接入认证阶段群组中的首个申请接入卫星的用户，经过相关操作后，地面管理中心和用户分别生成了会话主密钥，并由地面管理中心将其产生的会话主密钥和GP加密发送给卫星；此时卫星解密消息，并与刚才申请接入的用户进行通信，各自产生临时会话密钥；3)在群组密钥生成阶段，由第1个认证通过的用户向群组中其他用户发送消息，以便群组内用户各自生成相关密钥.在切换协议中，仅仅与卫星通过3次交互即可实现群组切换.

在PCL安全模型中分别证明了各个阶段协议的密钥机密性和会话认证性，通过顺序组合和并行组合的组合证明方法证明了组合后的协议依然满足密钥机密性和会话认证性，同时协议也确保了消息的完整性.分析结果表明：使用TSNP在空间信息网中实现群组认证和切换是高效和安全的.

[1]Mukherjee J, Ramamurthy B. Communication technologies and architectures for space network and interplanetary internet[J]. IEEE Communications Surveys & Tutorials, 2013, 15(2): 881-897

[2]Jiang Wei, Hao Huicheng, Li Yijun. Review of task scheduling research for the earth observing satellites[J]. Systems Engineering and Electronics, 2013, 35(9): 1878-1885 (in Chinese)(姜维, 郝会城, 李一军. 对地观测卫星任务规划问题研究述评[J]. 系统工程与电子技术, 2013, 35(9): 1878-1885)

[3]Wang C, Li D, Zhou X, et al. HJ satellite based mapping technologies of land use products for emergency response of agricultural disasters[C] //Proc of the 23rd Int Conf on Geoinformatics. Piscataway, NJ: IEEE, 2015: 1-4

[4]Wooster M J, Smith T, Drake N A. Key Methods in Geography[M]. London: SAGE Publications, 2016: 423

[5]Uchida N, Sato G, Takahata K, et al. Optimal route selection method with satellite system for cognitive wireless network in disaster information network[C] //Proc of the 25th Int Conf on Advanced Information Networking and Applications . Piscataway, NJ: IEEE, 2011: 23-29

[6]Wolff R, Preusche C, Gerndt A. A modular architecture for an interactive real-time simulation and training environment for satellite on-orbit servicing[J]. Journal of Simulation, 2014, 8(1): 50-63

[7]Hilland D H, Phipps G S, Jingle C M, et al. Satellite threat warning and attack reporting[C] //Proc of IEEE AeroConf’98. Piscataway, NJ: IEEE, 1998: 207-217

[8]Jiang C, Wang X, Wang J, et al. Security in space information networks[J]. IEEE Communications Magazine, 2015, 53(8): 82-88

[9]Ahmed A, Boulahia L M, Gaiti D. Enabling vertical handover decisions in heterogeneous wireless networks: A state-of-the-art and a classification[J]. IEEE Communications Surveys & Tutorials, 2014, 16(2): 776-811

[10]Farserotu J, Prasad R. A survey of future broadband multimedia satellite systems, issues and trends[J]. IEEE Communications Magazine, 2000, 38(6): 128-133

[11]Kota S L. Broadband satellite networks: Trends and challenges[C] //Proc of IEEE WCNC’05. Piscataway, NJ: IEEE, 2005: 1472-1478

[12]Liang L, Iyengar S, Cruickshank H, et al. Security for flute over satellite networks[C] //Proc of IEEE CMC’09. Piscataway, NJ: IEEE, 2009: 485-491

[13]Cruickshank H, Mort R, Berioli M. Broadband satellite multimedia (BSM) security architecture and interworking with performance enhancing proxies[C] //Proc of the 1st Int Conf on Personal Satellite Services. Berlin: Springer, 2009: 132-142

[14]Datta A. Security analysis of network protocols compositional reasoning and complexity-theoretic foundations[D]. Palo Alto, California: Standford University, 2005

[15]Datta A, Derek A, Mitchell JC, et al. Protocol composition logic (PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007, 172: 311-358

[16]Canetti R. Security and composition of multiparty cryptographic protocols[J]. Journal of Cryptology, 2000, 13(1): 143-202

[17]He C, Sundararajan M, Datta A, et al. A modular correctness proof of IEEE 802.11i and TLS[C] //Proc of the 12th ACM Conf on Computer and Communications Security. New York: ACM, 2005: 2-15

[18]Tie Manxia, Li Jiandong, Huang Zhenhai, et al. A correctness proof of WAPI certificate authentication protocol[C] //Proc of the 3rd Int Conf on Wireless Communications, Networking and Mobile Computing. Piscataway, NJ: IEEE, 2007: 2310-2313

[19]Roy A, Datta A, Mitchell J C. Formal proofs of cryptographic security of Diffie-Hellman-based protocols[C] //Proc of the 3rd Symp on Trustworthy Global Computing. Berlin: Springer, 2007: 312-329

[20]Zhang J, Ma J, Yang C. Protocol derivation system for the Needham-Schroeder family[J]. Security and Communication Networks, 2015, 8(16): 2687-2703

[21]Jiang Y, Lin C, Shen X, et al. Mutual authentication and key exchange protocols for roaming services in wireless mobile networks[J]. IEEE Trans on Wireless Communications, 2006, 5(9): 2569-2577

[22]Feng Tao, Ma Jianfeng. The universally composable security authentication and key exchange protocol for mobile satellite communication systems[J]. Journal of Astronautics, 2008, 29(6): 1959-1964 (in Chinese)(冯涛, 马建峰. UC 安全的移动卫星通信系统认证密钥交换协议[J]. 宇航学报, 2008, 29(6): 1959-1964)

[23]Guo Yuanbo, Wang Chao, Wang Liangmin. Universally composable authentication and key exchange protocol for access control in spatial information networks[J]. ACTA Electronica Sinica, 2010, 38(10): 2358-2364 (in Chinese)(郭渊博, 王超, 王良民. UC 安全的空间网络双向认证与密钥协商协议[J]. 电子学报, 2010, 38(10): 2358-2364)

[24]Zhong Yantao,Ma Jianfeng. A highly secure identity-based authenticated key-exchange protocol for satellite communication[J]. Journal of Communications and Networks, 2010, 12(6): 592-599

[25]Chen Y W, Wang J T, Chi K H, et al. Group-based authentication and key agreement[J]. Wireless Personal Communications, 2012, 62(4): 965-979

[26]Lai C, Li H, Lu R, et al. SE-AKA: A secure and efficient group authentication and key agreement protocol for LTE networks[J]. Computer Networks, 2013, 57(17): 3492-3510

[27]Chowdhury P K, Atiquzzaman M, Ivancic W D. Handover schemes in satellite networks: State-of-the-art and future research directions[J]. IEEE Communications Surveys and Tutorials, 2006, 8(4): 2-14

[28]Nakhjiri M, Nakhjiri M. AAA and Network Security for Mobile Access: Radius, Diameter, EAP, PKI and IP Mobility[M]. New York: John Wiley & Sons, 2005

[29]Dutta A, Famolari D, Das S, et al. Media-independent pre-authentication supporting secure interdomain handover optimization[J]. IEEE Trans on Wireless Communications, 2008, 15(2): 55-64

[30]He D, Chen C, Chan S, et al. Secure and efficient handover authentication based on bilinear pairing functions[J]. IEEE Trans on Wireless Communications, 2012, 11(1): 48-53

[31]Roy A, Datta A, Derek A, et al. Secrecy analysis in protocol composition logic[M] //Proc of the 11th Asia Computing Science Conf, Secure Software and Related Issues. Berlin: Springer, 2006: 197-213

[32]Datta A, Franklin J, Garg D, et al. A logic of secure systems and its application to trusted computing[C] //Proc of the 30th IEEE Symp on Security and Privacy. Piscataway, NJ: IEEE, 2009: 221-236

Li Xuefeng, born in 1975. Associate professor at Qinghai Radio&Television University . Visiting scholar in the School of Cyber Engineering at Xidian University. His main research interests include cryptography and network security.

Zhang Junwei, born in 1982. Associate professor in the School of Cyber Engineering at Xidian University. His main research interests include cryptography and network security.

Ma Jianfeng, born in 1963. PhD, professor and PhD supervisor in the School of Cyber Engineering at Xidian University. His main research interests include computer system security, cryptography and network security.

Liu Hai, born in 1984. PhD candidate at Xidian University. His main research interests include rational cryptographic protocol, location-based privacy protection, and software defined network.

附录A PCL预备知识

1) 协议建模

2) 协议逻辑和证明系统

正文中文献[14-15]给出了PCL的逻辑语法和非正式描述的逻辑谓词.更多协议的证明使用形式化的公式θ[P]Xφ，这是公式的含义是从某一个状态开始公式为真θ，通过线程X执行动作P后，公式φ的生成状态也为真.公式θ和φ是关于时序行动某种认定或者是对于不同主体的数据是可进入的某种认定.θ用于声明认证性，φ用于声明机密性.协议组合逻辑PCL采用标准逻辑概念，提出认证属性是协议动作之间的时间匹配关系，只推理诚实主体的动作即可证明攻击下协议的安全性，并通过逻辑公理和模块化推理方法支持复杂安全协议的组合推理，可以用来证明安全协议的认证和机密性等安全属性.

证明系统扩展了一阶逻辑公理和证明规则以适应协议动作，时序推导和一种不变量规则的特殊形式(诚实准则).诚实准则是至关重要的，它用于合并一个角色与推断其他角色行动的事实.例如，如果A接收一个来自B发送的消息响应，诚实准则将“俘获”A的能力去使用B的属性来推导出B如何产生他自己的响应.总之，如果A假设B是诚实的，它将使用B的角色去推导出它的假设.

3) 组合证明方法

PCL模型提供了2类可组合证明的方法，分别是组合证明方法和抽象改进方法.本文使用组合证明方法，抽象改进方法参见正文中文献[14-15,31-32].

组合证明是关于子协议复合推导的一种方法，它首先分析组件的安全性，接着再将组件以不同的方式组合，最后分析组合后的协议中其原有组件的安全性是否被破坏.组合证明方法主要解决组合安全的2个基本问题:1)组合后协议组件的安全属性是累加的，即顺序组合；2)如果组合2种机制，他们各自服务的安全属性不能因为任何一方而降低要求，即并行组合.

附录B 不变量及定理2证明过程

1) TSNP.MKP不变量描述

uidi,SIDA),MAC2)}.

MID,GID,uidi,SIDA),MAC1)})),

((rg,MID,GID,uidi,SIDA),MAC2})),

SIDA),MAC2)})∧After(Receive(SA,

MID,GID,uidi,SIDA),MAC2)},Send(M,

2) TSNP.SKP不变量描述

SIDA,rSA),MAC6,MAC7)).

MAC6,MAC7))).

ΓTSNP.SKP=ΓTSNP.SKP,1∧ΓTSNP.SKP,2∧ΓTSNP.SKP,3.

3) 定理2证明过程

下面分别证明定理2会话认证性和密钥机密性.

当TSNP.SKP协议被执行，会话认证性能够按照以下步骤推导：

① 因为卫星SA是诚实的，因此它能够清楚的知道自己行动的顺序，例如分别匹配SendMessage6，ReceiveMessage7，SendMessage8，参见式(B1)；

② 因为卫星SA接收和验证Message7，在前一阶段必然有一个能够计算和发送Message7的实体，这也就隐含着这个实体一定知道uski，GSK被用于MAC，以保证消息完整性，参见式(B2),(B3)；

步骤1至步骤7的结果在证明，式(B21)中体现，因此以卫星为诚实角色能够推导出安全属性中的会话认证性.

根据PCL模型相关语法、规则和公理，TSNP.SKP协议会话认证性证明过程如下：

① 由AA1,ARP,AA4可得：

(B1)

② 由ARP,HASH3可得：

MAC4,

MAC5,

∃Z.Computes(Z,HASHuski(GID,uidi,SIDA,

(B2)

③ 由HASH1可得:

(B3)

④ 由HASH4可得：

(Has(Z,uski)∧Has(Z,GSK))≡

(B4)

⑤ 由式(B4),ΓTSNP.SKP,1可得：

MAC4,

MAC5,

(B5)

⑥ 由式(B5),HASH1,φTSNP.SKP.sec可得：

MAC4,

MAC5,

(B6)

⑦ 由AA1,ΓTSNP.SKP,2可得：

(B7)

⑧ 由式(B2),(B6),(B7)可得：

(B8)

⑨ 由式(B2),(B8)可得：

(B9)

⑩ 由式(B9),HON可得：

rSA,GID,SIDA,uidi,MAC3);

uidi,MAC4,MAC5);

(B10)

GID,SIDA,uidi,MAC6,MAC7),

MAC6,

MAC7⊃

(B11)

GID,SIDA,uidi)⊃Has(Z,uski)⊃

(B12)

(B13)

(B14)

(B15)

(B16)

(B17)

GID,SIDA,uidi)∧Send(Z,HASHumki(rSA,

(B18)

(B19)

(B20)

(B21)

当TSNP.SKP协议被执行，密钥机密性能够按照以下步骤推导：

① 某一实体(卫星或用户)如有参与双方的随机数，则根据CP1可以计算出相关密钥，在证明式(B22)中可见；

② 如果用户和卫星都是诚实的，则说明某一实体拥有随机数和密钥，而这个实体只能是卫星或用户，在证明式(B23)中可见；

③ 在证明式(B24)～(B28)，卫星按照顺序接收或发送消息，并且匹配消息，计算出自己所属的密钥；

步骤①至步骤④的结果在证明，式(B33)中体现，因此在TSNP.SKP协议中可以推导出其密钥机密性.

根据PCL模型相关语法、规则和公理，TSNP.SK协议会话机密性证明过程如下:

① 由CP1,ΓTSNP.SKP,2可得：

(B22)

② 由式(B22),ΓTSNP.SKP可得：

(B23)

③ 由ARP,REC可得：

MAC4,MAC5)]SA

(B24)

④ 由AA1,ORIG可得：

(B25)

⑤ 由式(B24),(B25)可得：

MAC5)]SAHas(SA,rSA)∧

(B26)

⑥ 由式(B26),CP1可得：

MAC5)]SACompute(SA,Hash(umki,

(B27)

⑦ 由ARP,CP3可得：

SIDA,MAC4,MAC5)⊃∃Z.(Compute(Z,

(B28)

⑧ 由式(B28)可得：

rSA,GID,uidi,SIDA)Compute(Z,Hash(GMK,

(B29)

⑨ 由式(B28),ΓTSNP.SKP可得：

(B30)

⑩ 由式(B28),(B29)可得：

(B31)

(B32)

(B33)

由(B21),(B33)可得TSNP.SKP协议具有会话认证性和密钥机密性，因此定理2得证.

TSNP: A Novel PCL-Secure and Efficient Group Authentication Protocol in Space Information Network

Li Xuefeng1,2, Zhang Junwei1, Ma Jianfeng1, and Liu Hai1

1(SchoolofCyberEngineering,XidianUniversity,Xi’an710071)2(EducationTechnologyCenter,QinghaiRadio&TelevisionUniversity,Xining810008)

In space information networks (SIN), to continuously collect information and enlarge the observation range, the group aircrafts need to fast access authenticate with the satellite. Unfortunately, the existing authentications schemes cannot be applied in SIN due to its particular characteristics, such as high dynamic topology, satellite computation and limited communication resources, etc. To this end, we propose a PCL (protocol composition logic) secure and efficient group authentication protocol named as TSNP through utilizing symmetric encryption and key hierarchy. With it, the authenticated node enables other users in this group to gain the session key and realize the secure group authentication and handover. Furthermore, we analyze its security properties in PCL mode and prove its composition security based on parallel and sequential rules. As a further contribution, the experimental results indicate that TSNP can reduce not only the dependence on group management center but also the satellite’s computation and communication overhead.

space information network(SIN); group authentication; protocol composition logic(PCL); authentication; secrecy

2016-06-16；

2016-08-18

国家“八六三”高技术研究发展计划基金项目(2015AA016007)；国家自然科学基金项目(U1405255，61472310,61372075)

TP309

This work was supported by the National High Technology Research and Development Program of China (863 Program) (2015AA016007) and the National Natural Science Foundation of China (U1405255,61472310,67372075).