三方認證密鑰協(xié)商協(xié)議形式化安全模型的分析與改進

1、三方認證密鑰協(xié)商協(xié)議形式化安全模型的分析與改進摘要：木文對兩個三方認證密鑰協(xié)商協(xié)議的形式化安全模型一一擴展br模型和擴展ck模型進行了分 析，發(fā)現了擴展br模型中在三方身份認證方面存在的安全漏洞，指出了擴展ck模型中兀配會話定義的局 限性，并根據802.1 li所規(guī)范的協(xié)議流程，通過引入有效ap的概念，提出了三方認證密鑰協(xié)商協(xié)議改進的 形式化安全模型，并在該模型下證明了改進后eap-tls協(xié)議的安全性。新模型為解決無線局域網等特定環(huán) 境下認證密鑰協(xié)商協(xié)議的安全性問題提供了較好的解決思路。詞：802.hi； eapi辦議；可證明安全性；三方形式化安全模型1引言2004年ieee 802.11標準

2、組提出了802.11i標準以增強無線局域網的安全性能。在該標準中，客戶端的 認證和接入控制功能是通過802.1x協(xié)議實現的，而802. ix協(xié)議的認證功能是通過上層認證協(xié)議eap完成的， 因此對eap協(xié)議的安全性進行研究就顯得十分重要。然而，目前針對802.1 li的三方認證協(xié)議研究還沒有完 善的形式化安全模型，1995年bellare等人提出了三方密鑰交換的形式化安全模型，但此模型沒有考慮實 體間的認證關系。2008年曹春杰提出了擴展的ck模型，給出了三方認證密鑰協(xié)商協(xié)議的形式化模型， 但該模型中關于接入點ap會話標識符sm的定義因為存在不確定性而并不實用（事實上文獻3中也并沒 有給出具體的

3、協(xié)議并利用該模型進行證明）。2010年宋宇波等人提出了擴展的br模型，該模型利用參與 方產生的會話序列對匹配會話進行定義，但由于沒有考慮接入點ap在一-次協(xié)議中產生的兩條會話序列之 間的關系，因而該定義有可能會導致三方消息認證不安全。因此，如何對三方認證密鑰協(xié)商協(xié)議的形式化 安全模型進行改進與完善，使其能保證無線局域網的參與方可以進行安全認證還需要進一步的深入研究。本文通過對現有三方認證密鑰協(xié)商協(xié)議形式化模型進行深入分析，指出利用匹配會話定義三方協(xié)議的 認證關系吋需要考慮特定的應用背景，這是因為交互的三方中至少有一方要與其它兩方同吋進行消息交 互，対于這一方的會話描述（無論是用會話序列或是會話

4、標識符）必須考慮其自身所處的網絡位置和所具 備的網絡功能，否則一旦攻擊者對該方進行冒充或破壞，就可能造成匹配會話定義的失效。對于802.hi而 言，4p作為client和4s中間具有轉發(fā)功能的參與方，其與client和as的交互內容有一定的重復性， 本文根據這一重要特點，在改進的形式化安全模型中給出ap會話標識符有效的定義。802.11 i協(xié)議流程如圖1所示：圖1 802. hi協(xié)議流程客戶端加通過無線網絡與接入點4p進行連接，ap通過有線網絡與認證服務器as進行連接， ap的功能是接收消息后進行加脫密操作并轉發(fā)消息，as的功能是對client進行認證。802.hi協(xié)議中 client和as通

5、過ap轉發(fā)響應各自的身份、加密方式、公鑰等相關信息，然后由c"幼/發(fā)起eap認證協(xié) 議。設client有一對公私鑰（pkc,skc）, as有一對公私鑰（pks,sks）, ap與4s間共享長期對稱 密鑰k o eap-tls協(xié)議的目的是通過一系列的交互使客戶端與認證服務器間協(xié)商主會話密鑰msk ,并實 現相互的身份認證。eap協(xié)議完成后as將協(xié)商得到的msk通過加密的方式發(fā)送給ap.然后client與 ap利用msk進-步完成四步握手協(xié)議。在本文中，三方認證密鑰協(xié)商協(xié)議指eap協(xié)議，山于eap是完成認證和主會話密鑰msk協(xié)商的核心 步驟，所以改進的形式化安全模型也是建立在802.1

6、 li所規(guī)范的eap環(huán)節(jié)上。2現有三方認證密鑰協(xié)商協(xié)議安全模型分析本節(jié)我們簡要回顧文獻4和文獻3中提出的擴展br模型和擴展ck模型。通過分析發(fā)現，擴展的br 模型中關于匹配會話的定義可能會導致消息認證不安全，不能抵抗攻擊者對client的冒充攻擊。在擴展的 ck模型屮，當攻擊者冒充ap時會導致ap會話標識符定義的失效。2.1擴展br模型及安全性分析文獻4中擴展br模型將三方認證密鑰協(xié)商協(xié)議形式化為一個四元組p = 5©（p,ll）來描述。英中，兀 定義了一個誠實客戶端的會話行為，0定義了一個誠實接入點的會話行為，0定義為誠實認證服務器的會 話行為，zz為認證服務器分發(fā)給客戶端和無線接

7、入點的初始會話密鑰。該模型將攻擊者形式化為擁有黑 盒預言機和心 的概率圖靈機，且可以對這些預言機進行預定的查詢并從預言機那里獲得應答。為了描述參與方之間的認證關系，文獻4在原br模型兩方認證安全的基礎上進行了擴展。在原br模型 中，若兩條會話序列分別是對方的匹配會話，則稱這兩條會話序列是匹配會話。在擴展br模型中，這種匹 配會話的定義被直接推廣到了三方的情況：設預言機為疋、0：以及硏,$,產生的相應會話序列分別用 c1,ct和c2,c2'表示，則在擴展br模型屮，三方之間的匹配會話和消息認證安全的定義如下：定義1 如果c1是c1'的匹配會話，ct也是c1的匹配會話；c2是c2&

8、#39;的匹配會話,c2'也是c2的 匹配會話，則稱預言機疋之間有匹配的會話。當一個協(xié)議p在攻擊者的控制下執(zhí)行，如果 存在一個沒有被攻破的預言機呈接受狀態(tài)，但沒有一個與它有匹配會話的預言機存在的時候，稱這樣的會 話是不匹配的。定義2如果不匹配會話的概率是可忽略的，則稱協(xié)議p是消息認證安全的。定義1分別給出了 client與ap , ap與as之間會話的匹配關系，但是卻忽略了這兩者之間的相關性, 也就是說攻擊者對以通過重放某次協(xié)議中的一個匹配關系構造出滿足定義1的匹配會話使三方都接受。因 此通過上述匹配會話給出的認證安全的定義2至多只能提供client和ap, ap和as之間的認證，卻不

9、能 保證ap與4s之間的認證，這樣就不能實現802.1 lil'eap-tls協(xié)議的目的（提供客戶端和認證服務器的雙 向認證）。為了便于說明舉例如下：a ap as(1)c1cvc2ct人是協(xié)議的合法參與方，與正常的ap, as進行一次會話后得到匹配會話cl, c11,c2, c2 ap as(2)clcr c4c4人是攻擊者，通過重放(1)中的會話與正常的ap, as進行一次會話后得到相應的會話cl, cr, c4, c4由于cl, ct是匹配會話，c4, c4'是ap與4s完成的一次正常交互，因此同樣是匹配會話， 那么根據定義1有cl, cr, c4, c4是一個匹配會話，

10、但此時ap, as均認為攻擊者心的正確身份 是人。這說明在文獻4中擴展的br模型關于消息認證安全的定義有一定的局域性，為了避免因此造成的 安全漏洞，有必要對其進行改進。2.2擴展ck模型的定義缺陷2008年曹春杰基于ck模型，提出了支持三方協(xié)議的形式化安全模型一一擴展ck模型。該模型通過 會話標識符sid來定義匹配會話。定義3門】令sid為會話標識符，普片為協(xié)議參與方的身份，role e client, ap, as為參與方在 協(xié)議中的角色。設在三方認證協(xié)議p的一次執(zhí)行中，乙生成會話(ppf d/oh), 生成會話 (pj,pi，p“sidj,rolej),人生成(無，用,p,sidk,rol

11、ek),如果有 sidi = sidj = sidk，且 role., rolej,rolek 互不相同，則我們稱這三個會話是匹配會話。利用會話標識符sm定義匹配會話比通過會話序列定義更簡潔有效。但該模型與ck模型一樣，并沒有 給出sm的具體定義，只是簡單地將兩方的情況推廣至三方，而沒有考慮sid定義的存在性和確定性。擴 展的ck模型同樣是基于無線局域網而設計的。該模型假設協(xié)議止常執(zhí)行的情況下，包括敵手在內的任意會 話omcb在執(zhí)行后都生成相應的sid,并基于此定義兀配會話。但我們通過分析發(fā)現，當攻擊者對ap進 行冒充時可能造成會話標識符sid具有不確定性，如下例所示：ek messagex&

12、#39;) asek (niessaget)ek (messaged')clienl 加wssdgwl. 4pmessage!' messaged假設敵手通過消息重放等手段完成了以上會話實例，按照定義和as分別生成會話標識符 sidc = h(messaged ii message2' messaged), sids = hmessagevw message! ii messaged*)。由于 協(xié)議執(zhí)行中ap涉及接收并發(fā)送多個不同消息(messagex , messagei' , message! , message!' , messaged , mes

13、saged'),因而此時對ap會話標識符sida的定義可以有多種選擇，例如nf以設 sid人=h(messagel ii message!'ll message3)或 sid« = h(messagel ii message!'ll messaged'), 這就 造成sma定義具有不確定性。而事實上，sid的作用是對協(xié)議的某一次會話做特定的標識，應當具有唯一 性，因此在上述情況下，擴展ck模型關于兀配會話的定義顯然是不合理的。為了解決上述問題，需對802.111 的協(xié)議流程進行進一步分析，根據ap的功能對會話標識符定義進一步完善。3改進的三方認證密鑰協(xié)

14、商協(xié)議形式化安全模型我們在對擴展br模型和擴展ck模型分析的基礎上，提出了改進的三方認證密鑰協(xié)商協(xié)議形式化安全模 型。該模型充分考慮了 ap的功能和特點，通過引入有效4p的概念，解決了三方身份認證中匹配會話定 義不完善和不確定的問題。在該模型下可證安全的三方eap協(xié)議可以實現client與as的交互認證且能保 證主會話密鑰msk安全，因而對802.11i中eap協(xié)議的設計與分析有著重要的意義，對該模型的詳細描述 如下：3.1敵手能力由于802.lli協(xié)議中的認證環(huán)節(jié)是采用完整的加密或簽名算法來實現的，所以新模型并不適合假設敵手 可以通過某種方法得到參與者的長期密鑰或者臨時密鑰，因為這種假設會直

15、接導致敵手對用戶消息的簽名 偽造或者加脫密。在本模型中對敵手的攻擊能力假設如下。client. as分別擁有自己的公私鑰對，此外ap . as之間共享一對長期對稱密鑰。攻擊者可以竊聽、 篡改、轉發(fā)、刪除、偽造、嵌入三方之間交互的消息，具體地可以將敵手能力形式化為以下對預言機的查 詢：execute查詢：攻擊者可以對client、ap、as進行execute查詢。當進行execute(role,u)查詢時， osch返回參與方廠。滄的第u次會話的會話實例。此查詢模擬被動攻擊，即敵手具有獲得大量會話實例的 能力。smd查詢：攻擊者可以對client、ap、as進彳亍s幼d查詢。當進行send (r

16、ole,u,m )查詢時，攻 擊者發(fā)送消息m給參與方"滄的第"次會話，oracle根據協(xié)議的約定執(zhí)行，并返冋給敵手相應的執(zhí)行結 果。此詢問模擬主動攻擊，描述敵手進行消息的偽造、重放、篡改等對消息進行修改操作的能力。在802.lli所規(guī)范的協(xié)議流程中，client和4s協(xié)商生成主會話密鑰msk ,并由4s將msk加密后發(fā) 送給ap.為了使模型簡單且易于分析，可以合理的假設msk的安全性僅依賴于認證協(xié)議的安全性，對 于as將msk加密后發(fā)送給ap這一步驟并不計算在認證密鑰協(xié)商協(xié)議中，且認為英不泄露msk的任何 信息。因此對reveal查詢定義如下：reveal查詢：攻擊者可以對

17、client和as的會話進行reveal查詢，當進行reveal (role, u)查詢時， role( client或as)所對應的會話實例u返回給攻擊者本次會話生成的會話密鑰。此攻擊形式化了敵手進 行相關密鑰攻擊的能力。查詢：攻擊者只能對沒有被進行過reveal查詢且已經完成的client或as的會話進行test詢問。 敵手s進行一次隨機擲幣，如果擲幣結果b=0,則返冋給敵手msk；如果b=l,則返冋給敵手一個隨機數 r (取自主會話密鑰msk空間)，但敵手不知道擲幣的結果，他根據返回值做判斷，輸出，用prb = b' 表示敵手猜對的概率，用aclv = prh = h,-/2表示

18、敵手的優(yōu)勢，根據不可區(qū)分性理論，如果ad眄的 值是可忽略，那么敵手不能得到會話密鑰的任何信息。我們稱具有上述4種能力的敵手為3ake敵手。上述対敵手的形式化描述僅限于此三方協(xié)議是利川加脫 密算法和簽名算法進行設計的情況，因此不適合假設敵手具有很強的攻擊能力。但是如果在此模型下的協(xié) 議是利用困難問題進行設計的，則可以進一步考慮敵手得到長期密鑰和臨時密鑰的能力，從而得到基于 eck2007模型的三方擴展模型。3.2安全性定義在對擴展br模型分析后發(fā)現，通過交互消息產生的會話序列來定義匹配會話具有一定的局域性，這是 因為在三方協(xié)議中，ap在與client進行消息交互的同時也與as進行消息交互，所以會

19、話序列很難將ap 與另兩方的會話都刻畫清楚，因此在改進的模型中我們通過會話標識符sid來定義匹配會話。由于ap的 功能主要是消息的加脫密和轉發(fā)，這意味著會話(1)中的ct, c2的消息內容有著明顯的關聯和重復性， 我們可以利用這種關聯引入有效ap的概念，通過有效ap將ap與client. ap與as之間的會話聯系起來，進而給出三方匹配會話的定義。定義4設ap與as之間共享密鑰k、加密算法e和相應的脫密算法d,如果在時刻q, ap接收到 來自client的消息messaged,在緊鄰的下一個時刻r,發(fā)送給4s消息ek(messagev),在時刻q接收到 來自as的消息ek message!),在

20、緊鄰的下一個時刻r3發(fā)送給client消息message!'，且有 (message! ii message!') = messagevw message!),則稱 ap 是有效的。會話標識符sid是協(xié)議參與方在接受后生成的用于標記此次會話的標識，具體定義為參與方執(zhí)行過程 中接收和發(fā)送消息內容的串接。不妨設參與方client . ap . 4s接受后生成的會話標識符為 sid°si(l八，sid$，英中client與as的會話標識符sidc,sids與ck模型類似，對于ap執(zhí)行過程中重復出 現的消息內容僅在計算在此次會話的$加八時使用一次。根據上述定義可以得到如下性質

21、。性質1對于一次正確會話的參與方client > ap. as,在協(xié)議完成后oracle云":用分別生成相 應的會話標識符sidcsid,2叫，如果ap是有效的，則有sidc - sida - sids。證明 設cdn為ap與client會話消息的串接。如果協(xié)議執(zhí)行過程中沒有攻擊者的參與，且各方都順利 完成了會話過程，(即是止確會話)，那么有sid(：二sma。由ap有效性的定義可知 (messagel ii message!') = (messagel * ii message!),其中 mess a gelmessage!為 ap 與 as 交互的消 息內容，據此可

22、以定義as的會話標識符"ds。同理可知，當協(xié)議正確執(zhí)行時有sicla = sids,于是性質1 成立。性質2對于不是有效ap參與的協(xié)議會話oracle云,兀：,在全部接受后生成會話標識符 side>sih,sids，則必然有sidc 工sids。證明 若ap不是有效的由定義可知(messagel ii message! *)工(message' ii message!),所以 messagel h message!'或 messagel h message!',不妨設 messagel h messagel1,因為在某個時刻片, ap接收到消息messa

23、gel，則必然在時刻g由疳發(fā)送過消息message,所以sidc 111包含message； 如果在某個吋刻t.f, ap發(fā)送過消息message',則必然在吋刻r;+1由譏接收到消息messagel',所以 sids 中包含 messagel',由 messagel 工 messagel'可知 sidc 豐 sids。以下給出改進后安全模型下關于匹配會話和認證密鑰協(xié)商安全的定義：定義5如果對有效的4p參與的會話在執(zhí)行后，參與的三方oracle都接受會話ii生成的會話標識符sidc = sida = sids,則稱云疋，譏是匹配會話。定義6稱802.1 li規(guī)范

24、下的eap-tls協(xié)議是三方認證安全的，如果該協(xié)議滿足以下三條：如果打，龍;，斗是匹配會話，則對應的oracle都接受；(2) 如果oscb對,兀；,成都接受，則打，龍;是匹配會話；(3) 對于無效ap參與的協(xié)議，不存在會話使osch云或兀；接受。定義7稱802.11i規(guī)范下的eap-tls協(xié)議是msk安全的，如果對任意3ake敵手滿足以下兩條：協(xié)議執(zhí)行后client. as生成相同的msk ；(2) 敵手優(yōu)勢ad屹是可忽略的。4 eap-tls協(xié)議及其安全證明為進一步驗證改進后安全模型的有效性和合理性，我們提岀一個適用于802.1 li的新eap-tls協(xié)議，并 利用所提出的新三方認證密鑰協(xié)

25、商形式化安全模型對英進行證明。crapear)as ,sigsks(r、epkc(msky)ek(sigsks(r，epkc(msk)sigskc(mmsk)ek(sigskc(h(msk新的eap-tls協(xié)議協(xié)議的執(zhí)行過程如下：client收到eap-start請求后，隨機生成/?并發(fā)送給ap , ap對尺進行加密后 轉發(fā)給as； asli密鑰空間中隨機生成msk利用emi密后與r起進行簽名，將簽名后的結果加密后 發(fā)送給ap , ap脫密后轉發(fā)給client: client對簽名進行驗證(檢查r是否相等)，并利用自己的私鑰對 e'pkc(msk)脫密得到msk , client對ms

26、k進行雜湊并用自己的私鑰簽名后發(fā)送給ap ,然后client接 受，ap隨后加密轉發(fā)給as ； as對ek(sigskc(hmsk)進行脫密操作后對msk進行雜湊并驗證其是 否為簽名內容，若驗證通過as接受。c竝m和as協(xié)商得主會話密鑰msk , sidc = sida = sids = h(r ii 隅冏(r，epkc(msk) ii sigskc(h(msk)。定理1如果簽名算法sig是不可偽造的，則上述協(xié)議是三方認證安全的。證明只需要證明上述新eap-tls協(xié)議滿足定義6中的三條即可。對于定義的第一條易知在協(xié)議正常執(zhí) 行的情況下，ap滿足有效性的定義，此吋若龍；,龍;，龍；是匹配會話，則

27、由性質1有sig二sid八二sids， 顯然三方都會接受。下面我們證明協(xié)議滿足定義6的第二條：對于有效ap參與的協(xié)議，要使三方osc滄都接受，則sic中 一定包含消息sigsks(r，epkc(msk)使得osch疳接受。同樣對于認證服務器as , s%中一定包含 消息ek(sigskc(h(msk)使osch兀：接受。由于簽名算法是不可偽造的，所以攻擊者不可能構造出這 樣的簽名，則這兩個簽名必然是由ap轉發(fā)的，這說明ap曾接收到消息ek(sigsks(r，epkc(msk)和 sigskcwmsk)。又山長期密鑰k的保密性和簽名算法的安全性可知，攻擊者同樣不能対這兩條消息進 行偽造，因此as

28、曾發(fā)送過消息ek(sigsks(r，epkc(msk), client曾發(fā)送過消息sigskc5(msk)。 綜上所述，各osc/w包含的消息如下：打 包含消息 sigsks(r，epkc(msk、sigskc(h(msk)；兀:包含消息 sigsks(r,epkc(msk). ek(sigsks(r，epkc(msk)、sigskcwmsk)、ek(sigskc(h(mskm :朮包含消息 ek(sigsks(r，epkc(msk)、ek(sigskc(h(msk),因此有 sidc =sida = sids ,于是 對，疋，卅 是 匹配會話。最后我們證明當參與協(xié)議的ap非有效時，不存在會話

29、使三方都接受。利用反證法不妨假設存在會話 云疋"i使三方都接受，則接受后的會話生成相應的會話標識符 sidc =/(/? ii sigsks (r，epkc(msk) ii sigskc(hmsk), sids = h皿(r ')wek (sigsks(r ； pkc(msk') ii ek (sigskc (h(msk *)由性質2可知，當ap非有效時有sidc豐sids,則必然有r工卍或者是msk豐msk'。對于前一種情 況意味著攻擊者可以對認證服務器as的簽名進行偽造，第二種情況意味著攻擊者可以對client的簽名進 行偽造，這顯然與簽名算法的安全性相矛

30、盾，因此該協(xié)議滿足三方認證安全定義的三個條件。定理2如果雜湊函數力是安全的，加密算法e和e'是安全的，簽名算法sfg是不可偽造的，則上述協(xié) 議是msk安全的。證明設攻擊者進行北“查詢后猜測擲幣結果成功的概率為pr/ = b,我們分別對敵手三種不同的攻 擊方式構造區(qū)分器。(1) execute查詢：假設攻擊者可以進行乞次execute查詢，用prb ' = b表示敵手利用此類查詢猜測 b' = b成功的概率。攻擊者利用此查詢獲得關于msk信息的有效方式是通過和h(msk)來 進行計算的，我們對此做如下實驗。實驗1：挑戰(zhàn)者進行一次隨機擲幣勺| ,若結果為 =0則返回給攻擊者

31、eikc(msk),若結果為 % = 1則隨機選擇r w g(g為msk空間)返回給攻擊者e'pkc(r),攻擊者根據返回的結果猜測挑戰(zhàn)者擲 幣的結果為% ,令prb= % 表示攻擊者猜測正確的概率。實驗2：挑戰(zhàn)者進行一次隨機擲幣如，若結果為b2=0則返冋給攻擊者/z(msk),若結果為bl2= 1則 隨機選擇reg(g為msk空間)返回給攻擊者/i(r),攻擊者根據返回的結果猜測挑戰(zhàn)者擲幣的結果為 bj,令= %表示攻擊者猜測正確的概率。在實驗1中，由于算法e'是安全的，攻擊者至多進行/次execute查詢，則敵手通過此查詢贏得實驗 1的概率prbii, = bn<qc

32、/go同理在實驗2中，由于雜湊函數力是安全的，因此敵手通過execute查詢 贏得實驗2的概率prbi21 = bn<qe/g,因此(2) send查詢：假設攻擊者可以進行qs次send查詢，用pr/721 =方表示敵手利用此查詢猜測夕=b成 功的概率。事實上，攻擊者能否利用swnd查詢得到msk的信息等同于攻擊者能否對簽名進行偽造。因 此我們構造攻擊者對簽名的偽造實驗仏：實驗對于給定的參數r, s«z?d查詢做出后，攻擊者隨機生成mskwg,并由as的密鑰空間 中隨機選擇sks、,構造簽名sigsk(r，e'pkc(mskj),山于攻擊者至多進行依次s幼d查詢，不妨假

33、 設攻擊者利用此方法構造了一個具有依個簽名的列表厶：msk、 mskt mskqssigsks、(r，e、kc(mskj) si£sksr，e'pkc(mski sigsksr，e'pkc(msg在實驗人中，如果第i次查詢的簽名屬于列表厶，則返回給攻擊者相應的主會話密鑰msk,否 則返回“丄”。實驗舛：同實驗a類似，smd查詢做出后，攻擊者隨機生成msk g g ,并由c"刃"的密鑰空間 中隨機選擇skc、,構造簽名sigskc'h(mskj),由于攻擊者至多進行依次smd查詢，不妨假設攻擊 者利用此方法構造了一個具有qs個簽名的列表l2:

34、msk,.msk,.a/sk“、1jsigskctwmskj) sigskc(h(mskt)si&kjgmskq)在實驗舛中，如果第i次s幼d查詢的簽名屬于列表厶2，則返回給攻擊者相應的主會話密鑰msk”,否則返回“丄”。設client和as的密鑰空間為則攻擊者利用實驗1偽造成功的概率為qjn ,利用實驗2偽造成 功的概率為/(amgi),因此prh2' = h2 = prsigsks(疋厶+ prsigskc() w 厶 <么 /(nig i) + 你 /n(3) reveal查詢：設攻擊者可以對當前攻擊實例外的其它乞個會話實例進行reveal查詢，返冋給攻擊 者被查詢

35、會話生成的主會話密鑰msk。市于每次會話的msk都隨機獨立的選取，因此攻擊者利用此查 詢猜測test查詢擲幣結果成功的概率prb/ = b3<qr/g o綜上所述，攻擊者對北w查詢擲幣結果猜測成功的概率prb* = /? = prb'=勺+ prz?2* = /?2 + pr&3* = z?3< 2qe/g +qs /(am g i) + 么 /n + 乞 /g因此該協(xié)議是msk安全的。5小結本文在802li的協(xié)議規(guī)范下，根據4p所具有的特定功能和實際應用中的一些特點，給出了有效ap的 概念，并利用其給出了此類模型的兩個基本性質。并通過將其應用于具體的eap-tls

36、協(xié)議的安全性證明中, 說明了該模型具有一定的合理性和適用性。本文所提出的三方模型主要考慮了無線局域網這一特定的應用 背景，對于其它三方環(huán)境并未做細致的研究。在下一步工作中，可以針對其它有特定應用背景的三方協(xié)議 對形式化安全模型進一步研究，并可以假設敵手具有更強的攻擊能力來建立新的模型，在此類新模型下， 可以利用數學困難問題設計更高效的安全認證密鑰協(xié)商協(xié)議。參考文獻11 ieee802.1 li. ieee standard for information technology-telecommunications and inform ation exchange between system

37、s-local and metropolitan area networks-specific requirements part 1 1: wireless lan medium access control (mac) and physical layer( ph y)specifi cations: medium access control(mac) securityenhancementss. america,iso/iec,2004:1341.2 m bell are and p rogaway. provably secure session key distribution-t

38、he three party case a. proc. 27th annual symposium on the theory of computingc. acm,2005:57一66.3 曹春杰.可證明安全的認證及密鑰交換協(xié)議設計與分析.西安電子科技大學博士學位論文.2008.4 宋宇波，胡愛群，姚冰心.802.hi認證協(xié)議可驗安全性形式化分析.中國工程科學,2010,1(12): 67-73.5 kevin benton. the evolution of 802.11 wireless security. inf795-april 18th,2010 unlv infonnatics

39、 spring2010.6 r. canetti and h. krawczyk. analysis of key-exchange protocols and their use for building secure channels. advances in cryptology-eurocrypt 2001,pp.453-474,springer-verlag,2001.7 b lamacchia, k lauter and a mityagin. stronger security of authenticated key exchange. </2006/073>.8 gast and s matthe. 8021 wireless networks: the definitive guide; creating &administering wireless networks; covers 802.11a, g,n& i. beijing: o'reilly,2007. print.9 rfc 2865 - remote authentication dial in user servic