无人机无线通信协议的形式化认证分析与验证

刘 栋，连晓峰，王宇龙，谭 励，赵宇琦，李 林

(1.北京工商大学 人工智能学院，北京 100048；2.中国兵器工业信息中心，北京 100089；3.北京工商大学 计算机学院，北京 100048)

0 引言

随着科学技术的不断发展，生产力不断进步，无人机的技术越来越成熟，无人机已经走进人们的日常生产和生活中。由于无人机具有成本较低，操作简单，灵活度高，适用于多种复杂环境等优点，故无人机广泛应用于环境探测[1]、货物运输[2]、应急救援[3]及个人航拍等领域。然而无人机在给我们的日常生产生活带来便利的同时，无人机通信方面可能会受到攻击者的攻击[4]，使无人机通讯信息遭到泄露，从而产生严重的安全问题[5]。

形式化方法[6]是一种以数学为基础，使系统设计各个步骤实现可靠性和正确性的方法，在协议设计方面的应用极大地提高了安全协议的可靠性。形式化方法主要分为逻辑推理[7]，模型检测[8]和定理证明[9]。模型检测可以自动检测要验证的系统是否满足要验证的属性，如果不满足要验证的属性，则会给出攻击流程图。模型检测具有完全自动化，检测速度快，自动显示攻击流程图等优点。

2002年Maggi等人[10]以N-S公钥协议为例，提出一种基于模型检测工具SPIN(Simple Promela Interpreter)的安全协议建模分析方法。2006年M.H.Xiao等人[11]提出了一种Promela建模的方法，并对Helsinki协议进行建模，发现了对此协议的攻击。2015年程道雷等人[12]对OAuth2.0协议进行分析，拓展了Maggi的方法，实现了多主体建模分析。2017年梅映天等人[13]对Maggi的方法进行改进，实现了四通道并行建模法，优化了模型复杂度。2019年Li Wei等人[14]提出一种抽象建模的方法，运用Maggi的方法对RCIA和RAPP两种协议进行分析，并提出了通用的UMAP模型。

2019年朱辉等人[15]提出了一种有控制站支持的无人机认证协议ASUSG(authentication scheme for UAV network supported by ground station)，该协议基于椭圆曲线密码体制[16]，控制站作为密钥的生成中心和分发中心，实现了无人机与控制站，无人机与无人机之间的身份认证，并且减少了无人机节点的计算开销。

本文以无人机无线通信协议为研究对象，在分析协议形式化认证过程的基础上，利用模型检测工具SPIN对协议进行建模分析，并验证协议的一致性。其中，在攻击者建模方面，提出一种改进的知识项获取方法，直接通过攻击者可以学会的知识项求取攻击者需要表示的知识项。

1 模型检测工具SPIN

SPIN[17]即Promela[18]语言解析器，用于检测有限状态系统与期望的性质是否相符合，其中期望的性质用线性时序逻辑LTL(linear temporary logic)[19]公式来表示。

1980年美国贝尔实验室开发了一个用于验证系统性质的工具Pan，1989年该工具起名为SPIN，之后工具支持C语言的嵌入，加入深度优先搜索算法等改进，使得SPIN的功能和应用进一步得到了加强。美国国家航天局曾经使用SPIN对火星探测器的软件系统进行验证，发现了软件系统的某些缺陷。

运用SPIN来分析与验证安全协议的优势为:1)SPIN的编程语言为Promela，功能强大，它可以更好的形式化描述安全协议的性质，并且可以检测出模型的语法，死锁和无效的循环等问题;2)SPIN可以对安全协议的认证性，一致性等众多性质进行验证，在模拟通信过程方面既可以描述异步通信，也可以描述同步通信;3)在出现违反性质情况后，SPIN会自动给出流程图，还会显示模型中设置的变量变化情况，利于操作人员分析其具体原因。

SPIN的验证过程如图1所示，协议通信流程用Promela进行建模，协议的性质根据规则转化成LTL公式，之后输入到模型检测工具SPIN进行语法检查，通过后进行自动验证，如果出现违反协议性质的情况，则会给出反例；如果无违反协议性质的情况，则验证成功。

图1 SPIN验证过程

2 无人机无线通信协议认证过程分析

无人机无线通信协议认证过程如图2所示，应用场景为多个无人机和地面控制站之间进行无线通信，以及各个无人机之间进行信息交换。其中，控制站具有较强的计算能力和存储资源；而无人机节点计算能力和存储资源较弱。为保证信息通信的安全性，通信双方需进行身份认证。在此，根据Dolev-Yao模型[20]，进行合理化假设：

1)该协议本身使用的加密算法没有漏洞，即攻击者无法利用密码算法的漏洞进行攻击。

2)经过密钥加密的消息，只有相应的解密密钥才可以解密。

3)攻击者可以参与到合法主体的会话中，即攻击者也拥有自己的密钥和随机数。

图2 无人机无线通信协议认证示意图

为分析方便，设置无人机无线通信协议中的相关变量符号如表1所示。

表1 无人机无线通信协议变量符号

根据协议的通信过程，相应的认证过程主要分为认证初始化、无人机节点与控制站之间身份认证、无人机节点之间身份认证3个阶段。

2.1 认证初始化阶段：

1)设定符合密码机制的椭圆曲线Ep(a,b)及其点群上阶次为q的生成元G(x,y)、合适的散列函数H、加密算法ENC和解密算法DEC，以及时间间隔ΔT。

2)控制站CS生成①CS公私钥对(Prcs,Pucs)：

(1)

②UAV节点(设为n个)公私钥对密钥表{Pruav(i),Puuav(i)|1≤i≤n}，其中，每个节点的公私钥对计算如下：

(2)

③CS向各个UAV节点发送的随机数RANDCS。

{RANDCS(i)∈[1,q-1],1≤i≤n}

(3)

由图3可知，G(x,y)为椭圆曲线Ep(a,b)上一点，所有私钥均为[1,q-1]区间内的随机数，而公钥均是位于椭圆曲线上的一点。

图3 网络模型中各节点公私钥生成示意图

3)UAV接收由CS发送的所有参数{Ep(a,b),q,G(x,y),H,ENC,DEC,ΔT,Prcs,Pucs,Pruav(i),Puuav(i),RANDcs(i)}，并保证自身系统时间与CS一致。

2.2 无人机节点与控制站身份认证阶段：

1)UAV请求CS认证：UAV由RANDuav和G(x,y)生成椭圆曲线上的一点(xt,yt)，并根据式(4)计算签名认证信息S1UAV和S2UAV,之后将元组信息{TUAV,S1UAV,S2UAV}发送给CS，即消息1(Msg1)，其中TUAV为当前系统时间。

(4)

Msg1:UAV→CS:TUAV,S1UAV,S2UAV

2)CS首先验证是否满足T-TUAV<△T以保证Msg1的新鲜性。若条件满足，则计算签名信息S1CS和S2CS，如式(5)所示，只有S2CS=S1UAV时UAV才能通过CS的认证；否则，认证失败。之后CS生成其与UAV的会话密钥KEYCU，随后CS向UAV发送{RANDCS+1}KEYCU,即消息2(Msg2)，并更新本地随机数RANDCS=RANDCS+1。

(5)

Msg2:CS→UAV:{RANDcs+1}KEYCU

3)UAV对CS进行认证。UAV同样需生成KEYCU,如式(6)所示，用该密钥解密Msg2，如果解密消息为RANDCS+1，则CS通过认证；否则认证失败。认证成功后UAV更新本地随机数RANDCS=RANDCS+1 。之后UAV和CS之间使用会话密钥KEYCU进行通信。

(6)

2.3 无人机节点间身份认证阶段

在此，设UAVi和UVAj两个无人机节点之间进行身份认证，具体过程如下：

1)UAVi生成随机数RANDij，其中RANDij∈[1,q-1]，之后通过UAVi和CS的会话密钥KEYCUi将随机数加密后发送给CS，即消息3(Msg3)。

Msg3:UAVi→CS:{RANDij}KEYCU(i)

2)CS解密后获得随机数RANDij，再通过UAVj和CS的会话密钥KEYCU(j)将得到的随机数加密后发送给UAVj，即消息4(Msg4)。

Msg4:CS→UAVj:{RANDij}KEYCU(j)

3)UAVi向UAVj发起认证请求。UAVi计算节点间会话密钥KEYij，如式(7)所示，其中Pruavi为UAVi的私钥，Puuavj为UAVj的公钥，并获取当前系统时间Ti，之后用该密钥加密{RANDij||Ti}发送给UAVj，即消息5(Msg5)。

(7)

(8)

Msg6:UAVj→UAVi:{RANDij+1||Tj}KEYij

3 无人机无线通信协议认证建模

为对该协议进行一致性认证，需通过线性时序逻辑LTL进行模型检测。具体包括以下3个部分。

3.1 定义协议安全属性

要进行模型检测，首先需利用线性时序逻辑LTL来表示无人机协议的安全属性，以便通过模型检测工具SPIN来自动检测模型是否满足安全属性，若不满足，则会给出反例。

模型的安全属性需要用原子谓词变量来进行表示，其中0代表事件为假，1代表事件为真，本文定义的原子谓词变量为：

bitstartUAVjCS=0;bitstartCSUAVj=0;

bitfinishUAVjCS=0;bitfinishUAViCS=0;

bitstartUAViCS=0;bitstartCSUAVi=0;

bitRANDj=1;bitRANDi=1;

其中startUAVjCS表示无人机UAVj向控制站CS发起会话，startUAVjCS=0表示无人机UAVj没有向控制站CS发起会话，当无人机UAVj向控制站CS发起会话则startUAVjCS=1,startCSUAVj表示控制站CS向无人机UAVj发起会话，finishUAVjCS表示无人机UAVj完成了与控制站CS的会话，其他原子谓词变量含义与之类似。RANDj=1表示UAVj收到CS发送的随机数与收到UAVi发送的随机数相等，RANDi=1表示UAVi收到UAVj发送的随机数比自己生成的随机数大1。

然后通过宏定义方式来更新原子谓词的值，例如定义update_RANDj(x,y)，当x与y的值不相等，则会使原子谓词变量RANDj的值变为0，类似如下：

#defineupdate_RANDj(x,y)if

∷(x!=y)->RANDj=0

∷elseskipfi

… …

根据定义好的原子谓词来构建LTL公式，其中，LTL公式中符号[]表示总是处于某个状态，符号!表示逻辑非，符号||表示逻辑或，符号U表示直到，符号&&代表逻辑与，例如x和y为原子命题，公式(！xUy)表示命题y为真之前命题x一直为假。无人机UAV与控制站CS认证性分析如下：

无人机UAVj与控制站CS的认证，需要控制站CS向发起方无人机UAVj发起会话之后，无人机UAVj结束了与应答方控制站CS的会话或者无人机UAVj一直没有结束与控制站CS的会话。LTL公式表示为：

[](([]!finishUAVjCS)||(!finishUAVjCSU

startCSUAVj))

同理无人机UAVi与控制站CS的认证用LTL公式表示为：

[](([]!finishUAViCS)||(!finishUAViCSU

startCSUAVi))

无人机UAV与控制站CS认证性需要同时满足这两条LTL公式，故完整的LTL公式为：

([](([]!finishUAVjCS)||(!finishUAVjCSU

startCSUAVj)))&

&([](([]!finishUAViCS)||(!finishUAViCSU

startCSUAVi)))

无人机UAVi与无人机UAVj认证性分析如下：无人机UAVj对无人机UAVi的认证为UAVj收到CS发送的随机数与收到UAVi发送的随机数相等。LTL公式表示为：

[]RANDj

无人机UAVi对无人机UAVj的认证为UAVi收到UAVj发送的随机数比自己生成的随机数大1。LTL公式表示为：

[]RANDi

无人机UAVi与无人机UAVj认证性需要同时满足这两条LTL公式，故完整的LTL公式为：

([]RANDj)&&([]RANDi)

3.2 诚实主体建模

无人机无线通信协议的诚实主体为无人机UAV和控制站CS，为反映无人机与控制站，以及无人机之间的相互认证过程，在此，设3个进程proctypePUAVj(),proctypePUAVi()和proctypePCS()。

首先，构建一个数据项的有限集合，对本文所使用的消息进行枚举：

mtype={UAVi,UAVj,CS,Att,R,Tuavj,Tuavi,Tj,Ti,

S1uavj,S2uavj,S1uavi,S2uavi,RANDcsj1,RANDcsi1,

RANDij,RANDij1,KEYcuj,KEYcui,KEYca,KEYij,gD}

上述数据项中Att表示攻击者，R表示未知的主体，KEYca为控制站CS与攻击者Att的会话密钥，gD表示攻击者产生的随机数信息。

其次根据无人机认证协议中传输消息的数目和传输目的不同，故需要用6个通道来模拟数据项的传输，如图4所示。

图4 传输通道示意图

其中：c1,c2通道分别用于传输UAVj和CS认证信息Msg1,Msg2，c3,c4通道分别用于传输UAVi和CS认证信息Msg1,Msg2，c5通道用于传输Msg3和Msg4，c6通道用于传输Msg5和Msg6。每个通道所定义的元素比要传输的元素多两项，因为每个通道第一项表示消息的发送者，最后一项表示消息的接收者，例如：

c1!UAVj,Tuavj,S1uavj,S2uavj,CS;

表示消息发送者UAVj通过通道c1向消息接收者CS发送信息TUAVj,S1UAVj,S2UAVj。

3.3 攻击者建模

攻击者建模遵循Dolev-Yao攻击者模型的攻击能力，攻击者可以窃听、截获、存储、重放接收到的信息，并可以利用得到的知识项进行消息的重组、转发。

3.3.1 攻击者需要表示的知识项的获取

首先求解攻击者可以学会的知识项，攻击者可以学会的知识项是由攻击者通过截获诚实主体发送的信息，对未加密的信息直接存储，能解密的信息解密后进行存储，不能解密的信息整条进行存储。

例如无人机UAVj向控制站CS发送认证消息{TUAVj,S1UAVj,S2UAVj}，此消息属于未加密的信息，则攻击者可以学会的知识项为TUAVj,S1UAVj和S2UAVj。而控制站CS向无人机UAVj发送认证消息{RANDCSj+1}KEYCU(j)，此消息属于加密消息，但攻击者无解密密钥KEYCU(j)，故攻击者对整条消息进行存储，可学会的知识项为{RANDCSj+1}KEYCU(j)。

故攻击者可学会的知识项如表2所示。

表2 攻击者可学会的知识项

其次通过设立的接收语句来判断每一条攻击者可以学会知识项是否可以构成诚实主体能接收的消息，如果能，则为攻击者需要表示的知识项；否则不是攻击者需要表示的知识项。设立的接收语句如下：

c1?eval(party1),g1,g2,g3,eval(self);

c2?eval(self),eval(RANDcsj1),eval(KEYcuj),eval(self);

c3?eval(party2),g4,g5,g6,eval(self);

c4?eval(self),eval(RANDcsi1),eval(KEYcui),eval(self);

c5?eval(self),g7,g8,eval(self);

c5?eval(self),g9,eval(KEYcuj),eval(self);

c6?eval(party2),g10,g11,eval(KEYij),eval(self);

c6?eval(party2),g12,g13,eval(KEYij),eval(self);

其中，eval函数的作用是判断接收值与期望值是否相同，依次从左到右进行判断，如果相同则接收数据项；否则只要有一项数据项不相同则拒绝接收整条消息。变量self，party1和party2取值为消息的发送者或接收者。符号?表示消息的接收。例如无人机UAVj向控制站CS发送认证消息Msg1，对于接收者CS来说，接收到的信息都不是由它自己生成的，不能直接确定接收到的信息，对于不能确定的信息用变量来表示，即g1,g2和g3。而控制站CS向无人机UAVj发送认证消息Msg2，对于接收者UAVj来说，信息RANDcsj1，KEYcuj在协议的初始化阶段控制站CS和无人机UAVj就已经协商好，接收者UAVj可以确定这些信息，故直接用eval函数来判断。

接收者不能确定的数据项用g(1-13)变量表示，g8变量的取值范围{KEYcuj,KEYcui,KEYca}，其他变量取值范围为{Tuavj,Tuavi,Tj,Ti,S1uavj,S2uavj,S1uavi,S2uavi,RANDcsj1,RANDcsi1,RANDij,gD,RANDij1}。例如攻击者可学会的知识项TUAVj，它可以构成{TUAVj,TUAVj,TUAVj}使得接收语句c1?eval(party1),g1,g2,g3,eval(self);接收，故TUAVj是攻击者需要表示的知识项。

根据分析得出攻击者需要表示的知识项，如下所示：

TUAVj,S1UAVj,S2UAVj,TUAVi,S1UAVi,S2UAVi

{RANDCSj+1}KEYCU(j),{RANDCSi+1}KEYCU(i)

{RANDij}KEYCU(i),{RANDij}KEYCU(j)

{RANDij||Ti}KEYij,{RANDij+1||Tj}KEYij

3.3.2 攻击者行为建模

攻击者行为建模包括知识项的表示，知识项的截取和学习，消息的构建与转发3个部分。

知识项的表示：例如定义bitk_Tuavj=0;来表示攻击者TUAVj知识项，其中初始值为0表示攻击者还未学会此条知识项，若值变为1表示攻击者已学会。

知识项的截取和学习：攻击者可以截取知识项并对截取的知识项进行学习。例如c1?_,x1,x2,x3,_;表示攻击者可以通过c1通道来截获通讯主体间的信息，下划线_表示攻击者不需要判断发送者和接收者是谁，直接获取知识项。

消息的构建与转发：攻击者可以根据自己已经学会的知识项进行消息构建并转发。例如：c1!((k_Tuavj&&k_S1uavj&&k_S2uavj)->CS:R),Tuavj,S1uavj,S2uavj,CS。

表示攻击者如果分别学会TUAVj,S1UAVj,S2UAVj，则会通过c1通道将消息TUAVj,S1UAVj,S2UAVj发送给CS，否则消息发送给未知的主体R。

4 实验结果与分析

在Windows 10 64位系统SPIN6.5.1，iSPIN1.1.4的模拟环境下进行仿真实验，最终验证出无人机无线通信协议的攻击漏洞。

验证无人机UAV与控制站CS认证性时，攻击者攻击流程如图5所示。

图5 攻击者攻击流程

此过程破坏了无人机UAVj对控制站CS的认证性。首先UAVj向CS发送TUAVj,S1UAVj,S2UAVj，CS对UAVj认证通过后向UAVj发送{RANDCSj+1}KEYCU(j)，但是此过程被攻击者Att截获，随后冒充CS给UAVj发送{RANDCSj+1}KEYCU(j)，导致UAVj误认为发送者Att的身份是CS，使无人机UAVj对控制站CS的认证遭到了破坏具体攻击过程如下：

(1)UAVj→CS:TUAVj,S1UAVj,S2UAVj

(2)CS→Att:{RANDCSj+1}KEYCU(j)

(3)Att→UAVj:{RANDCSj+1}KEYCU(j)

此过程还破坏了无人机UAVi对控制站CS的认证性。首先UAVi向CS发送TUAVi,S1UAVi,S2UAVi，CS对UAVi认证通过后向UAVi发送{RANDCSi+1}KEYCU(i)，但是此过程被攻击者Att截获，随后冒充CS给UAVi发送{RANDCSi+1}KEYCU(i)，导致UAVi误认为发送者Att的身份是CS，使无人机UAVi对控制站CS的认证遭到了破坏，具体攻击过程如下：

(1)UAVi→CS:TUAVi,S1UAVi,S2UAVi

(2)CS→Att:{RANDCSi+1}KEYCU(i)

(3)Att→UAVi:{RANDCSi+1}KEYCU(i)

验证无人机UAVi与无人机UAVj认证性时，攻击者攻击流程如图6所示。

图6 攻击者攻击流程

经过分析得到下列攻击过程：

(1)UAVj→CS:TUAVj,S1UAVj,S2UAVj

(2)CS→Att:{RANDCSj+1}KEYCU(j)

(3)Att→UAVj:{RANDCSj+1}KEYCU(j)

(4)UAVi→CS:TUAVi,S1UAVi,S2UAVi

(5)CS→Att:{RANDCSi+1}KEYCU(i)

(6)Att→UAVi:{RANDCSi+1}KEYCU(i)

(7)UAVi→Att:{RANDij}KEYCU(i)

(8)Att→CS:{gD}KEYCA

(9)CS→Att:{gD}KEYCU(j)

(10)Att→UAVj:{gD}KEYCU(j)

(11)UAVi→UAVj:{RANDij||Ti}KEYij

如图7为验证无人机之间认证结果相关信息，检测结果显示State-vector(状态向量)所需内存为120字节，depth reached(搜索深度)为40层,errors(错误项)的值为1，states,stored(状态存储数)值为16，transitions(状态迁移数)值为16。State-vector，depth reached，states,stored，transitions四个值越小，表示建立的模型越好，验证的速度越快，越不容易出现状态空间爆炸的情况。

图7 验证结果相关信息

5 结束语

本文主要针对无人机无线通信协议进行身份认证与一致性验证，提出一种改进的攻击者获取知识方法，可直接通过攻击者可学会的知识项来求取攻击者需要表示的知识项，使分析复杂协议的过程更加简单，并运用模型检测工具SPIN对控制站CS，无人机UAV，攻击者H三者进行建模，检测出攻击者攻击流程，结果表明此认证协议并不安全，故下一步的工作是针对此攻击者漏洞来对无人机认证协议进行改进和验证，来使其安全性更高。