劉 棟，連曉峰，王宇龍，譚 勵，趙宇琦，李 林

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

0 引言

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

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

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

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

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

1 模型檢測工具SPIN

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

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

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

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

圖1 SPIN驗證過程

2 無人機無線通信協(xié)議認證過程分析

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

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

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

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

圖2 無人機無線通信協(xié)議認證示意圖

為分析方便，設置無人機無線通信協(xié)議中的相關變量符號如表1所示。

表1 無人機無線通信協(xié)議變量符號

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

2.1 認證初始化階段：

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

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

(1)

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

(2)

③CS向各個UAV節(jié)點發(fā)送的隨機數(shù)RANDCS。

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

(3)

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

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

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)時間與CS一致。

2.2 無人機節(jié)點與控制站身份認證階段：

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

(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發(fā)送{RANDCS+1}KEYCU,即消息2(Msg2)，并更新本地隨機數(shù)RANDCS=RANDCS+1。

(5)

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

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

(6)

2.3 無人機節(jié)點間身份認證階段

在此，設UAVi和UVAj兩個無人機節(jié)點之間進行身份認證，具體過程如下：

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

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

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

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

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

(7)

(8)

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

3 無人機無線通信協(xié)議認證建模

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

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

要進行模型檢測，首先需利用線性時序邏輯LTL來表示無人機協(xié)議的安全屬性，以便通過模型檢測工具SPIN來自動檢測模型是否滿足安全屬性，若不滿足，則會給出反例。

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

bitstartUAVjCS=0;bitstartCSUAVj=0;

bitfinishUAVjCS=0;bitfinishUAViCS=0;

bitstartUAViCS=0;bitstartCSUAVi=0;

bitRANDj=1;bitRANDi=1;

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

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

#defineupdate_RANDj(x,y)if

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

∷elseskipfi

… …

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

無人機UAVj與控制站CS的認證，需要控制站CS向發(fā)起方無人機UAVj發(fā)起會話之后，無人機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發(fā)送的隨機數(shù)與收到UAVi發(fā)送的隨機數(shù)相等。LTL公式表示為：

[]RANDj

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

[]RANDi

無人機UAVi與無人機UAVj認證性需要同時滿足這兩條LTL公式，故完整的LTL公式為：

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

3.2 誠實主體建模

無人機無線通信協(xié)議的誠實主體為無人機UAV和控制站CS，為反映無人機與控制站，以及無人機之間的相互認證過程，在此，設3個進程proctypePUAVj(),proctypePUAVi()和proctypePCS()。

首先，構建一個數(shù)據(jù)項的有限集合，對本文所使用的消息進行枚舉：

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ù)項中Att表示攻擊者，R表示未知的主體，KEYca為控制站CS與攻擊者Att的會話密鑰，gD表示攻擊者產(chǎn)生的隨機數(shù)信息。

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

圖4 傳輸通道示意圖

其中：c1,c2通道分別用于傳輸UAVj和CS認證信息Msg1,Msg2，c3,c4通道分別用于傳輸UAVi和CS認證信息Msg1,Msg2，c5通道用于傳輸Msg3和Msg4，c6通道用于傳輸Msg5和Msg6。每個通道所定義的元素比要傳輸?shù)脑囟鄡身棧驗槊總€通道第一項表示消息的發(fā)送者，最后一項表示消息的接收者，例如：

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

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

3.3 攻擊者建模

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

3.3.1 攻擊者需要表示的知識項的獲取

首先求解攻擊者可以學會的知識項，攻擊者可以學會的知識項是由攻擊者通過截獲誠實主體發(fā)送的信息，對未加密的信息直接存儲，能解密的信息解密后進行存儲，不能解密的信息整條進行存儲。

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

接收者不能確定的數(shù)據(jù)項用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是攻擊者需要表示的知識項。

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

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

攻擊者行為建模包括知識項的表示，知識項的截取和學習，消息的構建與轉(zhuǎn)發(fā)3個部分。

知識項的表示：例如定義bitk_Tuavj=0;來表示攻擊者TUAVj知識項，其中初始值為0表示攻擊者還未學會此條知識項，若值變?yōu)?表示攻擊者已學會。

知識項的截取和學習：攻擊者可以截取知識項并對截取的知識項進行學習。例如c1?_,x1,x2,x3,_;表示攻擊者可以通過c1通道來截獲通訊主體間的信息，下劃線_表示攻擊者不需要判斷發(fā)送者和接收者是誰，直接獲取知識項。

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

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

4 實驗結果與分析

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

驗證無人機UAV與控制站CS認證性時，攻擊者攻擊流程如圖5所示。

圖5 攻擊者攻擊流程

此過程破壞了無人機UAVj對控制站CS的認證性。首先UAVj向CS發(fā)送TUAVj,S1UAVj,S2UAVj，CS對UAVj認證通過后向UAVj發(fā)送{RANDCSj+1}KEYCU(j)，但是此過程被攻擊者Att截獲，隨后冒充CS給UAVj發(fā)送{RANDCSj+1}KEYCU(j)，導致UAVj誤認為發(fā)送者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發(fā)送TUAVi,S1UAVi,S2UAVi，CS對UAVi認證通過后向UAVi發(fā)送{RANDCSi+1}KEYCU(i)，但是此過程被攻擊者Att截獲，隨后冒充CS給UAVi發(fā)送{RANDCSi+1}KEYCU(i)，導致UAVi誤認為發(fā)送者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 攻擊者攻擊流程

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

圖7 驗證結果相關信息

5 結束語

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