李學(xué)峰 張俊偉 馬建峰 劉 海

1(西安電子科技大學(xué)網(wǎng)絡(luò)與信息安全學(xué)院 西安 710071)2(青海廣播電視大學(xué)教育技術(shù)中心 西寧 810008) (jwzhang@xidian.edu.cn)

?

TSNP：空間信息網(wǎng)中PCL安全高效的群組認(rèn)證協(xié)議

李學(xué)峰1,2張俊偉1馬建峰1劉 海1

1(西安電子科技大學(xué)網(wǎng)絡(luò)與信息安全學(xué)院 西安 710071)2(青海廣播電視大學(xué)教育技術(shù)中心 西寧 810008) (jwzhang@xidian.edu.cn)

由于空間信息網(wǎng)絡(luò)(space information network, SIN)具有高動態(tài)拓?fù)?、衛(wèi)星計算和通信資源受限等特點，當(dāng)群組飛行器需要與衛(wèi)星快速接入認(rèn)證以實現(xiàn)信息連續(xù)收集或擴大觀測范圍時，已有協(xié)議方案不能完全滿足SIN的特點和一些應(yīng)用需求.為此，提出一種面向空間信息網(wǎng),協(xié)議組合邏輯(protocol composition logic, PCL)安全的群組多用戶快速認(rèn)證協(xié)議(TSNP).基于對稱加密體制、密鑰分層的思想，TSNP允許群組內(nèi)完成接入認(rèn)證的節(jié)點向其他用戶發(fā)送消息，通過計算使得群組內(nèi)用戶擁有與衛(wèi)星通信的密鑰，實現(xiàn)群組內(nèi)用戶高效安全認(rèn)證或切換.通過PCL模型對TSNP各階段協(xié)議安全屬性進行分析，并使用并行和順序組合方法證明TSNP能保障組合后協(xié)議的安全屬性.實驗結(jié)果表明:TSNP一方面減少了對地面管理中心的依賴程度，同時有效降低了衛(wèi)星計算和通信開銷.

空間信息網(wǎng)絡(luò)；群組認(rèn)證；協(xié)議組合邏輯；認(rèn)證性；機密性

隨著衛(wèi)星通信技術(shù)的發(fā)展和人們對無線網(wǎng)絡(luò)各種需求的激增，空間信息網(wǎng)絡(luò)已備受關(guān)注.空間信息網(wǎng)絡(luò)(space information network, SIN)[1]是以空間平臺(如同步衛(wèi)星或中、低軌道衛(wèi)星、平流層氣球和有人或無人駕駛飛機等)為載體，實時獲取、傳輸和處理空間信息的網(wǎng)絡(luò)系統(tǒng).SIN在環(huán)境與災(zāi)難檢測、緊急救助、全球定位、空間追蹤和控制等領(lǐng)域有廣泛的應(yīng)用前景[2-5].

當(dāng)群組飛行器需要接入衛(wèi)星以擴大其在執(zhí)行環(huán)境與災(zāi)難監(jiān)測或空間追蹤的范圍時或者當(dāng)群組飛行器因為超出某個衛(wèi)星的覆蓋范圍時需要切換至其他衛(wèi)星時，例如無人機群組，就需要一個安全的能支持認(rèn)證、切換的協(xié)議來保證群組飛行器與衛(wèi)星進行安全通信.這個協(xié)議主要完成2個任務(wù)：1)實現(xiàn)2個通信節(jié)點的身份認(rèn)證，以防止非法節(jié)點假冒合法節(jié)點刪除、篡改數(shù)據(jù)、占用網(wǎng)絡(luò)資源；2)通過認(rèn)證建立會話密鑰，以便通過加密機制保護合法節(jié)點在網(wǎng)絡(luò)上的通信，抵抗非法竊聽.

由于SIN具有高度復(fù)雜性、動態(tài)性、開放性的特點，節(jié)點之間通信容易受到攻擊者的截取、刪除、篡改等安全威脅，各節(jié)點也容易受到來自敵手的攻擊[6-9].例如，被動攻擊者可以任意截獲網(wǎng)絡(luò)數(shù)據(jù)流、隨意轉(zhuǎn)發(fā)數(shù)據(jù)，同時也可對消息進行重放攻擊，這樣就威脅到數(shù)據(jù)的機密性以及帶來非授權(quán)訪問等安全威脅；主動攻擊者可以截獲節(jié)點間的數(shù)據(jù)流，選擇性地對數(shù)據(jù)進行惡意刪除或修改，同時利用節(jié)點間的鏈路進行假冒身份，侵入系統(tǒng)或發(fā)送偽造信號，此外合法的節(jié)點也會受到欺騙攻擊等安全威脅.

為了確保SIN網(wǎng)絡(luò)通信及節(jié)點免受攻擊，需要認(rèn)證機制保證空間信息網(wǎng)的通信安全，其目的是防止非授權(quán)節(jié)點接入和訪問網(wǎng)絡(luò)并阻止假冒攻擊.認(rèn)證協(xié)議不僅能為空間信息網(wǎng)中通信的節(jié)點進行身份確認(rèn)并生成一個共享的秘密，建立一條安全的信道，而且還能使用組合證明的方式來證明其安全性，此外還要滿足空間信息網(wǎng)的特點[8,10-13]：

1) 高動態(tài)拓?fù)洌淳W(wǎng)絡(luò)拓?fù)浣Y(jié)構(gòu)變化頻繁，衛(wèi)星與衛(wèi)星、衛(wèi)星與節(jié)點之間的相互位置不斷發(fā)生變化，這就要求衛(wèi)星之間以及衛(wèi)星與地面或飛行器隨時切換以維持通信.

2) 計算資源和通信能力受限，由于衛(wèi)星計算能力、存儲器容量以及通信能力均受到宇航級芯片限制，因此設(shè)計的協(xié)議運算量和交互次數(shù)也受到限制，必須保證在不失安全性的基礎(chǔ)上，構(gòu)建簡潔、高效的認(rèn)證協(xié)議.公鑰密碼算法需要更多的計算開銷，加之空間網(wǎng)絡(luò)中數(shù)據(jù)流量較大，為了滿足信息傳輸?shù)膶崟r性要求，可使用加解密速度快得多的對稱密鑰算法.

3) 節(jié)點之間通信往返時間長，由于空間信息網(wǎng)各節(jié)點(地面設(shè)備、衛(wèi)星、飛行器)設(shè)備距離較遠，他們之間的通信時延較大，因此設(shè)計的協(xié)議既要有安全性，同時也要保證速度和效率.設(shè)計的協(xié)議滿足群組接入認(rèn)證，以減少認(rèn)證過程中的密碼算法處理時間和通信開銷，從而達到減少認(rèn)證持續(xù)時間、提高認(rèn)證效率.

4) SIN復(fù)雜性決定認(rèn)證協(xié)議可能需要多階段協(xié)議執(zhí)行，這些協(xié)議組合后應(yīng)能保證協(xié)議的安全屬性.另外，由于SIN開放性，節(jié)點之間的通信數(shù)據(jù)容易被攻擊者截取甚至篡改，合法的節(jié)點也容易受到偽裝攻擊，因此要考慮節(jié)點之間通信的安全性需求.

由于上述空間信息網(wǎng)的特點，對設(shè)計面向空間信息網(wǎng)的群組多用戶快速認(rèn)證協(xié)議帶來了挑戰(zhàn).

相關(guān)工作：

1) 組合安全理論.基于邏輯的可組合安全模型PCL是協(xié)議組合理論的典型代表之一.

PCL是一種支持協(xié)議屬性證明邏輯推導(dǎo)模型[14]，它由Cord演算、協(xié)議邏輯(語法和語義)、證明系統(tǒng)組成.PCL[15-16]是一個抽象了關(guān)于跟蹤的參數(shù)，消除了關(guān)于攻擊者明確推導(dǎo)的公理系統(tǒng).因為在一個假設(shè)攻擊者存在的情況下，對于任意協(xié)議的運行PCL完整的語義表明其公理和推導(dǎo)規(guī)則是正確的，這使得PCL證明簡潔、易讀.PCL已經(jīng)分析并驗證了許多重要的安全協(xié)議，如ISO-9798-3協(xié)議和STS協(xié)議族[14]、802.11i協(xié)議和TLS協(xié)議[17]、WAPI協(xié)議[18]、基于Diffie-Hellman協(xié)議[19]、基于NS(Needham-Schroeder, NS)協(xié)議[20]，使用PCL發(fā)現(xiàn)并改正一些協(xié)議中的安全缺陷.

在可證明組合安全方面：文獻[14]利用PCL模型對ISO9798-3協(xié)議的密鑰機密性和會話認(rèn)證性進行了證明；文獻[17]利用PCL模型找出了802.11i協(xié)議的缺陷，使用順序組合證明方法證明了改進協(xié)議的安全屬性；文獻[20]利用PCL模型證明了NS協(xié)議族的安全屬性.因此，設(shè)計的協(xié)議可證明安全，以驗證其安全屬性.

2) 認(rèn)證及密鑰交換.文獻[21]基于DH困難假設(shè)提出了無線移動網(wǎng)絡(luò)下的相互認(rèn)證和密鑰交換協(xié)議，該協(xié)議無安全性證明；文獻[22]基于CDH假設(shè)提出了移動衛(wèi)星通信系統(tǒng)認(rèn)證密鑰交換協(xié)議；文獻[23]基于DDH假設(shè)提出了空間網(wǎng)絡(luò)相互認(rèn)證與密鑰協(xié)商協(xié)議，提出了基于有證書的公鑰系統(tǒng)模型；文獻[24]基于CDH假設(shè)提出了基于身份的衛(wèi)星通信認(rèn)證及密鑰交換協(xié)議；文獻[25-26] 面向移動通信提出了基于群組的認(rèn)證和密鑰協(xié)商協(xié)議.

上述文獻雖然面向無線移動網(wǎng)絡(luò)或空間信息網(wǎng)提出了認(rèn)證和密鑰交換或協(xié)商協(xié)議，有一定的借鑒意義，但和前述空間信息網(wǎng)的特點相比，文獻[21-24]一是沒有考慮群組認(rèn)證和密鑰協(xié)議，二是沒有考慮群組切換；文獻[23-24]也沒有考慮空間信息網(wǎng)的計算資源和通信能力以及認(rèn)證效率等方面的因素；文獻[25-26]未考慮群組切換、空間信息網(wǎng)的計算資源、通信能力等因素，另外基于Kerberos對稱密碼機制需要時鐘同步，在SIN中很難實現(xiàn).因此需要針對空間信息網(wǎng)的特點，設(shè)計高效、安全、群組多用戶快速接入?yún)f(xié)議.

3) 安全切換.文獻[27]依據(jù)地球同步軌道(geosynchronous earth orbit, GEO)衛(wèi)星的特點，設(shè)計與地面管理中心(無線網(wǎng)絡(luò))進行垂直切換的決策方法，該方案未考慮安全性因素；文獻[28]提出基于身份簽名的快速認(rèn)證方法，該方案對控制消息的機密性和完整性缺乏有效保護.文獻[29]通過采用預(yù)認(rèn)證和預(yù)配置的方法，提出了一種不與具體的移動性協(xié)議相關(guān)的快速切換框架，有效減少了切換延遲；文獻[30]基于雙線性配對函數(shù)提出了一個有效的安全切換方案，該方案未考慮群組安全切換.

上述文獻討論的安全切換方案，均未綜合考慮前述SIN的特點.因此，需要一個能支持群組多用戶快速安全切換的協(xié)議.

綜上所述，本文根據(jù)空間信息網(wǎng)的特點提出支持群組多用戶高效安全的認(rèn)證協(xié)議.本文工作如下：

1) 基于對稱密鑰機制、密鑰分層的思想面向空間信息網(wǎng)設(shè)計了支持群組高效、安全接入認(rèn)證和切換協(xié)議-TSNP.

2) 使用PCL模型對各階段協(xié)議進行形式化描述和安全性證明；對子協(xié)議組合并通過組合證明方法論證了組合后的協(xié)議具有密鑰機密性和會話認(rèn)證性.

3) 理論分析和實驗結(jié)果顯示TSNP協(xié)議減少了對地面管理中心的依賴程度，降低了衛(wèi)星的計算和通信開銷.

1 系統(tǒng)模型

1.1 系統(tǒng)模型

Fig. 1 System model.圖1 系統(tǒng)模型

VariableDescriptionMGroundManagementCenterGUUsersofGroupSA,SBSatelliteGKSharedKeyofMandGUMSA,MSBSharedKeyofMandSatelliteukiKeyofGroupUserGMKMasterSessionKeyofGUandSatelliteUMKMasterSessionKeyofUserGroupandSatelliteGSKTemporarySessionKeyofGUandSatelliteUSKTemporarySessionKeyofUserGroupandSatelliteGIDIdentityofGroupMIDIdentityofMuidiIdentityofFirstCommunicationinGUrmGeneratedRandomNumberbyMrg,r'gGeneratedRandomNumberbyuidirSA,rSBGeneratedRandomNumberbySatellitePRF(·)PseudoRandomOperationHASH(·)HASHOperationMAC(·)MACiscomputedusingaHashfunctionEK(·)EncryptionOperationbyKey

1.2 敵手模型

1) 地面管理中心M是可信的，它與群組用戶GU、衛(wèi)星SA,SB共享的長期密鑰不會泄露.

2) 信道被攻擊者控制，整個網(wǎng)絡(luò)通信環(huán)境是不可信的，攻擊者可以對數(shù)據(jù)流進行修改或偽造數(shù)據(jù).

3) 假設(shè)攻擊者不能攻破底層的密碼算法(PRF,HASH、分組加密算法)而獲取相關(guān)密鑰.

4) 假設(shè)攻擊者不能攻陷地面管理中心M和衛(wèi)星SA,SB.

1.3 安全目標(biāo)

1) 認(rèn)證性.系統(tǒng)模型中節(jié)點之間能夠相互認(rèn)證通信雙方節(jié)點身份以防止攻擊者進行仿冒或偽裝攻擊.

3) 順序組合安全性.接入認(rèn)證階段子協(xié)議進行順序組合后，能夠確保組合后協(xié)議的安全屬性，即滿足組合后協(xié)議的密鑰機密性和會話認(rèn)證性.

4) 并行組合安全性.群組內(nèi)用戶產(chǎn)生各自的密鑰被并行組合后，仍能夠保證協(xié)議的安全屬性，即群組內(nèi)用戶各自執(zhí)行協(xié)議動作，相互并行操作不影響整個協(xié)議安全屬性.

2 協(xié)議方案

2.1 認(rèn)證協(xié)議

認(rèn)證協(xié)議分為初始化階段、接入認(rèn)證階段、群組成員密鑰生成階段.

1) 初始化階段

地面管理中心M通過安全信道收集每個成員身份標(biāo)識及密鑰等信息，并進行存儲.M與群組成員和衛(wèi)星共享長期密鑰(GK,uki,MSA,MSB).群組由若干個成員構(gòu)成，每個成員的身份由GID和UID確定，每個成員都擁有對密鑰(GK,UK),GK為組密鑰，UK為成員密鑰.初始化階段完成后，地面管理中心M擁有群組中每個組成員的身份標(biāo)識UID、組標(biāo)識GID和每個成員的對密鑰(GK,UK)以及與衛(wèi)星共享的長期密鑰MSA,MSB.M收集的相關(guān)信息用GP表示，GP={MID,GID,UID}.

2) 接入認(rèn)證階段

圖2描述了TSNP認(rèn)證協(xié)議接入認(rèn)證階段的過程，整個過程包括主會話密鑰生成(記為TSNP.MKP)和臨時會話密鑰生成階段(記為TSNP.SKP)，主會話密鑰生成階段負(fù)責(zé)生成GMK,umki，臨時會話密鑰生成階段負(fù)責(zé)生成GSK,uski.密鑰生成主要使用偽隨機函數(shù)，計算公式如表2所示.

在消息傳輸過程中使用MAC來確保消息完整性，計算公式如表3所示.

主密鑰生成步驟如下：

② 衛(wèi)星SA收到Message1后，將Message2發(fā)送給地面管理中心M,其中Message2=(rg,GID,uidi,SIDA).

Fig. 2 Access authentication process of .圖接入SA認(rèn)證流程

GMKumkiuskiGSKPRF(GK‖rm‖MID‖rg‖GID‖SIDA)PRF(GMK‖uidi‖uki‖rg‖rm‖SIDA‖MID‖GID)PRF(umki‖rSA‖SIDA‖r'g‖uidi‖GID)PRF(GMK‖rSA‖r'g‖SIDA‖GID)

Table 3 Calculating Formula of MAC

③ 地面管理中心M收到Message2后，產(chǎn)生隨機數(shù)rm，依次生成GMK,UMK.地面管理中心M計算MAC1并將Message3發(fā)送給衛(wèi)星SA，其中Message3=(rm,MID,GID,uidi,SIDA,MAC1).

⑥ 衛(wèi)星SA接收Message4，將其轉(zhuǎn)發(fā)給地面管理中心M.

⑧ 衛(wèi)星SA接收Message5，解密消息并存儲.

臨時密鑰生成步驟如下：

3) 群組成員密鑰生成階段(記為TSNP.QKP)

Table 4 Calculating formula of MAC and Key

Fig..圖向群組成員發(fā)送消息

2.2 切換協(xié)議

中Message9=(r″g,GID,uidi,SIDA,MAC9),Message10=(rSB,SIDB,SIDA,MAC10,MAC11),Message11=(r″g,SIDB,SIDA,MAC12,MAC13).

Fig. 4 Handoff process of TSNP.圖4 TSNP切換

1) 主密鑰預(yù)置階段

因為空間信息網(wǎng)中衛(wèi)星的位置可以預(yù)判，所以當(dāng)衛(wèi)星SA解密消息EMSA{GP,GMK,UMK}后，通過安全信道發(fā)送給衛(wèi)星SB，這樣衛(wèi)星SB就擁有和群組用戶GU通信會話主密鑰.

2) 臨時密鑰生成階段

此階段臨時密鑰的生成與4.1節(jié)中臨時密鑰生成階段的方式相同，此處不再贅述.

2.3 密鑰層次

Fig. 5 Key Hierarchy.圖5 密鑰層次

1)GK,uki為長期共享密鑰，在此層次中為底層密鑰，在認(rèn)證協(xié)議初始化階段產(chǎn)生，它們負(fù)責(zé)導(dǎo)出其他層次密鑰.

2)GMK,umki為主會話密鑰，在TSNP協(xié)議主會話密鑰階段(MKP)生成，其中GMK由GK導(dǎo)出，umki由GMK和uki導(dǎo)出.

3)GSK,uski為臨時會話密鑰，在TSNP協(xié)議臨時會話密鑰階段(SKP)生成，其中GSK由GMK導(dǎo)出，uski由umki導(dǎo)出.

4)GMK,GSK負(fù)責(zé)加密通信雙方或群組成員的廣播消息.umki,uski負(fù)責(zé)加密通信雙方的消息.此外GMK,UMK還用于群組切換.

3 安全性及組合證明

TSNP協(xié)議方案包括認(rèn)證和安全切換2個協(xié)議，2個協(xié)議又分成了不同的階段執(zhí)行相關(guān)操作以生成主會話密鑰和臨時會話密鑰，由于安全切換協(xié)議與認(rèn)證協(xié)議中的臨時會話密鑰階段、群組內(nèi)成員密鑰生成階段類似，因此本節(jié)將給出TSNP協(xié)議MKP,SKP,QKP三個階段的形式化描述、安全屬性、不變量、安全證明等.本節(jié)使用PCL模型對協(xié)議的安全性及組合進行證明，PCL預(yù)備知識見附錄A.

3.1 主密鑰生成階段(TSNP.MKP)

3.1.1 協(xié)議形式化描述

uidi),MAC1)(MAC1MACGK(rm,MID,rg,

SIDA,uidi),MAC2),MAC2MACumki(rm,rg,

(rm,rg,MID,GID,uidi,SIDA))

3.1.2 前提條件

3.1.3 安全屬性

1) TSNP.MKP會話認(rèn)證性

2) TSNP.MKP密鑰機密性

由于篇幅有限及證明過程可參照定理2的證明.協(xié)議不變量描述見附錄B.

3.2 臨時會話密鑰生成階段(TSNP.SKP)

3.2.1 協(xié)議形式化描述

((GID,uidi,rSA,SIDA),MAC6,MAC7)〉]SA.

MAC6,MAC7))(MAC6

3.2.2 前提條件

3.2.3 安全屬性

1) TSNP.SKP會話認(rèn)證性

2) TSNP.SKP密鑰機密性

3.3 群組內(nèi)成員密鑰生成階段(TSNP.QKP)

3.3.1 協(xié)議形式化描述

以第j個成員為例，協(xié)議形式化描述如下：

(MAC8.

3.3.2 前提條件

3.3.3 安全屬性

1) TSNP.QKP會話認(rèn)證性

2) TSNP.QKP密鑰機密性

Has(Z,umkj)∧Has(Z,uskj)∧Has(Z,GSK))∧

協(xié)議不變量描述、證明過程與定理2類似，為節(jié)省篇幅，此處不再贅述.

3.4 組合TSNP協(xié)議

由于TSNP認(rèn)證協(xié)議中的接入認(rèn)證階段由主會話密鑰生成階段、臨時會話密鑰生成階段、群組內(nèi)用戶密鑰生成階段組成，3個階段協(xié)議組合后，需要借助PCL順序組合方法來保證組合后的協(xié)議滿足密鑰機密性和會話認(rèn)證性，另外群組內(nèi)用戶密鑰生成階段需要使用并行組合方法以證明群組內(nèi)用戶各自執(zhí)行協(xié)議而不影響其他用戶協(xié)議的安全屬性.

3.4.1 順序組合

TSNP認(rèn)證協(xié)議由TSNP.MKP,TSNP.SKP和TSNP.QKP協(xié)議順序組合而成，TSNP認(rèn)證協(xié)議的證明使用PCL中順序組合證明方法.

φTSNP.MKP=φTSNP.MKP,auth∧φTSNP.MKP,sec,

φTSNP.SKP=φTSNP.SKP,auth∧φTSNP.SKP,sec,

φTSNP.QKP=φTSNP.QKP,auth∧φTSNP.QKP,sec.

證明. TSNP認(rèn)證協(xié)議順序組合的安全性證明有5個步驟：

1) 由3個階段的安全性證明可得，TSNP.MKP,TSNP.SKP和TSNP.QKP可以滿足協(xié)議安全屬性：

φTSNP.QKP,sec.

2) 在更弱的前提假設(shè)下，協(xié)議安全屬性依然可以得到保證，即：

3) 由于φTSNP.MKP的后置條件滿足φTSNP.SKP的前提條件，同時φTSNP.SKP的前提條件滿足φTSNP.QKP的后置條件，即φTSNP.MKP?θTSNP.SKP,θTSNP.SKP?φTSNP.QKP,所以應(yīng)用順序規(guī)則S1進行順序組合.

4) 不變量ΓTSNP.MKP∪ΓTSNP.SKP∪ΓTSNP.QKP對于TSNP.MKP,TSNP.SKP和TSNP.QKP均成立，即：

5) 上述步驟說明TSNP.MKP,TSNP.SKP和TSNP.QKP的安全性在順序組合后仍然可以保證，即

φTSNP.SKP.auth∧φTSNP.SKP,sec.

證畢.

3.4.2 并行組合

假設(shè)TSNP.QKPm,TSNP.QKPn(m,n≠i)是TSNP.QKP階段任意2個子協(xié)議，子協(xié)議并行組合是2個協(xié)議線索并集.在并行組合下，為了保證每個協(xié)議安全屬性被保留，因此要充分驗證每個協(xié)議所代表的不變量.

證明. TSNP.QKP階段任意2個子協(xié)議的并行組合安全性證明如下：

1) 證明TSNP.QKPm,TSNP.QKPn各自的安全屬性

2) 確定證明中所使用不變量的集合ΓTSNP.QKPm,1∧ΓTSNP.QKPm,2和ΓTSNP.QKPn,1∧ΓTSNP.QKPn,2，從先前的步驟證明可以分解成2個部分:①使用誠實規(guī)則證明協(xié)議不變量;②不使用誠實規(guī)則，使用不變量作為假設(shè)證明協(xié)議的安全屬性.

φTSNP.QKPm.auth∧φTSNP.QKPm,sec,

φTSNP.QKPn,sec.

3) 在更弱的前提下(子協(xié)議不變量的并集)，協(xié)議安全屬性仍能夠得到保證.

φTSNP.QKPm.auth∧φTSNP.QKPm,sec,

φTSNP.QKPn.auth∧φTSNP.QKPn,sec.

4)TSNP.QKPm,TSNP.QKPn不變量的并集能夠持有2個協(xié)議:

φTSNP.QKPm.auth∧φTSNP.QKPm,sec,

φTSNP.QKPn.auth∧φTSNP.QKPn,sec.

證畢.

協(xié)議各階段安全性證明、順序組合及并行組合證明，說明TSNP協(xié)議已實現(xiàn)協(xié)議設(shè)計安全目標(biāo)，即子協(xié)議密鑰的機密性和會話的認(rèn)證性，通過組合證明，得出TSNP協(xié)議具有密鑰機密性和會話認(rèn)證性.

3.5 進一步安全性分析

除了上述的基于PCL證明之外，結(jié)合圖2對本文所提群組接入認(rèn)證協(xié)議的安全屬性進一步分析與說明.

1) 重放攻擊

在TSNP中，隨機數(shù)的使用可以有效地阻止重放攻擊，協(xié)議中的每個階段都有隨機數(shù)的產(chǎn)生，如rg，rm，rSA等，重新使用之前的隨機數(shù)不能產(chǎn)生有效的密鑰.

2) 竊聽

敵手可能在通信過程中竊聽消息，從而刪除或篡改消息.在TSNP中，參與通信雙方的身份標(biāo)識由地面管理中心統(tǒng)一控制，另外由于引入了MAC機制，因為TSNP可以抵抗竊聽.

3) 中間人攻擊

TSNP可以有效抵抗中間人攻擊，敵手不能收集到真實的密鑰信息，由于MAC機制存在，如果不能和地面管理中心產(chǎn)生的MAC值一致，則無法進行通信.

4) 前向攻擊

在TSNP中，如果敵手獲取了申請通信方目前的會話消息，但是之前的會話消息敵手無法獲取.因為在會話中有新隨機數(shù)的產(chǎn)生以及MAC校驗，所以之前的秘密消息是不能被泄露的，因此TSNP具有前向安全性.

4 性能分析

Table 5 Two Protocols Comparison of the Computation and Communication of Overhead

實驗對上述2個協(xié)議衛(wèi)星SA的計算時延進行了對比，如圖6所示.實驗時，在單機上測試協(xié)議的計算時延，而不考慮發(fā)送消息時的傳輸時延.本機的硬件環(huán)境：CPU為i5，內(nèi)存為4GB；軟件環(huán)境：系統(tǒng)是Win7，測試語言是C++.

從表5和圖6可以看出，與當(dāng)前主流無線安全接入認(rèn)證協(xié)議相比，在用戶規(guī)模相同的前提下，TSNP協(xié)議的通信和計算效率具有優(yōu)勢，具體分析如下：

2) 計算量.考慮到SA計算資源受限，TSNP協(xié)議將計算量交由群內(nèi)用戶和衛(wèi)星共同完成，希望通過降低衛(wèi)星端的計算開銷，提高TSNP協(xié)議的整體性能.由圖6可知，當(dāng)用戶規(guī)模逐漸增大時，協(xié)議TSNP的計算時延明顯小于協(xié)議IEEE80.211i+；表5表明，TSNP協(xié)議在SA和GU端的計算負(fù)載要明顯低于IEEE802.11i+.

因此，TSNP有效降低了衛(wèi)星的計算和通信開銷，同時減少了對地面管理中心的依賴程度.

Fig. 6 The comparison of the computation delay.圖6 2個協(xié)議SA計算時延對比

5 總 結(jié)

本文面向空間信息網(wǎng)提出了支持群組高效和安全的認(rèn)證協(xié)議-TSNP.

在認(rèn)證協(xié)議中又將協(xié)議分為3個階段：1)初始化階段地面管理中心分別與衛(wèi)星和群組的用戶共享長期密鑰，并收集了群組中用戶的相關(guān)信息GP；2)在接入認(rèn)證階段群組中的首個申請接入衛(wèi)星的用戶，經(jīng)過相關(guān)操作后，地面管理中心和用戶分別生成了會話主密鑰，并由地面管理中心將其產(chǎn)生的會話主密鑰和GP加密發(fā)送給衛(wèi)星；此時衛(wèi)星解密消息，并與剛才申請接入的用戶進行通信，各自產(chǎn)生臨時會話密鑰；3)在群組密鑰生成階段，由第1個認(rèn)證通過的用戶向群組中其他用戶發(fā)送消息，以便群組內(nèi)用戶各自生成相關(guān)密鑰.在切換協(xié)議中，僅僅與衛(wèi)星通過3次交互即可實現(xiàn)群組切換.

在PCL安全模型中分別證明了各個階段協(xié)議的密鑰機密性和會話認(rèn)證性，通過順序組合和并行組合的組合證明方法證明了組合后的協(xié)議依然滿足密鑰機密性和會話認(rèn)證性，同時協(xié)議也確保了消息的完整性.分析結(jié)果表明：使用TSNP在空間信息網(wǎng)中實現(xiàn)群組認(rèn)證和切換是高效和安全的.

[1]Mukherjee J, Ramamurthy B. Communication technologies and architectures for space network and interplanetary internet[J]. IEEE Communications Surveys & Tutorials, 2013, 15(2): 881-897

[2]Jiang Wei, Hao Huicheng, Li Yijun. Review of task scheduling research for the earth observing satellites[J]. Systems Engineering and Electronics, 2013, 35(9): 1878-1885 (in Chinese)(姜維, 郝會城, 李一軍. 對地觀測衛(wèi)星任務(wù)規(guī)劃問題研究述評[J]. 系統(tǒng)工程與電子技術(shù), 2013, 35(9): 1878-1885)

[3]Wang C, Li D, Zhou X, et al. HJ satellite based mapping technologies of land use products for emergency response of agricultural disasters[C] //Proc of the 23rd Int Conf on Geoinformatics. Piscataway, NJ: IEEE, 2015: 1-4

[4]Wooster M J, Smith T, Drake N A. Key Methods in Geography[M]. London: SAGE Publications, 2016: 423

[5]Uchida N, Sato G, Takahata K, et al. Optimal route selection method with satellite system for cognitive wireless network in disaster information network[C] //Proc of the 25th Int Conf on Advanced Information Networking and Applications . Piscataway, NJ: IEEE, 2011: 23-29

[6]Wolff R, Preusche C, Gerndt A. A modular architecture for an interactive real-time simulation and training environment for satellite on-orbit servicing[J]. Journal of Simulation, 2014, 8(1): 50-63

[7]Hilland D H, Phipps G S, Jingle C M, et al. Satellite threat warning and attack reporting[C] //Proc of IEEE AeroConf’98. Piscataway, NJ: IEEE, 1998: 207-217

[8]Jiang C, Wang X, Wang J, et al. Security in space information networks[J]. IEEE Communications Magazine, 2015, 53(8): 82-88

[9]Ahmed A, Boulahia L M, Gaiti D. Enabling vertical handover decisions in heterogeneous wireless networks: A state-of-the-art and a classification[J]. IEEE Communications Surveys & Tutorials, 2014, 16(2): 776-811

[10]Farserotu J, Prasad R. A survey of future broadband multimedia satellite systems, issues and trends[J]. IEEE Communications Magazine, 2000, 38(6): 128-133

[11]Kota S L. Broadband satellite networks: Trends and challenges[C] //Proc of IEEE WCNC’05. Piscataway, NJ: IEEE, 2005: 1472-1478

[12]Liang L, Iyengar S, Cruickshank H, et al. Security for flute over satellite networks[C] //Proc of IEEE CMC’09. Piscataway, NJ: IEEE, 2009: 485-491

[13]Cruickshank H, Mort R, Berioli M. Broadband satellite multimedia (BSM) security architecture and interworking with performance enhancing proxies[C] //Proc of the 1st Int Conf on Personal Satellite Services. Berlin: Springer, 2009: 132-142

[14]Datta A. Security analysis of network protocols compositional reasoning and complexity-theoretic foundations[D]. Palo Alto, California: Standford University, 2005

[15]Datta A, Derek A, Mitchell JC, et al. Protocol composition logic (PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007, 172: 311-358

[16]Canetti R. Security and composition of multiparty cryptographic protocols[J]. Journal of Cryptology, 2000, 13(1): 143-202

[17]He C, Sundararajan M, Datta A, et al. A modular correctness proof of IEEE 802.11i and TLS[C] //Proc of the 12th ACM Conf on Computer and Communications Security. New York: ACM, 2005: 2-15

[18]Tie Manxia, Li Jiandong, Huang Zhenhai, et al. A correctness proof of WAPI certificate authentication protocol[C] //Proc of the 3rd Int Conf on Wireless Communications, Networking and Mobile Computing. Piscataway, NJ: IEEE, 2007: 2310-2313

[19]Roy A, Datta A, Mitchell J C. Formal proofs of cryptographic security of Diffie-Hellman-based protocols[C] //Proc of the 3rd Symp on Trustworthy Global Computing. Berlin: Springer, 2007: 312-329

[20]Zhang J, Ma J, Yang C. Protocol derivation system for the Needham-Schroeder family[J]. Security and Communication Networks, 2015, 8(16): 2687-2703

[21]Jiang Y, Lin C, Shen X, et al. Mutual authentication and key exchange protocols for roaming services in wireless mobile networks[J]. IEEE Trans on Wireless Communications, 2006, 5(9): 2569-2577

[22]Feng Tao, Ma Jianfeng. The universally composable security authentication and key exchange protocol for mobile satellite communication systems[J]. Journal of Astronautics, 2008, 29(6): 1959-1964 (in Chinese)(馮濤, 馬建峰. UC 安全的移動衛(wèi)星通信系統(tǒng)認(rèn)證密鑰交換協(xié)議[J]. 宇航學(xué)報, 2008, 29(6): 1959-1964)

[23]Guo Yuanbo, Wang Chao, Wang Liangmin. Universally composable authentication and key exchange protocol for access control in spatial information networks[J]. ACTA Electronica Sinica, 2010, 38(10): 2358-2364 (in Chinese)(郭淵博, 王超, 王良民. UC 安全的空間網(wǎng)絡(luò)雙向認(rèn)證與密鑰協(xié)商協(xié)議[J]. 電子學(xué)報, 2010, 38(10): 2358-2364)

[24]Zhong Yantao,Ma Jianfeng. A highly secure identity-based authenticated key-exchange protocol for satellite communication[J]. Journal of Communications and Networks, 2010, 12(6): 592-599

[25]Chen Y W, Wang J T, Chi K H, et al. Group-based authentication and key agreement[J]. Wireless Personal Communications, 2012, 62(4): 965-979

[26]Lai C, Li H, Lu R, et al. SE-AKA: A secure and efficient group authentication and key agreement protocol for LTE networks[J]. Computer Networks, 2013, 57(17): 3492-3510

[27]Chowdhury P K, Atiquzzaman M, Ivancic W D. Handover schemes in satellite networks: State-of-the-art and future research directions[J]. IEEE Communications Surveys and Tutorials, 2006, 8(4): 2-14

[28]Nakhjiri M, Nakhjiri M. AAA and Network Security for Mobile Access: Radius, Diameter, EAP, PKI and IP Mobility[M]. New York: John Wiley & Sons, 2005

[29]Dutta A, Famolari D, Das S, et al. Media-independent pre-authentication supporting secure interdomain handover optimization[J]. IEEE Trans on Wireless Communications, 2008, 15(2): 55-64

[30]He D, Chen C, Chan S, et al. Secure and efficient handover authentication based on bilinear pairing functions[J]. IEEE Trans on Wireless Communications, 2012, 11(1): 48-53

[31]Roy A, Datta A, Derek A, et al. Secrecy analysis in protocol composition logic[M] //Proc of the 11th Asia Computing Science Conf, Secure Software and Related Issues. Berlin: Springer, 2006: 197-213

[32]Datta A, Franklin J, Garg D, et al. A logic of secure systems and its application to trusted computing[C] //Proc of the 30th IEEE Symp on Security and Privacy. Piscataway, NJ: IEEE, 2009: 221-236

Li Xuefeng, born in 1975. Associate professor at Qinghai Radio&Television University . Visiting scholar in the School of Cyber Engineering at Xidian University. His main research interests include cryptography and network security.

Zhang Junwei, born in 1982. Associate professor in the School of Cyber Engineering at Xidian University. His main research interests include cryptography and network security.

Ma Jianfeng, born in 1963. PhD, professor and PhD supervisor in the School of Cyber Engineering at Xidian University. His main research interests include computer system security, cryptography and network security.

Liu Hai, born in 1984. PhD candidate at Xidian University. His main research interests include rational cryptographic protocol, location-based privacy protection, and software defined network.

附錄A PCL預(yù)備知識

1) 協(xié)議建模

2) 協(xié)議邏輯和證明系統(tǒng)

正文中文獻[14-15]給出了PCL的邏輯語法和非正式描述的邏輯謂詞.更多協(xié)議的證明使用形式化的公式θ[P]Xφ，這是公式的含義是從某一個狀態(tài)開始公式為真θ，通過線程X執(zhí)行動作P后，公式φ的生成狀態(tài)也為真.公式θ和φ是關(guān)于時序行動某種認(rèn)定或者是對于不同主體的數(shù)據(jù)是可進入的某種認(rèn)定.θ用于聲明認(rèn)證性，φ用于聲明機密性.協(xié)議組合邏輯PCL采用標(biāo)準(zhǔn)邏輯概念，提出認(rèn)證屬性是協(xié)議動作之間的時間匹配關(guān)系，只推理誠實主體的動作即可證明攻擊下協(xié)議的安全性，并通過邏輯公理和模塊化推理方法支持復(fù)雜安全協(xié)議的組合推理，可以用來證明安全協(xié)議的認(rèn)證和機密性等安全屬性.

證明系統(tǒng)擴展了一階邏輯公理和證明規(guī)則以適應(yīng)協(xié)議動作，時序推導(dǎo)和一種不變量規(guī)則的特殊形式(誠實準(zhǔn)則).誠實準(zhǔn)則是至關(guān)重要的，它用于合并一個角色與推斷其他角色行動的事實.例如，如果A接收一個來自B發(fā)送的消息響應(yīng)，誠實準(zhǔn)則將“俘獲”A的能力去使用B的屬性來推導(dǎo)出B如何產(chǎn)生他自己的響應(yīng).總之，如果A假設(shè)B是誠實的，它將使用B的角色去推導(dǎo)出它的假設(shè).

3) 組合證明方法

PCL模型提供了2類可組合證明的方法，分別是組合證明方法和抽象改進方法.本文使用組合證明方法，抽象改進方法參見正文中文獻[14-15,31-32].

組合證明是關(guān)于子協(xié)議復(fù)合推導(dǎo)的一種方法，它首先分析組件的安全性，接著再將組件以不同的方式組合，最后分析組合后的協(xié)議中其原有組件的安全性是否被破壞.組合證明方法主要解決組合安全的2個基本問題:1)組合后協(xié)議組件的安全屬性是累加的，即順序組合；2)如果組合2種機制，他們各自服務(wù)的安全屬性不能因為任何一方而降低要求，即并行組合.

附錄B 不變量及定理2證明過程

1) TSNP.MKP不變量描述

uidi,SIDA),MAC2)}.

MID,GID,uidi,SIDA),MAC1)})),

((rg,MID,GID,uidi,SIDA),MAC2})),

SIDA),MAC2)})∧After(Receive(SA,

MID,GID,uidi,SIDA),MAC2)},Send(M,

2) TSNP.SKP不變量描述

SIDA,rSA),MAC6,MAC7)).

MAC6,MAC7))).

ΓTSNP.SKP=ΓTSNP.SKP,1∧ΓTSNP.SKP,2∧ΓTSNP.SKP,3.

3) 定理2證明過程

下面分別證明定理2會話認(rèn)證性和密鑰機密性.

當(dāng)TSNP.SKP協(xié)議被執(zhí)行，會話認(rèn)證性能夠按照以下步驟推導(dǎo)：

① 因為衛(wèi)星SA是誠實的，因此它能夠清楚的知道自己行動的順序，例如分別匹配SendMessage6，ReceiveMessage7，SendMessage8，參見式(B1)；

② 因為衛(wèi)星SA接收和驗證Message7，在前一階段必然有一個能夠計算和發(fā)送Message7的實體，這也就隱含著這個實體一定知道uski，GSK被用于MAC，以保證消息完整性，參見式(B2),(B3)；

步驟1至步驟7的結(jié)果在證明，式(B21)中體現(xiàn)，因此以衛(wèi)星為誠實角色能夠推導(dǎo)出安全屬性中的會話認(rèn)證性.

根據(jù)PCL模型相關(guān)語法、規(guī)則和公理，TSNP.SKP協(xié)議會話認(rèn)證性證明過程如下：

① 由AA1,ARP,AA4可得：

(B1)

② 由ARP,HASH3可得：

MAC4,

MAC5,

?Z.Computes(Z,HASHuski(GID,uidi,SIDA,

(B2)

③ 由HASH1可得:

(B3)

④ 由HASH4可得：

(Has(Z,uski)∧Has(Z,GSK))≡

(B4)

⑤ 由式(B4),ΓTSNP.SKP,1可得：

MAC4,

MAC5,

(B5)

⑥ 由式(B5),HASH1,φTSNP.SKP.sec可得：

MAC4,

MAC5,

(B6)

⑦ 由AA1,ΓTSNP.SKP,2可得：

(B7)

⑧ 由式(B2),(B6),(B7)可得：

(B8)

⑨ 由式(B2),(B8)可得：

(B9)

⑩ 由式(B9),HON可得：

rSA,GID,SIDA,uidi,MAC3);

uidi,MAC4,MAC5);

(B10)

GID,SIDA,uidi,MAC6,MAC7),

MAC6,

MAC7?

(B11)

GID,SIDA,uidi)?Has(Z,uski)?

(B12)

(B13)

(B14)

(B15)

(B16)

(B17)

GID,SIDA,uidi)∧Send(Z,HASHumki(rSA,

(B18)

(B19)

(B20)

(B21)

當(dāng)TSNP.SKP協(xié)議被執(zhí)行，密鑰機密性能夠按照以下步驟推導(dǎo)：

① 某一實體(衛(wèi)星或用戶)如有參與雙方的隨機數(shù)，則根據(jù)CP1可以計算出相關(guān)密鑰，在證明式(B22)中可見；

② 如果用戶和衛(wèi)星都是誠實的，則說明某一實體擁有隨機數(shù)和密鑰，而這個實體只能是衛(wèi)星或用戶，在證明式(B23)中可見；

③ 在證明式(B24)～(B28)，衛(wèi)星按照順序接收或發(fā)送消息，并且匹配消息，計算出自己所屬的密鑰；

步驟①至步驟④的結(jié)果在證明，式(B33)中體現(xiàn)，因此在TSNP.SKP協(xié)議中可以推導(dǎo)出其密鑰機密性.

根據(jù)PCL模型相關(guān)語法、規(guī)則和公理，TSNP.SK協(xié)議會話機密性證明過程如下:

① 由CP1,ΓTSNP.SKP,2可得：

(B22)

② 由式(B22),ΓTSNP.SKP可得：

(B23)

③ 由ARP,REC可得：

MAC4,MAC5)]SA

(B24)

④ 由AA1,ORIG可得：

(B25)

⑤ 由式(B24),(B25)可得：

MAC5)]SAHas(SA,rSA)∧

(B26)

⑥ 由式(B26),CP1可得：

MAC5)]SACompute(SA,Hash(umki,

(B27)

⑦ 由ARP,CP3可得：

SIDA,MAC4,MAC5)??Z.(Compute(Z,

(B28)

⑧ 由式(B28)可得：

rSA,GID,uidi,SIDA)Compute(Z,Hash(GMK,

(B29)

⑨ 由式(B28),ΓTSNP.SKP可得：

(B30)

⑩ 由式(B28),(B29)可得：

(B31)

(B32)

(B33)

由(B21),(B33)可得TSNP.SKP協(xié)議具有會話認(rèn)證性和密鑰機密性，因此定理2得證.

TSNP: A Novel PCL-Secure and Efficient Group Authentication Protocol in Space Information Network

Li Xuefeng1,2, Zhang Junwei1, Ma Jianfeng1, and Liu Hai1

1(SchoolofCyberEngineering,XidianUniversity,Xi’an710071)2(EducationTechnologyCenter,QinghaiRadio&TelevisionUniversity,Xining810008)

In space information networks (SIN), to continuously collect information and enlarge the observation range, the group aircrafts need to fast access authenticate with the satellite. Unfortunately, the existing authentications schemes cannot be applied in SIN due to its particular characteristics, such as high dynamic topology, satellite computation and limited communication resources, etc. To this end, we propose a PCL (protocol composition logic) secure and efficient group authentication protocol named as TSNP through utilizing symmetric encryption and key hierarchy. With it, the authenticated node enables other users in this group to gain the session key and realize the secure group authentication and handover. Furthermore, we analyze its security properties in PCL mode and prove its composition security based on parallel and sequential rules. As a further contribution, the experimental results indicate that TSNP can reduce not only the dependence on group management center but also the satellite’s computation and communication overhead.

space information network(SIN); group authentication; protocol composition logic(PCL); authentication; secrecy

2016-06-16；

2016-08-18

國家“八六三”高技術(shù)研究發(fā)展計劃基金項目(2015AA016007)；國家自然科學(xué)基金項目(U1405255，61472310,61372075)

TP309

This work was supported by the National High Technology Research and Development Program of China (863 Program) (2015AA016007) and the National Natural Science Foundation of China (U1405255,61472310,67372075).