８０２．１６ｅ中雙重ＥＡＰ認證的Ｒｕｂｉｎ邏輯分析

劉麗明　潘　進　王　松

摘 要：802.16是IEEE制定的無線城域網(wǎng)技術(shù)標(biāo)準(zhǔn)。作為當(dāng)今最具發(fā)展前景的無線寬帶接入技術(shù)之一，由于傳輸信號的開放性，其安全問題備受關(guān)注。802.16e標(biāo)準(zhǔn)的安全體制在802.16d安全體制的基礎(chǔ)上作了進一步的改進，不但實現(xiàn)了RSA的雙向認證，而且引入了應(yīng)用層認證協(xié)議EAP;實現(xiàn)了基于EAP的雙重認證。根據(jù)協(xié)議分析需求,首先對所選形式化分析方法Rubin邏輯進行了擴展，并用擴展后的Rubin邏輯對雙重認證模式進行分析，驗證了802.16e中的雙重認證模式的安全性。

關(guān)鍵詞：802.16；TLS協(xié)議；形式化分析；Rubin邏輯

中圖分類號：TN915文獻標(biāo)識碼：A

文章編號：1004-373X(2009)05-067-05

Rubin Logic Analysis of Double EAP Authentication in 802.16e

LIU Liming1,PAN Jin1,WANG Song2

(1.Xi′an Communications Institute，Xi′an,710106,China;2.Academy of Equipment Command & Technology,Beijing,101416,China)

Abstract：802.16 is the technical standard of wirless metropolitan network made by IEEE.Its security is paid much attention because of open features of wireless channel.The security mechanism of 802.16e makes more improvement than 802.16d.It not only achieves the mutual authentication based on RSA,but also introduces EAP protocol and dual EAP protocol.According to the requirement of protocol analyzing,Rubin logic is improved,and the dual authentication mode with Rubin logic is analysed,security of the dual authentication mode is validated.

Keywords：802.16;TLS protocol;formal analysis;Rubin logic

0 引 言

IEEE802.16無線城域網(wǎng)技術(shù)是一種新興的無線寬帶接入技術(shù),與其他接入技術(shù)相比,具有一系列顯著優(yōu)點,但由于無線信號的開放性,其面臨的安全威脅比有線網(wǎng)絡(luò)嚴(yán)重的多。隨著人們對安全問題重視程度的日益提高,并鑒于IEEE802.11無線局域網(wǎng)的設(shè)計和推廣經(jīng)驗,802.16在設(shè)計之初就充分考慮了安全問題,專門在MAC層中定義了一個安全保密子層來提供通信的安全保障。802.16d［1］發(fā)布后,文獻［2,3］都對其安全體制進行了討論,發(fā)現(xiàn)存在很多漏洞,其中最大的安全問題就是PKM密鑰管理協(xié)議的單向認證性,即只能實現(xiàn)基站對客戶端的身份認證。之后推出的802.16e［4］版本在802.16d安全體制的基礎(chǔ)上進行了改進和完善,其密鑰管理協(xié)議PKMv2不但實現(xiàn)了 RSA的雙向認證,而且引入了應(yīng)用層可擴展認證框架——EAP,并實現(xiàn)了基于EAP的雙重認證模式。雙重認證的思想符合當(dāng)前安全協(xié)議的發(fā)展方向,但關(guān)于雙重認證協(xié)議形式化分析方面的相關(guān)工作尚未收集到。為此使用形式化分析方法——Rubin邏輯驗證了雙重EAP認證的安全性,并根據(jù)協(xié)議分析需要首先對該方法進行了擴展。

1 雙重EAP-TLS認證協(xié)議簡介

可擴展認證框架EAP可以支持多種認證機制,例如EAP-MD5,EAP-OTP和EAP-TLS等。這里選擇對其中應(yīng)用范圍最廣，安全強度最高的EAP-TLS協(xié)議進行分析。TLS協(xié)議的前身是SSL協(xié)議,兩者的差別非常微小。文獻［5,6］對SSL協(xié)議的安全性進行了分析,認為該協(xié)議的安全性較高,但仍存在一些安全漏洞,例如,協(xié)議交互過程當(dāng)中存在以明文形式傳送的信息,無法標(biāo)定消息來源；預(yù)主密鑰(PMS)的來源和新鮮性得不到確認；此外,協(xié)議使用明文消息發(fā)送EAP-Success /EAP-Failure消息,沒有任何保護措施。 PKMv2中支持雙重EAP-TLS認證模式,其交互過程如圖1所示。

(1) 第一輪的EAP-TLS握手過程與一次EAP-TLS相同,基站和終端用PKMv2 EAP Transfer消息來裝載EAP消息,并且用剛剛產(chǎn)生的EIK簽名的PKMv2 EAP Complete消息來裝載EAP-Success/EAP-Failure。

(2) 第一輪認證成功后,基站和終端都擁有密鑰PMK1和EIK。終端發(fā)送用EIK簽名的PKMv2 EAP Start 消息發(fā)起第二輪認證，然后通過發(fā)送PKMv2 EAP Transfer消息進行第二輪EAP-TLS握手過程,并對每條消息用EIK進行完整性校驗。

(3) 如果第二輪的EAP-TLS認證成功,終端和基站都擁有了PKM1和PKM2,并可由此生成密鑰AK,至此雙重接入認證結(jié)束。

由于雙重EAP-TLS認證中第一輪的TLS握手交互過程與一次SSL握手過程基本相同,因此不再重復(fù)文獻［6］的工作,直接在其基礎(chǔ)上用Rubin邏輯對第二輪EAP-TLS認證展開分析,并根據(jù)協(xié)議分析需要,對Rubin邏輯進行擴展。

圖1 交互過程

2 Rubin邏輯擴展

Rubin邏輯［7］是A.D.Rubin在其博士論文中提出的一種分析安全協(xié)議的新方法。關(guān)于Rubin邏輯的詳細介紹參考文獻［7］,由于篇幅問題不再贅述。與之前的模態(tài)邏輯分析方法相比,該邏輯具有一系列顯著優(yōu)點。在此沿用文獻［6］中分析SSL協(xié)議時所使用的Rubin邏輯,并根據(jù)協(xié)議分析需求,對該邏輯擴展如下：

隨著密碼學(xué)的發(fā)展,安全協(xié)議中出現(xiàn)的一些新的密碼操作和數(shù)據(jù)類型,Rubin邏輯都無法描述和分析,例如,Rubin邏輯中沒有關(guān)于MAC校驗的相關(guān)表示和推理規(guī)則,人們使用Rubin邏輯分析協(xié)議時,大都對MAC校驗做了等同加密的簡單處理,但兩者并非同一個概念,原理和功能也大不相同。為了更好地使用Rubin邏輯對后文中安全協(xié)議進行分析,對Rubin邏輯擴展如下：

首先,定義完整性校驗值的表示方法：

MIC(X,k)：表示用完整性校驗密鑰k對消息X進行完整性校驗的值。

其次,定義以下關(guān)于完整性校驗的推理規(guī)則：

·擴展的子消息來源規(guī)則

(X,MIC(X,k))∈POSS(P)

Xcontainsx1,(k∈POSS(Q))∈BEL(P)x1fromQ∈POSS(P)

說明：P擁有消息X和X的完整性校驗值,X包含子消息x1,且P相信Q擁有消息X的完整性校驗密鑰,則P相信x1 from Q。

·簽名規(guī)則

#(k)∈BEL(P),k∈POSS(P)

LINK(N璦)∈BEL(P),Xcontainsf(N璦)

X containsx1,(X,MIC(X,k))from Q∈POSS(P)BEL(P):=(BEL(P)－LINK(N璦))∪{#(x1)}

說明：在一定條件下,消息X的子消息是新鮮的。第一個條件是P擁有未使用過的臨時值N璦；第二個條件是消息X必須包含f(N璦)；第三個條件是P擁有包含N璦消息X的完整性校驗值,且計算該值的完整性校驗密鑰是新鮮的,并被P擁有。

3 協(xié)議分析

3.1 協(xié)議規(guī)范

規(guī)范協(xié)議時所用“動作”和“推理規(guī)則”取自于文獻［7］以及上文中對Rubin邏輯的擴展。此外,根據(jù)協(xié)議定義以下函數(shù),其中前6個引用文獻［6］中的定義：

(1) Generate-keys(X1,X2,X3)

通過master-secret、客戶的隨機數(shù)和服務(wù)器的隨機數(shù)生成會話密鑰。

(2) Choose-ciphersuite(X)

從客戶提供的CipherSuite列表中選擇一個ciphersuite。

(3) Match(X1,X2)

檢查CipherSuite是否包含在Cipher- Suite列表中。

(4) Finished(P,X1,X2)

對master-secret和已發(fā)送的所有消息進行散列運算,生成Finished消息。

(5) Ske(X1,X2,X3)

對客戶的隨機數(shù)、服務(wù)器的隨機數(shù)和服務(wù)器的公開密鑰進行散列運算,生成ServerKeyExchange消息。

(6) Cv(X1,X2)

對master-secret和已發(fā)送的所有消息進行散列運算,生成ClientCertificate-Verify消息。

(7) Check-same(X)

驗證對方發(fā)送消息中的MAC完整性校驗值是否與自己生成的一致。

規(guī)范結(jié)果如下：

PrincipalC

POSS(C)={k+瑿A∞CA,{k+璫}璳－瑿A,k+璫∞C,k－璫,ciph-ersuites璫,Finished(),Generate-keys(),Match(),Cv(),EIK,PAK}

BEL(C)={#(k+瑿A),#(k－璫),#(k+璫),#((k+璫)璳－瑿A),#(EIK),#(PAK)}

Binding(C)={k+璫∞C,k+瑿A∞CA}

BL(C)=

Generate-Nonce(N璫)

Concet(N璫,ciphersuites璫)

Send(S,{N璫,ciphersuites璫,MIC((N璫,cipher-suites璫),EIK)})

Update({N璫,ciphersuites璫,MIC((N璫,cipher-suites璫),EIK)})

Receive(S,{N璼,…,HelloDone璼,MIC((N璼,…,HelloDone璼),EIK)})

Split({N璼,…,HelloDone璼,MIC((N璼,…,Hello Done璼),EIK)})

Apply(Check-same(),{MIC})

Apply(Match,{ciphersuites璫,cipher璼})

Apply-asymkey({Ske(N璫,N璼,k+璗S)}璳－璼,k+璼)

Generate-Secret(PMS)

Apply-asymkey(PMS,k+璗S)

Generate-Secret(MS)

Forget-Secret(PMS)

Apply(Generate-keys,{MS,N璫,N璼})

Apply(Cv,{MS,SentM})

Apply-asymkey(Cv({MS,SentM}),k－璫)

Apply(Finished,{Client,MS,SentMessages})

Encrypt(Finished璫,k璫s)

Send(S,Concat({k+璫}璳－瑿A,{PMS}璳+璗S,{Cv(MS,SentM)}璳－璫,ChangeCipherSpec,{Finished璫}璳璫s,MIC(({k+璫}璳－瑿A,…,{Fini-shed璫}璳璫s),EIK))

Update({{k+璫}璳－瑿A,…,{Finished璫}璳璫s,MIC(({k+璼}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Receive(S,{ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Split({ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Apply(Check-same(),{MIC})Decrypt({Finished璼}璳璼c,k璼c)

PrinsipalS

POSS(S)={k+瑿A∞CA,{k+璼}璳－瑿A,k+璼∞S,k－璼,Fi-nished(),Generate-keys(),Choosecipher-suite(),Ske(),EIK,PAK}

BEL(S)={#(k+瑿A),#(k－璼),#(k+璼),#((k+璼)璳－瑿A),#(EIK),#(PAK)}Binding(S)={k+璼∞S,k+瑿A∞CA}

BL(S)=

Receive(C,{N璫,ciphersuites璫,MIC((N璫,ciph-ersuites璫),EIK)})

Split({N璫,ciphersuites璫,MIC(N璫,ciphersuites璫),EIK)})

Apply(Check-same(),{MIC})

Apply(Choose-ciphersuites(),{ciphersuites璫})Generate-Nonce(N璼)

Generate-key-pair(k+璗S,k－璗S)

Apply(Ske,Concat(N璫,N璼,k+璗S))

Apply-asymkey(Ske(N璫,N璼,k+璗S),k－璼)

Concat(N璼,cipher璼,{k+璼}璳－瑿A,{k+璗S,{Ske(N璫,N璼,k+璗S)}璳－璼},CertificateRequest,HelloDone璼,MIC((N璼,…,HelloDone璼),EIK))

Send(C,{N璼,…,HelloDone璼,MIC璼)(N璼,…,HelloDone璼),EIK)})

Update({N璼,…,HelloDone璼,MIC((N璼,…,He-lloDone璼),EIK)})

Receive(C,{{k+璫}璳－瑿A,…,{Finished璫}璳璫s,

MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Split({{k+璫}璳－瑿A,…,{Finished璫}璳璫s,

MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Apply(Check-same(),{MIC})

Apply-asymkey({k+璫}璳－瑿A,k+瑿A)

Apply-asymkey({PMS}璳+璗S,k－璗S)

Generate-Secret(MS)

Forget-Secret(PMS)

Apply(Generate-keys,{MS,N璫,N璼})

Apply-asymkey(Cv(MS,SentM)璳－璫,k+璫)

Decrypt({Finished璫}璳璫s,k璫s)

Apply(Finished,{Server,MS,SentMessages})

Encrypt(Finished璼,k璼c)

Send(C,{ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Update({ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Fi-nished璼}璳璼c),EIK)})

3.2 協(xié)議分析

從“行為列表”BL(C)的第一個動作開始分析協(xié)議,前5個動作執(zhí)行完后,POSS(C)中增加新的元素N璫；BLE(C)中增加新的元素LINK(N璫)。Update操作使得Observer(N璫=W)(W表示所有的主體)。至此,沒有使用推理規(guī)則。下一個要執(zhí)行的動作是“行為列表”BL(S)中的Receive。即：

Receive(C,{N璫,ciphersuites璫,MIC((N璫,ciphersuites璫),EIK)})

BL(S)中的前3個動作執(zhí)行后,加入到POSS(S)中的新元素有N璫,ciphersuites璫,MIC((N璫,ciphersuites璫),EIK)；下一個要執(zhí)行的動作是：

Apply(Check-same,{MIC})

若通過MIC值校驗,此時可應(yīng)用擴展的子消息來源規(guī)則推得N璫 from C,ciphersuites璫 from C,即A相信該消息來自于C,將此結(jié)論加入POSS(S)中。然后繼續(xù)執(zhí)行之后的9個動作,執(zhí)行后,加入到POSS(S)中的新元素有N璼,k+璗S∞S,k－璗S和Ske(N璫,N璼,k+璗S)；加入到BEL(S)中的新元素有LINK(N璼),#(k－璗S),#(k+璗S),#(Ske(N璫,N璼,k+璗S))。下一個要執(zhí)行的動作是BL(C)中的第6個動作,即：

Receive(S,{N璼,…,HelloDone璼,MIC((N璼,…,HelloDone璼),EIK)})

Receive之后的2個動作被執(zhí)行后,加入到POSS(C)中的新元素有N璼,cipher璼,{k+璼}璳－瑿A,k+璗S,Ske(N璫,N璼,k+璗S),k+璼以及MIC((N璼,…,HelloDone璼),EIK)；下面要執(zhí)行的動作是：

Apply(Check-same,{MIC})

若通過MIC值校驗,此時,可應(yīng)用擴展的子消息來源規(guī)則推得N璼 from S,且消息中的其他元素均來自于S,即C相信該消息來自于S,將此結(jié)論加入POSS(C)中,此外擴展的簽名規(guī)則也被滿足,可推該消息中的所有子消息都是新鮮的,將此結(jié)論加入BEL(C)中；將k+璼∞S加入到Binding(C)中,因此C相信S,TRUST［1,2］=1。下一個要執(zhí)行的動作是：

Apply-asymkey({Ske(N璫,N璼,k+璗S)}璳－璼,k+璼)

此時,用于非對稱加密的子消息來源規(guī)則的條件被滿足,可推得Ske(N璫,N璼,k+璗S) from S,進一步對消息來源進行了確認。并且,簽名規(guī)則的條件也被滿足,可進一步確認#(Ske(N璫,N璼,k+璗S)),并將LINK(N璫)從BEL(C)中刪除。然后C繼續(xù)執(zhí)行之后的三個動作。執(zhí)行后,將PMS,MS和{PMS}璳+璗S加入到POSS(C)中,PMS和MS加入到秘密集合S中,#(PMS)和#(MS)加入到BEL(C)中。然后繼續(xù)執(zhí)行下一個動作：

Forget-Secret(PMS)

執(zhí)行這個操作后,將PMS從POSS(C)中刪除,#(PMS)從集合BEL(C)中刪除。隨后C繼續(xù)執(zhí)行之后的8個動作,執(zhí)行后將k璫s,k璼c,Cv(MS,SentM),{Cv(MS, SentM)}璳－璫,Finished璫,{Finished璫}璳璫s和MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)加入到POSS(C)中,k璫s和k璼c加入到秘密集合S中,#(k璫s)和#(k璼c)加入到BEL(C)中。Update操作將S加入到Observers (PMS)中。下一個要執(zhí)行的動作是BL(S)中的Re-ceive操作,即:

Receive(C,{{k+璫}璳－瑿A,…,{Finished璫}璳璫s,MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Receive之后的兩個動作被執(zhí)行后,將{k+璫}璳－瑿A,{PMS}璳+璗S,{Cv(MS,SentM)}璳－璫,{Finished璫}璳璫s,k+璫,以及 MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)加入到POSS(S)中,下面要執(zhí)行的動作是：

Apply(Check-same,{MIC})

若通過MIC值校驗,此時,可應(yīng)用擴展子消息來源規(guī)則推得{PMS}璳+璗Sfrom C,且消息中的其他元素均來自于C,即S相信該消息來自于C,將此結(jié)論加入POSS(S)中。此外,擴展的簽名規(guī)則也被滿足,可推得#({PMS}璳+璗S),且該消息的其他子消息都是新鮮的,將此結(jié)論加入BEL(S)中；將k+璫∞C加入到集合Binding(S)中,因此S相信C,TRUST［2,1］=1。然后S繼續(xù)執(zhí)行下一個動作：

Apply-asymkey({PMS}璳+璗S,k－璗S)

執(zhí)行此操作后,將PMS from C加入到POSS(S)中,#(PMS)加入到BEL(S)中。S繼續(xù)執(zhí)行以后的兩個動作后,將MS加入到POSS(S)中,#(MS)加入到BEL(S)中,并將PMS from C從POSS(S)中刪除,#(PMS)從集合BEL(S)中刪除。隨后繼續(xù)執(zhí)行以后的8個動作,執(zhí)行后將k璫s,k璼c,Cv(MS,SentM),{Cv(MS,SentM)}璳－璫,Finished璫,和{Finished璫}璳璫s加入到POSS(S)中,k璫s和k璼c加入到秘密集合S中,#(k璫s)和#(k璼c)加入到BEL(S)中。下一個要執(zhí)行的動作是BL(C)中的Receive操作,即：

Receive(S,{ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Receive之后的兩個動作被執(zhí)行后,加入到POSS(C)中的元素有ChangeCipher- Spec,{Finished璼}璳璼c以及MIC((ChangeC璱- pherSpec,{Finished璼}璳璼c),EIK)。下一個要執(zhí)行的動作是：

Apply(Check-same,{MIC})

若通過MIC值校驗,此時,可應(yīng)用擴展的子消息來源規(guī)則推得ChangeCipher- Spec from S,{Finished璼}璳璼c from S,即C相信該消息來自于S,將此結(jié)論加入POSS(C)中,此外擴展的簽名規(guī)則也被滿足,可推得#({Finished璼}璳璼c),將此結(jié)論加入BEL(S)中；然后繼續(xù)執(zhí)行下一個動作：

Decrypt({Finished璼}璳璼c,k璼c)

執(zhí)行后將Finished璼加入到POSS(C)中,#(Finished璼)加入到BEL(C)中,至此,協(xié)議分析完畢。

4 結(jié)果分析

通過以上分析可知,雙重EAP-TLS認證的安全性比單重EAP-TLS認證有了很大的提高。通過第二輪的認證,文獻［5，6］中提出的安全漏洞都得到了彌補。首先,原來發(fā)送的明文消息有了EIK的完整性校驗,從而可以判斷消息的來源,避免了假冒攻擊；且有了完整性保護,避免了攻擊者任意篡改明文消息導(dǎo)致的“版本滾回”等攻擊。其次,通過擴展的關(guān)于完整性校驗的推理規(guī)則可推知,PMS的新鮮性和來源都可以由EIK的完整性保護而得到確認,從而避免了攻擊者對PMS的重放攻擊和假冒攻擊。再次,從分析過程可看出,秘密信息的傳送有了加密和完整性校驗的雙重保護,其來源和新鮮性得到了雙重確認,安全強度有了很大提高。此外,如前文介紹,雙重認證中用PKMv2 EAP Complete消息來裝載EAP-Success或EAP-Failure,并對該消息進行完整性校驗,從而避免了攻擊者偽造該消息造成的協(xié)議中斷。

參考文獻

［1］IEEE P802.16-2004.IEEE Standard for Local and Metropolitan Area Networks Part 16.Interface for Fixed Broadband Wireless Access Systems,2004.

［2］Sen Xu,Manton Matthews,ChinTser Huang.Security Issues in Privacy and Key Management Protocols of IEEE 802.16.In: ACM SE'06,Melbourne,Florida,USA,2006.

［3］David Johnston,Jesse Walker.Overview of IEEE 802.16 Security.IEEE Security & Privacy,2004,2(3).

［4］IEEE P802.16e-2005.IEEE Standard for Local and Metropolitan Area Networks Part 16.Air Interface for Fixed and Mobile Broadband Wireless Access Systems,2005.

［5］Analysis of the SSL 3.0 Protocol.Proceedings of the Second USENIX Workshop on Electronic Commerce,USENIX Press,1996.

［6］李秋山,胡游君.SSL協(xié)議的擴展Rubin邏輯形式化分析［J］.計算機工程與應(yīng)用,2007,8(16):3 852-3 859.

［7］Rubin D.An Interface Specification Language for Automatically Analyzing Cryptographic Protocols.Internet Society Symposium on Network and Distributed System Security.San Diego,CA,1997.

［8］徐一兵,田緒安,樊中山.無線寬帶接入技術(shù)WiMAX802．16e［J］.現(xiàn)代電子技術(shù),2008,31(13):35-37.

作者簡介 劉麗明 女,1983年出生，碩士研究生。主要研究方向為網(wǎng)絡(luò)安全。

潘 進 男,1959年出生，教授。