顧兆軍,劉東楠
1(中國民航大學 信息安全測評中心,天津 300300)2(中國民航大學 計算機科學與技術學院,天津 300300)
飛機降落后??客C位時,向航空公司提交飛機健康管理數據、電子飛行包等關鍵數據,目前大部分機型及航空公司采用人工拷貝及GateLink的方式進行數據傳輸.隨著航電技術和無線技術的發展,Boeing等公司在新機型(如Boeing 787)中裝載了無線終端網絡模塊(TWLU,Terminal Wireless LAN Unit),即機載天線,飛機與航空公司的數字通信可以使用機載天線和布置在廊橋上的無線接入點,該過程采用802.11協議.傳統無線網絡采用有線等效加密(Wired Equivalent Privacy,WEP)及Wi-Fi保護訪問(Wi-Fi Protected Access,WPA)的加密方式,目前WEP、WPA、WPA2均被攻破.故在飛機與廊橋AP進行數據傳輸時,需要一種更安全的身份認證方式.
1985年,Victor Miller和Neal Koblitz首次提出將橢圓曲線密碼體制(Elliptic Curves Cryptography, ECC)的離散對數問題應用到加密中[1,2].因ECC不存在亞指數時間算法,在相同安全強度下具有更小的密鑰尺寸、更快的運行速度、抗攻擊性強等特點,近年來被越來越多地應用到數字簽名、身份認證及無線網絡和機載網絡中.俞惠芳等將身份混合簽密與雙線性映射結合提出了ECC身份混合簽密方案[3];周志彬等將ECC應用到了RFID身份認證中[4],以Nam J為代表的研究團隊將ECC應用到了無線網絡中,從而增強無線網絡數據傳輸的安全性[5],黃后彪將ECC與機載無線移動自組織網相結合[6],以解決機載網絡身份認證和密鑰協商的問題;李建華等對當前主流網絡安全協議的形式化驗證做出了詳細的分析[7].此外,還出現了基于零知識證明的身份認證方案,如文獻[8].
本文結合民航信息系統的特點及飛機健康管理數據、電子飛行包等數據在傳輸過程中所需的安全需求,利用橢圓曲線密碼技術,提出一種數字簽名技術,并首次提出一種用于飛機與航空公司間的身份認證方案,將該認證接入到某民航專用模擬系統中,使用SVO邏輯對該方案進行形式化驗證,確保該方案的可行性及有效性.
2.1.1 ECC相關知識
定義1. 有限域.設p是一個素數,Fp由{0,1,2,…,p-1}中p個元素構成,稱Fp為有限域.
定義2. 有限域上的橢圓曲線.有限域Fp上的橢圓曲線是由點組成的集合.在仿射坐標系下,橢圓曲線上點P(P≠O)的坐標為P=(xp,yp),其中xp,yp為滿足一定方程的域元素,為點P的x坐標和y坐標.
定義3. 階.Fp(p是素數,p>3)上一條橢圓曲線的階是指點集E(Fp)中元素的個數,記為#E(Fp).由Hasse定理知,p滿足下述條件:
(1)
在素域上,若一條曲線的階#E(Fp)=p+1,則稱此曲線是超奇異的,否則稱為非超奇異的.
定義4. ECC的離散對數問題(ECDLP).已知橢圓曲線E(Fq)、階為n的點P∈E(Fq)及Q∈
,橢圓曲線離散對數問題是指確定整數l∈[0,n-1],使得Q=[l]P成立.
定理1. ECC的加法乘法運算.
域元素的加法是整數的模p加法,即若a,b∈Fp,則a+b= (a+b) modp.
域元素的乘法是整數的模p乘法,即若a,b∈Fp,則a·b= (a·b) modp.
ECC的加法乘法運算變換如圖1所示.
圖1 ECC中加法和乘法運算Fig.1 Addition and multiplication of ECC
定理2. ECC的多倍點運算.設k為一個正整數,P是橢圓曲線上的點.稱點P的k次加為P的k倍點運算,記為:Q=[k]P=P+P+…+P.
2.1.2 ECC加密流程
1)ECC中各數據類型轉換關系如圖2所示.
圖2 數據類型和轉換約定Fig.2 Data types and transformation agreed rules
2)基于ECC的一般數據加密過程
Step1.節點A在選定的橢圓曲線EP(a,b)上找一點G作為基點.
Step2.節點A選擇私鑰k,生成公鑰K=kG.
Step3.節點A將三元組
Step4.節點B收到消息后,將明文編碼到EP(a,b)上一點M上,生成隨機數r(r Step5.節點B計算:C1=M+rK,C2=rG,并傳給節點A. Step6.用戶A接收到消息后,計算C1-kC2,結果為M. 本方案采用一種組合式偽隨機數發生器生成認證過程中所需的隨機數,該方法能有效解決隨機數中常見的“重復值”的問題,大大降低了出現相同隨機數的概率,能夠有效抵抗重 圖3 偽隨機序列生成Fig.3 Generation of pseudo random sequences 放攻擊.SEED進入隨機數發生器后,首先由雜湊函數Hv()計算后生成偽隨機序列,從該序列中任選兩個值,作為EP(a,b)的基點及倍數,進行多倍點運算,最后計算出K值,即為新的隨機數.偽隨機序列生成過程如圖3所示. 3.1.1 Gatelink數據傳輸的缺點 GateLink傳輸方式分為紅外連接及有線連接兩種方式,存在易受外部環境影響、硬件成本高等問題;人工拷貝的方式存在工作效率低、安全性差等問題.GateLink數據傳輸及廊橋AP數據傳輸方案如圖4所示. 圖4 三種數據傳輸方式示意圖Fig.4 Diagram of 3 kinds of data transmission mode 3.1.2 面向廊橋AP數據傳輸的安全需求 面向廊橋AP的數據傳輸只允許來自機載天線的連接.在應用層面,廊橋AP連接傳輸數據類型及功能單一,只用于傳輸電子飛行包等關鍵數據,且安全需求極高;該連接可以在需要時開啟,即飛機艙門開啟后開始進行數據傳輸.而傳統無線網絡,一般情況下不能隨時開啟,所有終端均可接入,傳輸數據種類多,應用廣泛,安全需求不高.故在本方案中,飛機接入網絡后,首先識別文件簽名及文件類型,拒絕非法節點接入及數據傳輸.下面對廊橋AP的安全需求進行分析,傳統無線網絡需滿足數據傳輸的保密性、完整性及可靠性,面向廊橋AP的數據傳輸還應保證認證實體的雙向認證、不可否認性及可審計性等. 1)雙向認證 在飛機與廊橋AP數據傳輸過程的認證方案中,由于傳輸的數據敏感度高、安全需求大,在身份認證過程中需要精確的辨識度,故機載天線與廊橋天線需要進行雙向認證,以防止重放攻擊及無關AP的偶然連接或惡意連接. 2)不可否認性 在數據傳輸過程中,由于傳輸數據的特殊性,需要一種技術確定數據來源及其不可否認性,即每個實體在通信過程中都要具有唯一身份標識. 3)可審計性[12] 在面向廊橋AP的數據傳輸中,要求每個實體的行為均可被追蹤到.一旦發生安全事故,可根據審計記錄追尋入侵過程. 本方案由三個認證實體組成,分別為:飛機(A)、航空公司(HK,即廊橋節點)及認證中心(CA).飛機和廊橋節點首先通過CA進行注冊,然后進行雙方認證,在認證過程中需要使用用戶唯一身份標識. 認證過程中出現的符號如表1所示. 表1 符號說明Table 1 Symbol explanation 1)簽名生成 飛機節點A生成數字簽名的方法如下: Step1. 飛機的身份為IDA,IDA的長度為ENTLA,a,b為橢圓曲線方程參數,G為在橢圓曲線上選取的基點,待簽名消息為M,選取的橢圓曲線方程為: Ep(a,b):y2=x3+ax+b (2) ZA=Hv(ENTLA‖IDA‖a‖b‖xG‖yG‖xA‖yA) (3) (4) Step3. 隨機數發生器生成隨機數k∈[1,n-1],計算橢圓曲線點(x1,y1)=[k]G Step4. 計算r=(e+x1)modn Step5. 判斷:若r=0或r+k=n返回. Step6. 計算 s=((1+dA)-1·(k-r·dA))modn (5) Step7. 判斷:若s=0返回Step 3. Step8. 消息M的簽名即為(r,s). 2)簽名驗證 機場節點B收到的來自飛機節點A的消息為M′,數字簽名為(r′,s′),驗證方法如下: Step1.判斷:r′∈[1,n-1]及s′∈[1,n-1]是否同時成立,若不同時成立,則驗證不通過. (6) Step3.計算 t=(r′+s′)modn (7) Step4.判斷:若t=0,則驗證不通過. Step5.計算橢圓曲線點 (8) Step6.計算 (9) 判斷:R=r′,若成立則驗證通過,否則驗證不通過. 3.4.1 注冊階段 當飛機節點通過機載天線與廊橋AP連接向機場進行傳輸數據時,首先要在CA注冊該節點合法,飛機節點由CA生成公鑰,并自行生成私鑰,最后通過CA向機場方證明其身份,飛機節點向CA注冊過程如下: Step1. 飛機節點由隨機數生成器生成隨機數k1,計算: V=hv(k1,IDA)·G (10) 將IDA和V發送給CA. Step2. CA由隨機數生成器生成隨機數k2,計算飛機節點A的公鑰,將飛機節點地公鑰及w傳給飛機節點. PA=V+(k2-hv(IDA))·G (11) w=k2+dCA(XPA+hv(IDA))modn (12) Step3. 飛機節點收到公鑰后,計算私鑰,并驗證公鑰的有效性. dA=w+hv(k1,IDA)modn (13) dA·G=PA+hv(IDA)·G+(XPA+hv(IDA))PCA (14) Step4. 若上述等式成立,則飛機節點注冊成功,公鑰和私鑰分別為PA、dA. 飛機節點向CA注冊后,擁有其公鑰和私鑰.公鑰由CA負責管理,其它節點可以通過CA獲得;私鑰由飛機節點自行管理,不能透漏給其它節點. 3.4.2 認證階段 當飛機到達具備廊橋AP的機場時,艙門打開后連接開始建立,飛機節點(A)、廊橋節點(B)在CA注冊成功后,開始進行身份認證,過程如圖5所示. Step1. 飛機節點向廊橋節點發布自己的身份信息IDA、公鑰PA及TA,TA為由隨機數k3經過ECC變換后的值,即: TA=k3·G (15) Step2. 廊橋節點接收到飛機節點的身份及其它信息后,將隨機數k4返回給飛機節點. 圖5 身份認證過程Fig.5 Authentication process Step3. 廊橋節點將IDB、PB及TB傳給飛機節點,TA為由隨機數k5經過ECC變換后的值,即: TB=k5·G (16) Step4. 飛機節點將生成的隨機數k6發給廊橋節點. Step5. 飛機節點、廊橋節點分別計算VB、yA及VA、yB,即 VB=PB+hv(IDB)·G+(XPB+hv(IDB))·PCA (17) yA=k3+dA·k4(modn) (18) VA=PA+hv(IDA)·G+(XPA+hv(IDA))·PCA (19) yB=k5+dB·k6(modn) (20) Step6. 驗證階段,飛機節點及廊橋節點互相發送yA及yB,結合ECC的性質,判斷: (21) 是否成立.在本階段,Ti、yi、ki均為共享參數,Vi可由CA提供的信息進行計算獲得,在驗證中,須驗證三個式子相等,若出現一方與其它兩方不相等,說明認證出現錯誤或中間人攻擊,則驗證不成功,若三個式子同時成立,則認證成功,數據傳輸開始. 4.1.1 相關規則 SVO邏輯使用MP(Modus Ponens)及Nec(Necessitation)兩條推理規則及20條公理,如下所示. 1)兩條基本推理規則 Modus Ponens:Fromφandφ?ψinferψ Necessitation:From ┠φinfer ┠Pbelievesφ 2)SVO邏輯的推理公理 A.信任公理(BelievingAxioms) Pbelievesφ∧Pbelieves(φ?ψ)?Pbelievesψ Pbelievesφ?Pbelieves(Pbelievesφ) B.消息來源公理(SourceAssociationAxioms) (PKσ(Q,K)∧Preceived{X}K-1)?QsaidX C.密鑰協商公理(KeyAgreementAxioms) D.接收公理(ReceivingAxioms) Preceived(X1,…,Xn)?PreceivedXi E.看到公理(SeeingAxioms) PreceivedX?PseesX Psees(X1,…,Xn)?PseesXi (PseesX1∧…∧PseesXn)?(PseesF(X1,…,Xn)) F.理解公理(ComprehendingAxioms) Pbelieves(PseesF(X))?Pbelieves(PseesX) (PreceivedF(X)∧Pbelieves(PseesX))?Pbelieves(PreceivedF(X)) G.敘述公理(SayingAxioms) Psaid(X1,…,Xn)?(PsaidXi∧PseesXi) Psays(X1,…,Xn)?(Psaid(X1,…,Xn)∧PsaysXi) H.仲裁公理(JurisdictionAxioms) (Pcontrolsφ∧Psaysφ)?φ I.新鮮公理(FreshnessAxioms) freshXi?fresh(X1,…,Xn) fresh(X1,…,Xn) ?fresh(F(X1,…,Xn)) J.隨機數驗證公理(Nonce-VerificationAxioms) (fresh(X)∧PsaidX)?PsaysX K.共享密鑰的對稱良好性公理(SymmetricgoodnessofsharedkeysAxioms) L.擁有公理 (HavingAxioms) PhasK≡PseesK 4.1.2 形式化分析 使用SVO邏輯對協議的形式化分析分為四個部分,即初始化假設集、預期目標、推理及證明. 1)初始化假設集 P1:Abelievesfresh(k3,k6) P2:Bbelievesfresh(k4,k5) P3:Areceived(IDB,PB,TB,k4,yA) P4:Breceived(IDA,PA,TA,k6,yB) P5:AbelievesBhas(k5) P6:BbelievesAhas(k3) P7:AbelievesBhas(PB,dB) P8:BbelievesAhas(PA,dA) P9:Bsaid(IDB,PB,TB,k4,yA) P10:Asaid(IDA,PA,TA,k6,yB) 2)預期目標 G1:A確認B是否可連通,即通信認證,可被表述為:AbelievesBsaysM. G2:A與B所發送消息的不可否認性,即AbelievesBsaidM. G3: 證明消息的雙向認證,即A與B可進行相互認證,可被表述為:AbelievesAsees(PB,k4,yA),BbelievesBsees(PA,k6,yB). G4:A要確認B發送的消息與近期對話有關,并確定消息及密鑰的新鮮性,即B近期發送的消息M,且M中含有A剛剛產生的消息,即實體認證,可被表述為:Abelieves(BsaysM∧fresh(k5)). 3)推理和證明 G1:通信認證 (Abelievesfresh(IDA,PA,TA,k3,k6,yB)∧Asaid(IDA,PA,TA,k3,yB))?Asays(IDA,PA,TA,k3,yB). by P2,P10,Nonce-verificationAxioms. 同理可推,B says (IDB,PB,TB,k4,yA) by P1,P9,Nonce-verificationAxioms. G2:消息的不可否認性 AbelievesBsaid(IDB,PB,TB,k4,yA) by P11,BelievingAxioms,SourceassociationAxioms. 同理可推,BbelievesAsaid(IDA,PA,TA,k6,yB). by P12,BelievingAxioms,SourceassociationAxioms. G3:雙向認證 Areceived(IDB,PB,TB,k4,yA)?AreceivedM AreceivedM?AseesM by P3,ReceivingAxioms,SeeingAxioms. 同理可推,BseesM,by P4,ReceivingAxioms,SeeingAxioms. G4:消息及密鑰的新鮮性 由G1可得,AbelievesBsaysM. 故,Abelieves(BsaysM∧fresh(k4,k5)). by P2,G1 同理可推,Bbelieves(AsaysM∧fresh(k3,k6)). by P1,G1 通過上述分析,本方案在完成實體通信的同時(G1),可以實現消息的不可否認性(G2)、雙向認證(G3)以及確保密鑰的新鮮性(G4),從而有效地抵御惡意節點的接入及攻擊,確保了方案的可行性和有效性. 4.2.1安全性分析 1)抗重放攻擊 為有效避免重放攻擊,本方案在認證時采用“非重復值”的方式,飛機節點或廊橋節點均由隨機數生成器中產生不同的隨機數ki.若攻擊者向參與認證階段的節點發送隨機值,該節點將對該值進行驗證,計算yi,若驗證不成功,則認證失敗,故本方案能有效防止重放攻擊.目前常見的防止重放攻擊的手段還有添加序列號及時間戳,添加序列號要求參與認證的節點保存所有狀態信息,需要消耗一定的系統資源,而時間戳要求雙方時間保持嚴格一致,這在跨時區飛行中具有一定的困難度,故不適合民航領域. 2)雙向認證 3)不可否認性 為提高在面向廊橋AP數據傳輸的不可抵賴性,在身份認證過程中,不同階段的消息在傳輸時使用不同隨機數進行加密,任一實體具備唯一身份標識IDi,形式化證明表示,本協議具備消息的不可否認性. 4.2.2 效率分析 本節結合提出的身份認證協議,將其應用到TWLU數據傳輸過程,使用Cpp和tcl語言在NS2軟件對TWLU數據傳輸原型系統中的身份認證過程進行實驗仿真,并與近年來提出的相關方案進行對比,探究提出的方案在TWLU數據傳輸中的運行效率以及在民航領域的適用程度,TWLU數據傳輸原型系統所使用的網絡結構如圖6所示. 圖6 網絡拓撲結構示意圖Fig.6 Diagram of network topology 本節對近年來身份認證領域相關研究進行了比較,在如圖6所示的網絡結構中,對文獻[9-11]進行仿真模擬,從安全需求、算法通信成本及算法效率等方面對協議進行了比較分析.安全需求方面,考慮認證方案在抗重放攻擊、雙向認證、不可否認性及密碼強度的實現情況;算法效率方面,對比了協議雙方的通信次數(EC)、雜湊運算次數(EH)以及完整協議的運算次數(EP),實驗結果如表2、表3所示. 表2 身份認證協議安全性對比Table 2 Security comparison 實驗分析表明,文獻[9]不能滿足TWLU數據傳輸過程所需的抗重放攻擊及雙向認證,且使用隨機數數量過少,不能保證其安全強度;文獻[10]提出的抗重放攻擊過于理想化,且忽視了密碼強度問題;文獻[11]不能有效抵御重放攻擊.由4.2.1節可知,重放攻擊是TWLU數據傳輸過程的重要威脅,選擇具有“非重復”特性的隨機數生成方案十分必要.綜上,文獻[9-11]不能滿足TWLU數據傳輸過程中的全部安全需求,故不適用于該領域,而本文所提出的算法能夠滿足該過程所需的安全需求,具備較強的安全性,在該領域有著較好的應用. 表3 身份認證協議效率對比Table 3 Efficiency comparison 從安全性及效率兩個方面可以得到如下結論: 結論1.相比其它方案,提出的認證協議具備更強的安全性能,可以抵御重放攻擊、實現雙向認證、具備不可否認性; 結論2.運算效率方面,提出的方案減少了協議的交互次數和運算次數,在雜湊函數運算次數與其它方案持平. 實驗結果表明,提出的方案在民航專用系統中的模擬,安全性能優于其它方案,同時減少了協議運行過程中的交互次數運算次數. 本文以機載天線和廊橋AP間使用無線網絡進行數據傳輸為背景,以橢圓曲線密碼體制為基礎,首次提出一種用于該過程的身份認證方案,解決了飛機與廊橋間沒有統一的認證方案的問題.提出一種新的隨機數生成方案,在認證的不同階段使用不同的隨機數以保證密鑰的新鮮性,從而有效抵御重放攻擊;同時,本方案還實現了雙向認證,能有效防御惡意節點或偽基站的非法接入.使用SVO邏輯分析表明,本方案可以滿足該數據傳輸中的安全需求;實驗表明,本方案的通信消耗適中,無極端值,安全性能達標,且更適用于民航領域,即面向廊橋AP數據傳輸及其身份認證過程.在未來的工作中,進一步優化時間戳算法,將該技術應用到TWLU數據傳輸數字簽名和身份認證中.2.2 偽隨機序列
3 身份認證方案
3.1 數據傳輸的安全需求
3.2 認證實體
3.3 數字簽名
3.4 身份認證過程
4 形式化驗證及分析
4.1 基于SVO邏輯的形式化證明
4.2 安全性能及效率分析
5 結束語