劉 棟,連曉峰,王宇龍,譚 勵(lì),趙宇琦,李 林
(1.北京工商大學(xué) 人工智能學(xué)院,北京 100048;2.中國(guó)兵器工業(yè)信息中心,北京 100089;3.北京工商大學(xué) 計(jì)算機(jī)學(xué)院,北京 100048)
隨著科學(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)。
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)證過程
無(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è)階段。
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一致。
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)
在此,設(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
為對(duì)該協(xié)議進(jìn)行一致性認(rèn)證,需通過線性時(shí)序邏輯LTL進(jìn)行模型檢測(cè)。具體包括以下3個(gè)部分。
要進(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)
無(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。
攻擊者建模遵循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。
在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)信息
本文主要針對(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)使其安全性更高。