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

1、三方認(rèn)證密鑰協(xié)商協(xié)議形式化安全模型的分析與改進(jìn)摘 要：本文對(duì)兩個(gè)三方認(rèn)證密鑰協(xié)商協(xié)議的形式化安全模型擴(kuò)展br模型和擴(kuò)展ck模型進(jìn)行了分析，發(fā)現(xiàn)了擴(kuò)展br模型中在三方身份認(rèn)證方面存在的安全漏洞，指出了擴(kuò)展ck模型中匹配會(huì)話定義的局限性，并根據(jù)802.11i所規(guī)范的協(xié)議流程，通過引入有效的概念，提出了三方認(rèn)證密鑰協(xié)商協(xié)議改進(jìn)的形式化安全模型，并在該模型下證明了改進(jìn)后eap-tls協(xié)議的安全性。新模型為解決無線局域網(wǎng)等特定環(huán)境下認(rèn)證密鑰協(xié)商協(xié)議的安全性問題提供了較好的解決思路。關(guān)鍵詞：802.11i；eap協(xié)議；可證明安全性；三方形式化安全模型1 引言2004年ieee 802.11標(biāo)準(zhǔn)組提出了80

2、2.11i標(biāo)準(zhǔn)以增強(qiáng)無線局域網(wǎng)的安全性能。在該標(biāo)準(zhǔn)中，客戶端的認(rèn)證和接入控制功能是通過802.1x協(xié)議實(shí)現(xiàn)的，而802.1x協(xié)議的認(rèn)證功能是通過上層認(rèn)證協(xié)議eap完成的，因此對(duì)eap協(xié)議的安全性進(jìn)行研究就顯得十分重要。然而，目前針對(duì)802.11i的三方認(rèn)證協(xié)議研究還沒有完善的形式化安全模型，1995年bellare等人提出了三方密鑰交換的形式化安全模型，但此模型沒有考慮實(shí)體間的認(rèn)證關(guān)系。2008年曹春杰提出了擴(kuò)展的ck模型，給出了三方認(rèn)證密鑰協(xié)商協(xié)議的形式化模型，但該模型中關(guān)于接入點(diǎn)會(huì)話標(biāo)識(shí)符的定義因?yàn)榇嬖诓淮_定性而并不實(shí)用（事實(shí)上文獻(xiàn)3中也并沒有給出具體的協(xié)議并利用該模型進(jìn)行證明）。2010

3、年宋宇波等人提出了擴(kuò)展的br模型，該模型利用參與方產(chǎn)生的會(huì)話序列對(duì)匹配會(huì)話進(jìn)行定義，但由于沒有考慮接入點(diǎn)在一次協(xié)議中產(chǎn)生的兩條會(huì)話序列之間的關(guān)系，因而該定義有可能會(huì)導(dǎo)致三方消息認(rèn)證不安全。因此，如何對(duì)三方認(rèn)證密鑰協(xié)商協(xié)議的形式化安全模型進(jìn)行改進(jìn)與完善，使其能保證無線局域網(wǎng)的參與方可以進(jìn)行安全認(rèn)證還需要進(jìn)一步的深入研究。本文通過對(duì)現(xiàn)有三方認(rèn)證密鑰協(xié)商協(xié)議形式化模型進(jìn)行深入分析，指出利用匹配會(huì)話定義三方協(xié)議的認(rèn)證關(guān)系時(shí)需要考慮特定的應(yīng)用背景，這是因?yàn)榻换サ娜街兄辽儆幸环揭c其它兩方同時(shí)進(jìn)行消息交互，對(duì)于這一方的會(huì)話描述（無論是用會(huì)話序列或是會(huì)話標(biāo)識(shí)符）必須考慮其自身所處的網(wǎng)絡(luò)位置和所具備的網(wǎng)絡(luò)功

4、能，否則一旦攻擊者對(duì)該方進(jìn)行冒充或破壞，就可能造成匹配會(huì)話定義的失效。對(duì)于802.11i而言，作為和中間具有轉(zhuǎn)發(fā)功能的參與方，其與和的交互內(nèi)容有一定的重復(fù)性，本文根據(jù)這一重要特點(diǎn)，在改進(jìn)的形式化安全模型中給出會(huì)話標(biāo)識(shí)符有效的定義。802.11i協(xié)議流程如圖1所示：圖1 802.11i協(xié)議流程客戶端通過無線網(wǎng)絡(luò)與接入點(diǎn)進(jìn)行連接，通過有線網(wǎng)絡(luò)與認(rèn)證服務(wù)器進(jìn)行連接，的功能是接收消息后進(jìn)行加脫密操作并轉(zhuǎn)發(fā)消息，的功能是對(duì)進(jìn)行認(rèn)證。802.11i協(xié)議中和通過轉(zhuǎn)發(fā)響應(yīng)各自的身份、加密方式、公鑰等相關(guān)信息，然后由發(fā)起eap認(rèn)證協(xié)議。設(shè)有一對(duì)公私鑰，有一對(duì)公私鑰，與間共享長期對(duì)稱密鑰。eap-tls協(xié)議的目的

5、是通過一系列的交互使客戶端與認(rèn)證服務(wù)器間協(xié)商主會(huì)話密鑰，并實(shí)現(xiàn)相互的身份認(rèn)證。eap協(xié)議完成后將協(xié)商得到的通過加密的方式發(fā)送給。然后與利用進(jìn)一步完成四步握手協(xié)議。在本文中，三方認(rèn)證密鑰協(xié)商協(xié)議指eap協(xié)議，由于eap是完成認(rèn)證和主會(huì)話密鑰協(xié)商的核心步驟，所以改進(jìn)的形式化安全模型也是建立在802.11i所規(guī)范的eap環(huán)節(jié)上。2 現(xiàn)有三方認(rèn)證密鑰協(xié)商協(xié)議安全模型分析本節(jié)我們簡(jiǎn)要回顧文獻(xiàn)4和文獻(xiàn)3中提出的擴(kuò)展br模型和擴(kuò)展ck模型。通過分析發(fā)現(xiàn)，擴(kuò)展的br模型中關(guān)于匹配會(huì)話的定義可能會(huì)導(dǎo)致消息認(rèn)證不安全，不能抵抗攻擊者對(duì)的冒充攻擊。在擴(kuò)展的ck模型中，當(dāng)攻擊者冒充時(shí)會(huì)導(dǎo)致會(huì)話標(biāo)識(shí)符定義的失效。2.1

6、 擴(kuò)展br模型及安全性分析文獻(xiàn)4中擴(kuò)展br模型將三方認(rèn)證密鑰協(xié)商協(xié)議形式化為一個(gè)四元組來描述。其中，定義了一個(gè)誠實(shí)客戶端的會(huì)話行為，定義了一個(gè)誠實(shí)接入點(diǎn)的會(huì)話行為，定義為誠實(shí)認(rèn)證服務(wù)器的會(huì)話行為，為認(rèn)證服務(wù)器分發(fā)給客戶端和無線接入點(diǎn)的初始會(huì)話密鑰。該模型將攻擊者形式化為擁有黑盒預(yù)言機(jī)、和的概率圖靈機(jī)，且可以對(duì)這些預(yù)言機(jī)進(jìn)行預(yù)定的查詢并從預(yù)言機(jī)那里獲得應(yīng)答。 為了描述參與方之間的認(rèn)證關(guān)系，文獻(xiàn)4在原br模型兩方認(rèn)證安全的基礎(chǔ)上進(jìn)行了擴(kuò)展。在原br模型中，若兩條會(huì)話序列分別是對(duì)方的匹配會(huì)話，則稱這兩條會(huì)話序列是匹配會(huì)話。在擴(kuò)展br模型中，這種匹配會(huì)話的定義被直接推廣到了三方的情況：設(shè)預(yù)言機(jī)為、以及

7、，產(chǎn)生的相應(yīng)會(huì)話序列分別用和表示，則在擴(kuò)展br模型中，三方之間的匹配會(huì)話和消息認(rèn)證安全的定義如下：定義1 如果是的匹配會(huì)話，也是的匹配會(huì)話；是的匹配會(huì)話，也是的匹配會(huì)話，則稱預(yù)言機(jī)之間有匹配的會(huì)話。當(dāng)一個(gè)協(xié)議在攻擊者的控制下執(zhí)行，如果存在一個(gè)沒有被攻破的預(yù)言機(jī)呈接受狀態(tài)，但沒有一個(gè)與它有匹配會(huì)話的預(yù)言機(jī)存在的時(shí)候，稱這樣的會(huì)話是不匹配的。定義2 如果不匹配會(huì)話的概率是可忽略的，則稱協(xié)議是消息認(rèn)證安全的。定義1分別給出了與，與之間會(huì)話的匹配關(guān)系，但是卻忽略了這兩者之間的相關(guān)性，也就是說攻擊者可以通過重放某次協(xié)議中的一個(gè)匹配關(guān)系構(gòu)造出滿足定義1的匹配會(huì)話使三方都接受。因此通過上述匹配會(huì)話給出的認(rèn)證

8、安全的定義2至多只能提供和，和之間的認(rèn)證，卻不能保證與之間的認(rèn)證，這樣就不能實(shí)現(xiàn)802.11i中eap-tls協(xié)議的目的(提供客戶端和認(rèn)證服務(wù)器的雙向認(rèn)證)。為了便于說明舉例如下： ( 1 ) 是協(xié)議的合法參與方，與正常的，進(jìn)行一次會(huì)話后得到匹配會(huì)話，。 ( 2 ) 是攻擊者，通過重放(1)中的會(huì)話與正常的，進(jìn)行一次會(huì)話后得到相應(yīng)的會(huì)話，。由于，是匹配會(huì)話，是與完成的一次正常交互，因此同樣是匹配會(huì)話，那么根據(jù)定義1有，是一個(gè)匹配會(huì)話，但此時(shí)，均認(rèn)為攻擊者的正確身份是。這說明在文獻(xiàn)4中擴(kuò)展的br模型關(guān)于消息認(rèn)證安全的定義有一定的局域性，為了避免因此造成的安全漏洞，有必要對(duì)其進(jìn)行改進(jìn)。2.2 擴(kuò)展

9、ck模型的定義缺陷2008年曹春杰基于ck模型，提出了支持三方協(xié)議的形式化安全模型擴(kuò)展ck模型。該模型通過會(huì)話標(biāo)識(shí)符來定義匹配會(huì)話。定義3 令為會(huì)話標(biāo)識(shí)符，為協(xié)議參與方的身份，為參與方在協(xié)議中的角色。設(shè)在三方認(rèn)證協(xié)議的一次執(zhí)行中，生成會(huì)話 ，生成會(huì)話，生成，如果有，且互不相同，則我們稱這三個(gè)會(huì)話是匹配會(huì)話。利用會(huì)話標(biāo)識(shí)符定義匹配會(huì)話比通過會(huì)話序列定義更簡(jiǎn)潔有效。但該模型與ck模型一樣，并沒有給出的具體定義，只是簡(jiǎn)單地將兩方的情況推廣至三方，而沒有考慮定義的存在性和確定性。擴(kuò)展的ck模型同樣是基于無線局域網(wǎng)而設(shè)計(jì)的。該模型假設(shè)協(xié)議正常執(zhí)行的情況下，包括敵手在內(nèi)的任意會(huì)話在執(zhí)行后都生成相應(yīng)的，并基

10、于此定義匹配會(huì)話。但我們通過分析發(fā)現(xiàn)，當(dāng)攻擊者對(duì)進(jìn)行冒充時(shí)可能造成會(huì)話標(biāo)識(shí)符具有不確定性，如下例所示： 假設(shè)敵手通過消息重放等手段完成了以上會(huì)話實(shí)例，按照定義和分別生成會(huì)話標(biāo)識(shí)符， 。由于協(xié)議執(zhí)行中涉及接收并發(fā)送多個(gè)不同消息(，)，因而此時(shí)對(duì)會(huì)話標(biāo)識(shí)符的定義可以有多種選擇，例如可以設(shè)或，這就造成定義具有不確定性。而事實(shí)上，的作用是對(duì)協(xié)議的某一次會(huì)話做特定的標(biāo)識(shí)，應(yīng)當(dāng)具有唯一性，因此在上述情況下，擴(kuò)展ck模型關(guān)于匹配會(huì)話的定義顯然是不合理的。為了解決上述問題，需對(duì)802.11i的協(xié)議流程進(jìn)行進(jìn)一步分析，根據(jù)的功能對(duì)會(huì)話標(biāo)識(shí)符定義進(jìn)一步完善。3 改進(jìn)的三方認(rèn)證密鑰協(xié)商協(xié)議形式化安全模型我們?cè)趯?duì)擴(kuò)展

11、br模型和擴(kuò)展ck模型分析的基礎(chǔ)上，提出了改進(jìn)的三方認(rèn)證密鑰協(xié)商協(xié)議形式化安全模型。該模型充分考慮了的功能和特點(diǎn)，通過引入有效的概念，解決了三方身份認(rèn)證中匹配會(huì)話定義不完善和不確定的問題。在該模型下可證安全的三方eap協(xié)議可以實(shí)現(xiàn)與的交互認(rèn)證且能保證主會(huì)話密鑰安全，因而對(duì)802.11i中eap協(xié)議的設(shè)計(jì)與分析有著重要的意義，對(duì)該模型的詳細(xì)描述如下：3.1 敵手能力由于802.11i協(xié)議中的認(rèn)證環(huán)節(jié)是采用完整的加密或簽名算法來實(shí)現(xiàn)的，所以新模型并不適合假設(shè)敵手可以通過某種方法得到參與者的長期密鑰或者臨時(shí)密鑰，因?yàn)檫@種假設(shè)會(huì)直接導(dǎo)致敵手對(duì)用戶消息的簽名偽造或者加脫密。在本模型中對(duì)敵手的攻擊能力假設(shè)

12、如下。、分別擁有自己的公私鑰對(duì)，此外、之間共享一對(duì)長期對(duì)稱密鑰。攻擊者可以竊聽、篡改、轉(zhuǎn)發(fā)、刪除、偽造、嵌入三方之間交互的消息，具體地可以將敵手能力形式化為以下對(duì)預(yù)言機(jī)的查詢：查詢：攻擊者可以對(duì)、進(jìn)行查詢。當(dāng)進(jìn)行查詢時(shí)，返回參與方的第次會(huì)話的會(huì)話實(shí)例。此查詢模擬被動(dòng)攻擊，即敵手具有獲得大量會(huì)話實(shí)例的能力。查詢：攻擊者可以對(duì)、進(jìn)行查詢。當(dāng)進(jìn)行查詢時(shí)，攻擊者發(fā)送消息給參與方的第次會(huì)話，根據(jù)協(xié)議的約定執(zhí)行，并返回給敵手相應(yīng)的執(zhí)行結(jié)果。此詢問模擬主動(dòng)攻擊，描述敵手進(jìn)行消息的偽造、重放、篡改等對(duì)消息進(jìn)行修改操作的能力。在802.11i所規(guī)范的協(xié)議流程中，和協(xié)商生成主會(huì)話密鑰，并由將加密后發(fā)送給。為了使模

13、型簡(jiǎn)單且易于分析，可以合理的假設(shè)的安全性僅依賴于認(rèn)證協(xié)議的安全性，對(duì)于將加密后發(fā)送給這一步驟并不計(jì)算在認(rèn)證密鑰協(xié)商協(xié)議中，且認(rèn)為其不泄露的任何信息。因此對(duì)查詢定義如下：查詢：攻擊者可以對(duì)和的會(huì)話進(jìn)行查詢，當(dāng)進(jìn)行查詢時(shí)，(或)所對(duì)應(yīng)的會(huì)話實(shí)例返回給攻擊者本次會(huì)話生成的會(huì)話密鑰。此攻擊形式化了敵手進(jìn)行相關(guān)密鑰攻擊的能力。查詢：攻擊者只能對(duì)沒有被進(jìn)行過查詢且已經(jīng)完成的或的會(huì)話進(jìn)行test詢問。敵手進(jìn)行一次隨機(jī)擲幣，如果擲幣結(jié)果b=0，則返回給敵手；如果b=1，則返回給敵手一個(gè)隨機(jī)數(shù)（取自主會(huì)話密鑰空間），但敵手不知道擲幣的結(jié)果，他根據(jù)返回值做判斷，輸出，用表示敵手猜對(duì)的概率，用表示敵手的優(yōu)勢(shì)，根據(jù)不

14、可區(qū)分性理論，如果的值是可忽略，那么敵手不能得到會(huì)話密鑰的任何信息。我們稱具有上述4種能力的敵手為3ake敵手。上述對(duì)敵手的形式化描述僅限于此三方協(xié)議是利用加脫密算法和簽名算法進(jìn)行設(shè)計(jì)的情況，因此不適合假設(shè)敵手具有很強(qiáng)的攻擊能力。但是如果在此模型下的協(xié)議是利用困難問題進(jìn)行設(shè)計(jì)的，則可以進(jìn)一步考慮敵手得到長期密鑰和臨時(shí)密鑰的能力，從而得到基于eck2007模型的三方擴(kuò)展模型。3.2 安全性定義在對(duì)擴(kuò)展br模型分析后發(fā)現(xiàn)，通過交互消息產(chǎn)生的會(huì)話序列來定義匹配會(huì)話具有一定的局域性，這是因?yàn)樵谌絽f(xié)議中，在與進(jìn)行消息交互的同時(shí)也與進(jìn)行消息交互，所以會(huì)話序列很難將與另兩方的會(huì)話都刻畫清楚，因此在改進(jìn)的模

15、型中我們通過會(huì)話標(biāo)識(shí)符來定義匹配會(huì)話。由于的功能主要是消息的加脫密和轉(zhuǎn)發(fā)，這意味著會(huì)話(1)中的，的消息內(nèi)容有著明顯的關(guān)聯(lián)和重復(fù)性，我們可以利用這種關(guān)聯(lián)引入有效的概念，通過有效將與、與之間的會(huì)話聯(lián)系起來，進(jìn)而給出三方匹配會(huì)話的定義。定義4 設(shè)與之間共享密鑰、加密算法和相應(yīng)的脫密算法，如果在時(shí)刻，接收到來自的消息，在緊鄰的下一個(gè)時(shí)刻發(fā)送給消息，在時(shí)刻接收到來自的消息，在緊鄰的下一個(gè)時(shí)刻發(fā)送給消息，且有，則稱是有效的。會(huì)話標(biāo)識(shí)符是協(xié)議參與方在接受后生成的用于標(biāo)記此次會(huì)話的標(biāo)識(shí)，具體定義為參與方執(zhí)行過程中接收和發(fā)送消息內(nèi)容的串接。不妨設(shè)參與方、接受后生成的會(huì)話標(biāo)識(shí)符為，其中與的會(huì)話標(biāo)識(shí)符與ck模型類

16、似，對(duì)于執(zhí)行過程中重復(fù)出現(xiàn)的消息內(nèi)容僅在計(jì)算在此次會(huì)話的時(shí)使用一次。根據(jù)上述定義可以得到如下性質(zhì)。性質(zhì)1 對(duì)于一次正確會(huì)話的參與方、，在協(xié)議完成后分別生成相應(yīng)的會(huì)話標(biāo)識(shí)符，如果是有效的，則有。證明 設(shè)為與會(huì)話消息的串接。如果協(xié)議執(zhí)行過程中沒有攻擊者的參與，且各方都順利完成了會(huì)話過程，（即是正確會(huì)話），那么有。由有效性的定義可知，其中為與交互的消息內(nèi)容，據(jù)此可以定義的會(huì)話標(biāo)識(shí)符。同理可知，當(dāng)協(xié)議正確執(zhí)行時(shí)有，于是性質(zhì)1成立。性質(zhì)2 對(duì)于不是有效參與的協(xié)議會(huì)話，在全部接受后生成會(huì)話標(biāo)識(shí)符，則必然有。證明 若不是有效的由定義可知，所以或，不妨設(shè)，因?yàn)樵谀硞€(gè)時(shí)刻，接收到消息，則必然在時(shí)刻由發(fā)送過消息，

17、所以中包含；如果在某個(gè)時(shí)刻，發(fā)送過消息，則必然在時(shí)刻由接收到消息，所以中包含，由可知。以下給出改進(jìn)后安全模型下關(guān)于匹配會(huì)話和認(rèn)證密鑰協(xié)商安全的定義：定義5 如果對(duì)有效的參與的會(huì)話在執(zhí)行后，參與的三方都接受會(huì)話且生成的會(huì)話標(biāo)識(shí)符，則稱是匹配會(huì)話。定義6 稱802.11i規(guī)范下的eap-tls協(xié)議是三方認(rèn)證安全的，如果該協(xié)議滿足以下三條：(1)如果是匹配會(huì)話，則對(duì)應(yīng)的都接受；(2)如果都接受，則是匹配會(huì)話；(3)對(duì)于無效參與的協(xié)議，不存在會(huì)話使或接受。定義7 稱802.11i規(guī)范下的eap-tls協(xié)議是安全的，如果對(duì)任意3ake敵手滿足以下兩條：(1)協(xié)議執(zhí)行后、生成相同的；(2)敵手優(yōu)勢(shì)是可忽略

18、的。4 eap-tls協(xié)議及其安全證明為進(jìn)一步驗(yàn)證改進(jìn)后安全模型的有效性和合理性，我們提出一個(gè)適用于802.11i的新eap-tls協(xié)議，并利用所提出的新三方認(rèn)證密鑰協(xié)商形式化安全模型對(duì)其進(jìn)行證明。 新的eap-tls協(xié)議協(xié)議的執(zhí)行過程如下：收到eap-start請(qǐng)求后，隨機(jī)生成并發(fā)送給，對(duì)進(jìn)行加密后轉(zhuǎn)發(fā)給；由密鑰空間中隨機(jī)生成利用加密后與一起進(jìn)行簽名，將簽名后的結(jié)果加密后發(fā)送給，脫密后轉(zhuǎn)發(fā)給；對(duì)簽名進(jìn)行驗(yàn)證(檢查是否相等)，并利用自己的私鑰對(duì)脫密得到，對(duì)進(jìn)行雜湊并用自己的私鑰簽名后發(fā)送給，然后接受，隨后加密轉(zhuǎn)發(fā)給；對(duì)進(jìn)行脫密操作后對(duì)進(jìn)行雜湊并驗(yàn)證其是否為簽名內(nèi)容，若驗(yàn)證通過接受。和協(xié)商得主會(huì)

19、話密鑰， 。定理1 如果簽名算法是不可偽造的，則上述協(xié)議是三方認(rèn)證安全的。證明 只需要證明上述新eap-tls協(xié)議滿足定義6中的三條即可。對(duì)于定義的第一條易知在協(xié)議正常執(zhí)行的情況下，滿足有效性的定義，此時(shí)若是匹配會(huì)話，則由性質(zhì)1有，顯然三方都會(huì)接受。下面我們證明協(xié)議滿足定義6的第二條：對(duì)于有效參與的協(xié)議，要使三方都接受，則中一定包含消息使得接受。同樣對(duì)于認(rèn)證服務(wù)器，中一定包含消息使接受。由于簽名算法是不可偽造的，所以攻擊者不可能構(gòu)造出這樣的簽名，則這兩個(gè)簽名必然是由轉(zhuǎn)發(fā)的，這說明曾接收到消息和。又由長期密鑰的保密性和簽名算法的安全性可知，攻擊者同樣不能對(duì)這兩條消息進(jìn)行偽造，因此曾發(fā)送過消息，曾

20、發(fā)送過消息。綜上所述，各包含的消息如下：包含消息、；包含消息、；包含消息、，因此有，于是是匹配會(huì)話。最后我們證明當(dāng)參與協(xié)議的非有效時(shí)，不存在會(huì)話使三方都接受。利用反證法不妨假設(shè)存在會(huì)話使三方都接受，則接受后的會(huì)話生成相應(yīng)的會(huì)話標(biāo)識(shí)符 ，由性質(zhì)2可知，當(dāng)非有效時(shí)有，則必然有或者是。對(duì)于前一種情況意味著攻擊者可以對(duì)認(rèn)證服務(wù)器的簽名進(jìn)行偽造，第二種情況意味著攻擊者可以對(duì)的簽名進(jìn)行偽造，這顯然與簽名算法的安全性相矛盾，因此該協(xié)議滿足三方認(rèn)證安全定義的三個(gè)條件。定理2 如果雜湊函數(shù)是安全的，加密算法和是安全的，簽名算法是不可偽造的，則上述協(xié)議是安全的。證明 設(shè)攻擊者進(jìn)行查詢后猜測(cè)擲幣結(jié)果成功的概率為，我

21、們分別對(duì)敵手三種不同的攻擊方式構(gòu)造區(qū)分器。(1)查詢：假設(shè)攻擊者可以進(jìn)行次查詢，用表示敵手利用此類查詢猜測(cè)成功的概率。攻擊者利用此查詢獲得關(guān)于信息的有效方式是通過和來進(jìn)行計(jì)算的，我們對(duì)此做如下實(shí)驗(yàn)。實(shí)驗(yàn)1：挑戰(zhàn)者進(jìn)行一次隨機(jī)擲幣，若結(jié)果為則返回給攻擊者，若結(jié)果為則隨機(jī)選擇(為空間)返回給攻擊者，攻擊者根據(jù)返回的結(jié)果猜測(cè)挑戰(zhàn)者擲幣的結(jié)果為，令表示攻擊者猜測(cè)正確的概率。實(shí)驗(yàn)2：挑戰(zhàn)者進(jìn)行一次隨機(jī)擲幣，若結(jié)果為則返回給攻擊者，若結(jié)果為則隨機(jī)選擇(為空間)返回給攻擊者，攻擊者根據(jù)返回的結(jié)果猜測(cè)挑戰(zhàn)者擲幣的結(jié)果為，令表示攻擊者猜測(cè)正確的概率。在實(shí)驗(yàn)1中，由于算法是安全的，攻擊者至多進(jìn)行次查詢，則敵手通過

22、此查詢贏得實(shí)驗(yàn)1的概率。同理在實(shí)驗(yàn)2中，由于雜湊函數(shù)是安全的，因此敵手通過查詢贏得實(shí)驗(yàn)2的概率，因此=+(2)查詢：假設(shè)攻擊者可以進(jìn)行次查詢，用表示敵手利用此查詢猜測(cè)成功的概率。事實(shí)上，攻擊者能否利用查詢得到的信息等同于攻擊者能否對(duì)簽名進(jìn)行偽造。因此我們構(gòu)造攻擊者對(duì)簽名的偽造實(shí)驗(yàn)：實(shí)驗(yàn)：對(duì)于給定的參數(shù)，查詢做出后，攻擊者隨機(jī)生成，并由的密鑰空間中隨機(jī)選擇，構(gòu)造簽名 ，由于攻擊者至多進(jìn)行次查詢，不妨假設(shè)攻擊者利用此方法構(gòu)造了一個(gè)具有個(gè)簽名的列表：在實(shí)驗(yàn)中，如果第次查詢的簽名屬于列表，則返回給攻擊者相應(yīng)的主會(huì)話密鑰，否則返回“”。實(shí)驗(yàn)：同實(shí)驗(yàn)類似，查詢做出后，攻擊者隨機(jī)生成，并由的密鑰空間中隨機(jī)選

23、擇，構(gòu)造簽名 ，由于攻擊者至多進(jìn)行次查詢，不妨假設(shè)攻擊者利用此方法構(gòu)造了一個(gè)具有個(gè)簽名的列表：.在實(shí)驗(yàn)中，如果第次查詢的簽名屬于列表，則返回給攻擊者相應(yīng)的主會(huì)話密鑰，否則返回“”。設(shè)和的密鑰空間為，則攻擊者利用實(shí)驗(yàn)1偽造成功的概率為，利用實(shí)驗(yàn)2偽造成功的概率為，因此=+(3)查詢：設(shè)攻擊者可以對(duì)當(dāng)前攻擊實(shí)例外的其它個(gè)會(huì)話實(shí)例進(jìn)行查詢，返回給攻擊者被查詢會(huì)話生成的主會(huì)話密鑰。由于每次會(huì)話的都隨機(jī)獨(dú)立的選取，因此攻擊者利用此查詢猜測(cè)查詢擲幣結(jié)果成功的概率。綜上所述，攻擊者對(duì)查詢擲幣結(jié)果猜測(cè)成功的概率=+因此該協(xié)議是安全的。 5 小結(jié)本文在802.11i的協(xié)議規(guī)范下，根據(jù)所具有的特定功能和實(shí)際應(yīng)用中

24、的一些特點(diǎn)，給出了有效的概念，并利用其給出了此類模型的兩個(gè)基本性質(zhì)。并通過將其應(yīng)用于具體的eap-tls協(xié)議的安全性證明中，說明了該模型具有一定的合理性和適用性。本文所提出的三方模型主要考慮了無線局域網(wǎng)這一特定的應(yīng)用背景，對(duì)于其它三方環(huán)境并未做細(xì)致的研究。在下一步工作中，可以針對(duì)其它有特定應(yīng)用背景的三方協(xié)議對(duì)形式化安全模型進(jìn)一步研究，并可以假設(shè)敵手具有更強(qiáng)的攻擊能力來建立新的模型，在此類新模型下，可以利用數(shù)學(xué)困難問題設(shè)計(jì)更高效的安全認(rèn)證密鑰協(xié)商協(xié)議。參考文獻(xiàn)1 ieee802.11i. ieee standard for information technology-telecommunica

25、tions and inform ation exchange between systems-local and metropolitan area networks-specific requirements part 1 1：wireless lan medium access control(mac) and physical layer(phy)specifications: medium access control(mac) securityenhancementss. america,iso/iec,2004:1341.2 m bellare and p rogaway. pr

26、ovably secure session key distribution-the three party casea. proc.annual symposium on the theory of computingc.acm,2005:5766.3 曹春杰.可證明安全的認(rèn)證及密鑰交換協(xié)議設(shè)計(jì)與分析.西安電子科技大學(xué)博士學(xué)位論文.2008. 4 宋宇波,胡愛群,姚冰心. 802.1li認(rèn)證協(xié)議可驗(yàn)安全性形式化分析. 中國工程科學(xué), 2010,1(l2): 67-73.5 kevin benton. the evolution of 802.11 wireless security. inf

27、795-april 18th,2010 unlv informatics 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.453474,springer-verlag,2001.7 b lamacchia, k lauter and a mityagin. stronger security of authenticated

28、 key exchange. .8 gast and s matthe. 802.11 wireless networks: the definitive guide; creating &administering wireless networks; covers 802.11a, g, n & i. beijing: oreilly,2007. print.9 rfc 2865 - remote authentication dial in user service (radius). ietf web. .10 finneran m f. voice over wlans:the complete guidem. boston:elsevier,2008:280286.11 fluhrer s, mantin i and shamir a. weaknesses in the key schedule algorithm of rc4c. the 8th annual international workshop on selected areas in cryptography. london:springer-verlag ,2001:325.12 曹秀英,耿嘉,沈平. 無線局域