無(wú)人機(jī)無(wú)線通信協(xié)議的形式化認(rèn)證分析與驗(yàn)證

劉 棟，連曉峰，王宇龍，譚 勵(lì)，趙宇琦，李 林

(1.北京工商大學(xué) 人工智能學(xué)院，北京 100048；2.中國(guó)兵器工業(yè)信息中心，北京 100089；3.北京工商大學(xué) 計(jì)算機(jī)學(xué)院，北京 100048)

0 引言

隨著科學(xué)技術(shù)的不斷發(fā)展，生產(chǎn)力不斷進(jìn)步，無(wú)人機(jī)的技術(shù)越來(lái)越成熟，無(wú)人機(jī)已經(jīng)走進(jìn)人們的日常生產(chǎn)和生活中。由于無(wú)人機(jī)具有成本較低，操作簡(jiǎn)單，靈活度高，適用于多種復(fù)雜環(huán)境等優(yōu)點(diǎn)，故無(wú)人機(jī)廣泛應(yīng)用于環(huán)境探測(cè)[1]、貨物運(yùn)輸[2]、應(yīng)急救援[3]及個(gè)人航拍等領(lǐng)域。然而無(wú)人機(jī)在給我們的日常生產(chǎn)生活帶來(lái)便利的同時(shí)，無(wú)人機(jī)通信方面可能會(huì)受到攻擊者的攻擊[4]，使無(wú)人機(jī)通訊信息遭到泄露，從而產(chǎn)生嚴(yán)重的安全問題[5]。

形式化方法[6]是一種以數(shù)學(xué)為基礎(chǔ)，使系統(tǒng)設(shè)計(jì)各個(gè)步驟實(shí)現(xiàn)可靠性和正確性的方法，在協(xié)議設(shè)計(jì)方面的應(yīng)用極大地提高了安全協(xié)議的可靠性。形式化方法主要分為邏輯推理[7]，模型檢測(cè)[8]和定理證明[9]。模型檢測(cè)可以自動(dòng)檢測(cè)要驗(yàn)證的系統(tǒng)是否滿足要驗(yàn)證的屬性，如果不滿足要驗(yàn)證的屬性，則會(huì)給出攻擊流程圖。模型檢測(cè)具有完全自動(dòng)化，檢測(cè)速度快，自動(dòng)顯示攻擊流程圖等優(yōu)點(diǎn)。

2002年Maggi等人[10]以N-S公鑰協(xié)議為例，提出一種基于模型檢測(cè)工具SPIN(Simple Promela Interpreter)的安全協(xié)議建模分析方法。2006年M.H.Xiao等人[11]提出了一種Promela建模的方法，并對(duì)Helsinki協(xié)議進(jìn)行建模，發(fā)現(xiàn)了對(duì)此協(xié)議的攻擊。2015年程道雷等人[12]對(duì)OAuth2.0協(xié)議進(jìn)行分析，拓展了Maggi的方法，實(shí)現(xiàn)了多主體建模分析。2017年梅映天等人[13]對(duì)Maggi的方法進(jìn)行改進(jìn)，實(shí)現(xiàn)了四通道并行建模法，優(yōu)化了模型復(fù)雜度。2019年Li Wei等人[14]提出一種抽象建模的方法，運(yùn)用Maggi的方法對(duì)RCIA和RAPP兩種協(xié)議進(jìn)行分析，并提出了通用的UMAP模型。

2019年朱輝等人[15]提出了一種有控制站支持的無(wú)人機(jī)認(rèn)證協(xié)議ASUSG(authentication scheme for UAV network supported by ground station)，該協(xié)議基于橢圓曲線密碼體制[16]，控制站作為密鑰的生成中心和分發(fā)中心，實(shí)現(xiàn)了無(wú)人機(jī)與控制站，無(wú)人機(jī)與無(wú)人機(jī)之間的身份認(rèn)證，并且減少了無(wú)人機(jī)節(jié)點(diǎn)的計(jì)算開銷。

本文以無(wú)人機(jī)無(wú)線通信協(xié)議為研究對(duì)象，在分析協(xié)議形式化認(rèn)證過程的基礎(chǔ)上，利用模型檢測(cè)工具SPIN對(duì)協(xié)議進(jìn)行建模分析，并驗(yàn)證協(xié)議的一致性。其中，在攻擊者建模方面，提出一種改進(jìn)的知識(shí)項(xiàng)獲取方法，直接通過攻擊者可以學(xué)會(huì)的知識(shí)項(xiàng)求取攻擊者需要表示的知識(shí)項(xiàng)。

1 模型檢測(cè)工具SPIN

SPIN[17]即Promela[18]語(yǔ)言解析器，用于檢測(cè)有限狀態(tài)系統(tǒng)與期望的性質(zhì)是否相符合，其中期望的性質(zhì)用線性時(shí)序邏輯LTL(linear temporary logic)[19]公式來(lái)表示。

1980年美國(guó)貝爾實(shí)驗(yàn)室開發(fā)了一個(gè)用于驗(yàn)證系統(tǒng)性質(zhì)的工具Pan，1989年該工具起名為SPIN，之后工具支持C語(yǔ)言的嵌入，加入深度優(yōu)先搜索算法等改進(jìn)，使得SPIN的功能和應(yīng)用進(jìn)一步得到了加強(qiáng)。美國(guó)國(guó)家航天局曾經(jīng)使用SPIN對(duì)火星探測(cè)器的軟件系統(tǒng)進(jìn)行驗(yàn)證，發(fā)現(xiàn)了軟件系統(tǒng)的某些缺陷。

運(yùn)用SPIN來(lái)分析與驗(yàn)證安全協(xié)議的優(yōu)勢(shì)為:1)SPIN的編程語(yǔ)言為Promela，功能強(qiáng)大，它可以更好的形式化描述安全協(xié)議的性質(zhì)，并且可以檢測(cè)出模型的語(yǔ)法，死鎖和無(wú)效的循環(huán)等問題;2)SPIN可以對(duì)安全協(xié)議的認(rèn)證性，一致性等眾多性質(zhì)進(jìn)行驗(yàn)證，在模擬通信過程方面既可以描述異步通信，也可以描述同步通信;3)在出現(xiàn)違反性質(zhì)情況后，SPIN會(huì)自動(dòng)給出流程圖，還會(huì)顯示模型中設(shè)置的變量變化情況，利于操作人員分析其具體原因。

SPIN的驗(yàn)證過程如圖1所示，協(xié)議通信流程用Promela進(jìn)行建模，協(xié)議的性質(zhì)根據(jù)規(guī)則轉(zhuǎn)化成LTL公式，之后輸入到模型檢測(cè)工具SPIN進(jìn)行語(yǔ)法檢查，通過后進(jìn)行自動(dòng)驗(yàn)證，如果出現(xiàn)違反協(xié)議性質(zhì)的情況，則會(huì)給出反例；如果無(wú)違反協(xié)議性質(zhì)的情況，則驗(yàn)證成功。

圖1 SPIN驗(yàn)證過程

2 無(wú)人機(jī)無(wú)線通信協(xié)議認(rèn)證過程分析

無(wú)人機(jī)無(wú)線通信協(xié)議認(rèn)證過程如圖2所示，應(yīng)用場(chǎng)景為多個(gè)無(wú)人機(jī)和地面控制站之間進(jìn)行無(wú)線通信，以及各個(gè)無(wú)人機(jī)之間進(jìn)行信息交換。其中，控制站具有較強(qiáng)的計(jì)算能力和存儲(chǔ)資源；而無(wú)人機(jī)節(jié)點(diǎn)計(jì)算能力和存儲(chǔ)資源較弱。為保證信息通信的安全性，通信雙方需進(jìn)行身份認(rèn)證。在此，根據(jù)Dolev-Yao模型[20]，進(jìn)行合理化假設(shè)：

1)該協(xié)議本身使用的加密算法沒有漏洞，即攻擊者無(wú)法利用密碼算法的漏洞進(jìn)行攻擊。

2)經(jīng)過密鑰加密的消息，只有相應(yīng)的解密密鑰才可以解密。

3)攻擊者可以參與到合法主體的會(huì)話中，即攻擊者也擁有自己的密鑰和隨機(jī)數(shù)。

圖2 無(wú)人機(jī)無(wú)線通信協(xié)議認(rèn)證示意圖

為分析方便，設(shè)置無(wú)人機(jī)無(wú)線通信協(xié)議中的相關(guān)變量符號(hào)如表1所示。

表1 無(wú)人機(jī)無(wú)線通信協(xié)議變量符號(hào)

根據(jù)協(xié)議的通信過程，相應(yīng)的認(rèn)證過程主要分為認(rèn)證初始化、無(wú)人機(jī)節(jié)點(diǎn)與控制站之間身份認(rèn)證、無(wú)人機(jī)節(jié)點(diǎn)之間身份認(rèn)證3個(gè)階段。

2.1 認(rèn)證初始化階段：

1)設(shè)定符合密碼機(jī)制的橢圓曲線Ep(a,b)及其點(diǎn)群上階次為q的生成元G(x,y)、合適的散列函數(shù)H、加密算法ENC和解密算法DEC，以及時(shí)間間隔ΔT。

2)控制站CS生成①CS公私鑰對(duì)(Prcs,Pucs)：

(1)

②UAV節(jié)點(diǎn)(設(shè)為n個(gè))公私鑰對(duì)密鑰表{Pruav(i),Puuav(i)|1≤i≤n}，其中，每個(gè)節(jié)點(diǎn)的公私鑰對(duì)計(jì)算如下：

(2)

③CS向各個(gè)UAV節(jié)點(diǎn)發(fā)送的隨機(jī)數(shù)RANDCS。

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

(3)

由圖3可知，G(x,y)為橢圓曲線Ep(a,b)上一點(diǎn)，所有私鑰均為[1,q-1]區(qū)間內(nèi)的隨機(jī)數(shù)，而公鑰均是位于橢圓曲線上的一點(diǎn)。

圖3 網(wǎng)絡(luò)模型中各節(jié)點(diǎn)公私鑰生成示意圖

3)UAV接收由CS發(fā)送的所有參數(shù){Ep(a,b),q,G(x,y),H,ENC,DEC,ΔT,Prcs,Pucs,Pruav(i),Puuav(i),RANDcs(i)}，并保證自身系統(tǒng)時(shí)間與CS一致。

2.2 無(wú)人機(jī)節(jié)點(diǎn)與控制站身份認(rèn)證階段：

1)UAV請(qǐng)求CS認(rèn)證：UAV由RANDuav和G(x,y)生成橢圓曲線上的一點(diǎn)(xt,yt)，并根據(jù)式(4)計(jì)算簽名認(rèn)證信息S1UAV和S2UAV,之后將元組信息{TUAV,S1UAV,S2UAV}發(fā)送給CS，即消息1(Msg1)，其中TUAV為當(dāng)前系統(tǒng)時(shí)間。

(4)

Msg1:UAV→CS:TUAV,S1UAV,S2UAV

2)CS首先驗(yàn)證是否滿足T-TUAV<△T以保證Msg1的新鮮性。若條件滿足，則計(jì)算簽名信息S1CS和S2CS，如式(5)所示，只有S2CS=S1UAV時(shí)UAV才能通過CS的認(rèn)證；否則，認(rèn)證失敗。之后CS生成其與UAV的會(huì)話密鑰KEYCU，隨后CS向UAV發(fā)送{RANDCS+1}KEYCU,即消息2(Msg2)，并更新本地隨機(jī)數(shù)RANDCS=RANDCS+1。

(5)

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

3)UAV對(duì)CS進(jìn)行認(rèn)證。UAV同樣需生成KEYCU,如式(6)所示，用該密鑰解密Msg2，如果解密消息為RANDCS+1，則CS通過認(rèn)證；否則認(rèn)證失敗。認(rèn)證成功后UAV更新本地隨機(jī)數(shù)RANDCS=RANDCS+1 。之后UAV和CS之間使用會(huì)話密鑰KEYCU進(jìn)行通信。

(6)

2.3 無(wú)人機(jī)節(jié)點(diǎn)間身份認(rèn)證階段

在此，設(shè)UAVi和UVAj兩個(gè)無(wú)人機(jī)節(jié)點(diǎn)之間進(jìn)行身份認(rèn)證，具體過程如下：

1)UAVi生成隨機(jī)數(shù)RANDij，其中RANDij∈[1,q-1]，之后通過UAVi和CS的會(huì)話密鑰KEYCUi將隨機(jī)數(shù)加密后發(fā)送給CS，即消息3(Msg3)。

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

2)CS解密后獲得隨機(jī)數(shù)RANDij，再通過UAVj和CS的會(huì)話密鑰KEYCU(j)將得到的隨機(jī)數(shù)加密后發(fā)送給UAVj，即消息4(Msg4)。

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

3)UAVi向UAVj發(fā)起認(rèn)證請(qǐng)求。UAVi計(jì)算節(jié)點(diǎn)間會(huì)話密鑰KEYij，如式(7)所示，其中Pruavi為UAVi的私鑰，Puuavj為UAVj的公鑰，并獲取當(dāng)前系統(tǒng)時(shí)間Ti，之后用該密鑰加密{RANDij||Ti}發(fā)送給UAVj，即消息5(Msg5)。

(7)

(8)

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

3 無(wú)人機(jī)無(wú)線通信協(xié)議認(rèn)證建模

為對(duì)該協(xié)議進(jìn)行一致性認(rèn)證，需通過線性時(shí)序邏輯LTL進(jìn)行模型檢測(cè)。具體包括以下3個(gè)部分。

3.1 定義協(xié)議安全屬性

要進(jìn)行模型檢測(cè)，首先需利用線性時(shí)序邏輯LTL來(lái)表示無(wú)人機(jī)協(xié)議的安全屬性，以便通過模型檢測(cè)工具SPIN來(lái)自動(dòng)檢測(cè)模型是否滿足安全屬性，若不滿足，則會(huì)給出反例。

模型的安全屬性需要用原子謂詞變量來(lái)進(jìn)行表示，其中0代表事件為假，1代表事件為真，本文定義的原子謂詞變量為：

bitstartUAVjCS=0;bitstartCSUAVj=0;

bitfinishUAVjCS=0;bitfinishUAViCS=0;

bitstartUAViCS=0;bitstartCSUAVi=0;

bitRANDj=1;bitRANDi=1;

其中startUAVjCS表示無(wú)人機(jī)UAVj向控制站CS發(fā)起會(huì)話，startUAVjCS=0表示無(wú)人機(jī)UAVj沒有向控制站CS發(fā)起會(huì)話，當(dāng)無(wú)人機(jī)UAVj向控制站CS發(fā)起會(huì)話則startUAVjCS=1,startCSUAVj表示控制站CS向無(wú)人機(jī)UAVj發(fā)起會(huì)話，finishUAVjCS表示無(wú)人機(jī)UAVj完成了與控制站CS的會(huì)話，其他原子謂詞變量含義與之類似。RANDj=1表示UAVj收到CS發(fā)送的隨機(jī)數(shù)與收到UAVi發(fā)送的隨機(jī)數(shù)相等，RANDi=1表示UAVi收到UAVj發(fā)送的隨機(jī)數(shù)比自己生成的隨機(jī)數(shù)大1。

然后通過宏定義方式來(lái)更新原子謂詞的值，例如定義update_RANDj(x,y)，當(dāng)x與y的值不相等，則會(huì)使原子謂詞變量RANDj的值變?yōu)?，類似如下：

#defineupdate_RANDj(x,y)if

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

∷elseskipfi

… …

根據(jù)定義好的原子謂詞來(lái)構(gòu)建LTL公式，其中，LTL公式中符號(hào)[]表示總是處于某個(gè)狀態(tài)，符號(hào)!表示邏輯非，符號(hào)||表示邏輯或，符號(hào)U表示直到，符號(hào)&&代表邏輯與，例如x和y為原子命題，公式(！xUy)表示命題y為真之前命題x一直為假。無(wú)人機(jī)UAV與控制站CS認(rèn)證性分析如下：

無(wú)人機(jī)UAVj與控制站CS的認(rèn)證，需要控制站CS向發(fā)起方無(wú)人機(jī)UAVj發(fā)起會(huì)話之后，無(wú)人機(jī)UAVj結(jié)束了與應(yīng)答方控制站CS的會(huì)話或者無(wú)人機(jī)UAVj一直沒有結(jié)束與控制站CS的會(huì)話。LTL公式表示為：

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

startCSUAVj))

同理無(wú)人機(jī)UAVi與控制站CS的認(rèn)證用LTL公式表示為：

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

startCSUAVi))

無(wú)人機(jī)UAV與控制站CS認(rèn)證性需要同時(shí)滿足這兩條LTL公式，故完整的LTL公式為：

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

startCSUAVj)))&

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

startCSUAVi)))

無(wú)人機(jī)UAVi與無(wú)人機(jī)UAVj認(rèn)證性分析如下：無(wú)人機(jī)UAVj對(duì)無(wú)人機(jī)UAVi的認(rèn)證為UAVj收到CS發(fā)送的隨機(jī)數(shù)與收到UAVi發(fā)送的隨機(jī)數(shù)相等。LTL公式表示為：

[]RANDj

無(wú)人機(jī)UAVi對(duì)無(wú)人機(jī)UAVj的認(rèn)證為UAVi收到UAVj發(fā)送的隨機(jī)數(shù)比自己生成的隨機(jī)數(shù)大1。LTL公式表示為：

[]RANDi

無(wú)人機(jī)UAVi與無(wú)人機(jī)UAVj認(rèn)證性需要同時(shí)滿足這兩條LTL公式，故完整的LTL公式為：

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

3.2 誠(chéng)實(shí)主體建模

無(wú)人機(jī)無(wú)線通信協(xié)議的誠(chéng)實(shí)主體為無(wú)人機(jī)UAV和控制站CS，為反映無(wú)人機(jī)與控制站，以及無(wú)人機(jī)之間的相互認(rèn)證過程，在此，設(shè)3個(gè)進(jìn)程proctypePUAVj(),proctypePUAVi()和proctypePCS()。

首先，構(gòu)建一個(gè)數(shù)據(jù)項(xiàng)的有限集合，對(duì)本文所使用的消息進(jìn)行枚舉：

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

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

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

上述數(shù)據(jù)項(xiàng)中Att表示攻擊者，R表示未知的主體，KEYca為控制站CS與攻擊者Att的會(huì)話密鑰，gD表示攻擊者產(chǎn)生的隨機(jī)數(shù)信息。

其次根據(jù)無(wú)人機(jī)認(rèn)證協(xié)議中傳輸消息的數(shù)目和傳輸目的不同，故需要用6個(gè)通道來(lái)模擬數(shù)據(jù)項(xiàng)的傳輸，如圖4所示。

圖4 傳輸通道示意圖

其中：c1,c2通道分別用于傳輸U(kuò)AVj和CS認(rèn)證信息Msg1,Msg2，c3,c4通道分別用于傳輸U(kuò)AVi和CS認(rèn)證信息Msg1,Msg2，c5通道用于傳輸Msg3和Msg4，c6通道用于傳輸Msg5和Msg6。每個(gè)通道所定義的元素比要傳輸?shù)脑囟鄡身?xiàng)，因?yàn)槊總€(gè)通道第一項(xiàng)表示消息的發(fā)送者，最后一項(xiàng)表示消息的接收者，例如：

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

表示消息發(fā)送者UAVj通過通道c1向消息接收者CS發(fā)送信息TUAVj,S1UAVj,S2UAVj。

3.3 攻擊者建模

攻擊者建模遵循Dolev-Yao攻擊者模型的攻擊能力，攻擊者可以竊聽、截獲、存儲(chǔ)、重放接收到的信息，并可以利用得到的知識(shí)項(xiàng)進(jìn)行消息的重組、轉(zhuǎn)發(fā)。

3.3.1 攻擊者需要表示的知識(shí)項(xiàng)的獲取

首先求解攻擊者可以學(xué)會(huì)的知識(shí)項(xiàng)，攻擊者可以學(xué)會(huì)的知識(shí)項(xiàng)是由攻擊者通過截獲誠(chéng)實(shí)主體發(fā)送的信息，對(duì)未加密的信息直接存儲(chǔ)，能解密的信息解密后進(jìn)行存儲(chǔ)，不能解密的信息整條進(jìn)行存儲(chǔ)。

例如無(wú)人機(jī)UAVj向控制站CS發(fā)送認(rèn)證消息{TUAVj,S1UAVj,S2UAVj}，此消息屬于未加密的信息，則攻擊者可以學(xué)會(huì)的知識(shí)項(xiàng)為TUAVj,S1UAVj和S2UAVj。而控制站CS向無(wú)人機(jī)UAVj發(fā)送認(rèn)證消息{RANDCSj+1}KEYCU(j)，此消息屬于加密消息，但攻擊者無(wú)解密密鑰KEYCU(j)，故攻擊者對(duì)整條消息進(jìn)行存儲(chǔ)，可學(xué)會(huì)的知識(shí)項(xiàng)為{RANDCSj+1}KEYCU(j)。

故攻擊者可學(xué)會(huì)的知識(shí)項(xiàng)如表2所示。

表2 攻擊者可學(xué)會(huì)的知識(shí)項(xiàng)

其次通過設(shè)立的接收語(yǔ)句來(lái)判斷每一條攻擊者可以學(xué)會(huì)知識(shí)項(xiàng)是否可以構(gòu)成誠(chéng)實(shí)主體能接收的消息，如果能，則為攻擊者需要表示的知識(shí)項(xiàng)；否則不是攻擊者需要表示的知識(shí)項(xiàng)。設(shè)立的接收語(yǔ)句如下：

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函數(shù)的作用是判斷接收值與期望值是否相同，依次從左到右進(jìn)行判斷，如果相同則接收數(shù)據(jù)項(xiàng)；否則只要有一項(xiàng)數(shù)據(jù)項(xiàng)不相同則拒絕接收整條消息。變量self，party1和party2取值為消息的發(fā)送者或接收者。符號(hào)?表示消息的接收。例如無(wú)人機(jī)UAVj向控制站CS發(fā)送認(rèn)證消息Msg1，對(duì)于接收者CS來(lái)說，接收到的信息都不是由它自己生成的，不能直接確定接收到的信息，對(duì)于不能確定的信息用變量來(lái)表示，即g1,g2和g3。而控制站CS向無(wú)人機(jī)UAVj發(fā)送認(rèn)證消息Msg2，對(duì)于接收者UAVj來(lái)說，信息RANDcsj1，KEYcuj在協(xié)議的初始化階段控制站CS和無(wú)人機(jī)UAVj就已經(jīng)協(xié)商好，接收者UAVj可以確定這些信息，故直接用eval函數(shù)來(lái)判斷。

接收者不能確定的數(shù)據(jù)項(xiàng)用g(1-13)變量表示，g8變量的取值范圍{KEYcuj,KEYcui,KEYca}，其他變量取值范圍為{Tuavj,Tuavi,Tj,Ti,S1uavj,S2uavj,S1uavi,S2uavi,RANDcsj1,RANDcsi1,RANDij,gD,RANDij1}。例如攻擊者可學(xué)會(huì)的知識(shí)項(xiàng)TUAVj，它可以構(gòu)成{TUAVj,TUAVj,TUAVj}使得接收語(yǔ)句c1?eval(party1),g1,g2,g3,eval(self);接收，故TUAVj是攻擊者需要表示的知識(shí)項(xiàng)。

根據(jù)分析得出攻擊者需要表示的知識(shí)項(xiàng)，如下所示：

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 攻擊者行為建模

攻擊者行為建模包括知識(shí)項(xiàng)的表示，知識(shí)項(xiàng)的截取和學(xué)習(xí)，消息的構(gòu)建與轉(zhuǎn)發(fā)3個(gè)部分。

知識(shí)項(xiàng)的表示：例如定義bitk_Tuavj=0;來(lái)表示攻擊者TUAVj知識(shí)項(xiàng)，其中初始值為0表示攻擊者還未學(xué)會(huì)此條知識(shí)項(xiàng)，若值變?yōu)?表示攻擊者已學(xué)會(huì)。

知識(shí)項(xiàng)的截取和學(xué)習(xí)：攻擊者可以截取知識(shí)項(xiàng)并對(duì)截取的知識(shí)項(xiàng)進(jìn)行學(xué)習(xí)。例如c1?_,x1,x2,x3,_;表示攻擊者可以通過c1通道來(lái)截獲通訊主體間的信息，下劃線_表示攻擊者不需要判斷發(fā)送者和接收者是誰(shuí)，直接獲取知識(shí)項(xiàng)。

消息的構(gòu)建與轉(zhuǎn)發(fā)：攻擊者可以根據(jù)自己已經(jīng)學(xué)會(huì)的知識(shí)項(xiàng)進(jìn)行消息構(gòu)建并轉(zhuǎn)發(fā)。例如：c1!((k_Tuavj&&k_S1uavj&&k_S2uavj)->CS:R),Tuavj,S1uavj,S2uavj,CS。

表示攻擊者如果分別學(xué)會(huì)TUAVj,S1UAVj,S2UAVj，則會(huì)通過c1通道將消息TUAVj,S1UAVj,S2UAVj發(fā)送給CS，否則消息發(fā)送給未知的主體R。

4 實(shí)驗(yàn)結(jié)果與分析

在Windows 10 64位系統(tǒng)SPIN6.5.1，iSPIN1.1.4的模擬環(huán)境下進(jìn)行仿真實(shí)驗(yàn)，最終驗(yàn)證出無(wú)人機(jī)無(wú)線通信協(xié)議的攻擊漏洞。

驗(yàn)證無(wú)人機(jī)UAV與控制站CS認(rèn)證性時(shí)，攻擊者攻擊流程如圖5所示。

圖5 攻擊者攻擊流程

此過程破壞了無(wú)人機(jī)UAVj對(duì)控制站CS的認(rèn)證性。首先UAVj向CS發(fā)送TUAVj,S1UAVj,S2UAVj，CS對(duì)UAVj認(rèn)證通過后向UAVj發(fā)送{RANDCSj+1}KEYCU(j)，但是此過程被攻擊者Att截獲，隨后冒充CS給UAVj發(fā)送{RANDCSj+1}KEYCU(j)，導(dǎo)致UAVj誤認(rèn)為發(fā)送者Att的身份是CS，使無(wú)人機(jī)UAVj對(duì)控制站CS的認(rèn)證遭到了破壞具體攻擊過程如下：

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

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

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

此過程還破壞了無(wú)人機(jī)UAVi對(duì)控制站CS的認(rèn)證性。首先UAVi向CS發(fā)送TUAVi,S1UAVi,S2UAVi，CS對(duì)UAVi認(rèn)證通過后向UAVi發(fā)送{RANDCSi+1}KEYCU(i)，但是此過程被攻擊者Att截獲，隨后冒充CS給UAVi發(fā)送{RANDCSi+1}KEYCU(i)，導(dǎo)致UAVi誤認(rèn)為發(fā)送者Att的身份是CS，使無(wú)人機(jī)UAVi對(duì)控制站CS的認(rèn)證遭到了破壞，具體攻擊過程如下：

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

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

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

驗(yàn)證無(wú)人機(jī)UAVi與無(wú)人機(jī)UAVj認(rèn)證性時(shí)，攻擊者攻擊流程如圖6所示。

圖6 攻擊者攻擊流程

經(jīng)過分析得到下列攻擊過程：

(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為驗(yàn)證無(wú)人機(jī)之間認(rèn)證結(jié)果相關(guān)信息，檢測(cè)結(jié)果顯示State-vector(狀態(tài)向量)所需內(nèi)存為120字節(jié)，depth reached(搜索深度)為40層,errors(錯(cuò)誤項(xiàng))的值為1，states,stored(狀態(tài)存儲(chǔ)數(shù))值為16，transitions(狀態(tài)遷移數(shù))值為16。State-vector，depth reached，states,stored，transitions四個(gè)值越小，表示建立的模型越好，驗(yàn)證的速度越快，越不容易出現(xiàn)狀態(tài)空間爆炸的情況。

圖7 驗(yàn)證結(jié)果相關(guān)信息

5 結(jié)束語(yǔ)

本文主要針對(duì)無(wú)人機(jī)無(wú)線通信協(xié)議進(jìn)行身份認(rèn)證與一致性驗(yàn)證，提出一種改進(jìn)的攻擊者獲取知識(shí)方法，可直接通過攻擊者可學(xué)會(huì)的知識(shí)項(xiàng)來(lái)求取攻擊者需要表示的知識(shí)項(xiàng)，使分析復(fù)雜協(xié)議的過程更加簡(jiǎn)單，并運(yùn)用模型檢測(cè)工具SPIN對(duì)控制站CS，無(wú)人機(jī)UAV，攻擊者H三者進(jìn)行建模，檢測(cè)出攻擊者攻擊流程，結(jié)果表明此認(rèn)證協(xié)議并不安全，故下一步的工作是針對(duì)此攻擊者漏洞來(lái)對(duì)無(wú)人機(jī)認(rèn)證協(xié)議進(jìn)行改進(jìn)和驗(yàn)證，來(lái)使其安全性更高。