無人機無線通信協議的形式化認證分析與驗證

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

(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三者進行建模，檢測出攻擊者攻擊流程，結果表明此認證協議并不安全，故下一步的工作是針對此攻擊者漏洞來對無人機認證協議進行改進和驗證，來使其安全性更高。