公共無(wú)線局域網(wǎng)安全體系研究及其可驗(yàn)安全性形式化分析.pdf

1、公共無(wú)線局域網(wǎng)(PWLAN)是目前無(wú)線網(wǎng)絡(luò)技術(shù)發(fā)展的熱點(diǎn)之一，旨在給用戶提供隨時(shí)隨地高效率、高質(zhì)量、低成本的移動(dòng)接入，其安全性直接影響到公共無(wú)線局域網(wǎng)技術(shù)的推廣應(yīng)用。如何設(shè)計(jì)和實(shí)現(xiàn)公共無(wú)線局域網(wǎng)的安全體系，為其安全協(xié)議的設(shè)計(jì)與分析提供理論指導(dǎo)，從而確保公共無(wú)線局域網(wǎng)的安全是目前迫切需要解決的問題。本文采用形式化分析手段，對(duì)當(dāng)前公共無(wú)線局域網(wǎng)安全協(xié)議的安全性進(jìn)行證明，并比較不同協(xié)議的安全性能，從而為選擇合適的安全協(xié)議提供依據(jù)。為此，本文開

2、展了以下幾個(gè)方面的研究： 1.通過(guò)對(duì)公共無(wú)線局域網(wǎng)現(xiàn)有應(yīng)用模式和體系結(jié)構(gòu)的分析，將公共無(wú)線局域網(wǎng)歸納為：WISP-ownedPWLAN、OperatorPWLAN以及PWLANforEnterprise三種類型。在此基礎(chǔ)上，提出了一個(gè)可以基本滿足各種類型公共無(wú)線局域網(wǎng)需求的基于接入控制器模式的通用公共無(wú)線局域網(wǎng)安全體系結(jié)構(gòu)，給出了該體系設(shè)計(jì)的合理性分析。 2.根據(jù)預(yù)言機(jī)模型，從協(xié)議的機(jī)密性和可靠性兩方面，對(duì)WEP、TKI

3、P以及CCMP密碼協(xié)議進(jìn)行了精確量化的可驗(yàn)安全性形式化分析；推導(dǎo)出WEP、TKIP和CCMP協(xié)議的安全量化函數(shù)，該函數(shù)采用攻擊成功率的優(yōu)勢(shì)函數(shù)來(lái)衡量加密機(jī)制的安全性能。分析表明，當(dāng)攻擊RC4算法的成功率為O(n2)*2-128(密鑰長(zhǎng)度為128比特)時(shí)，WEP的攻擊成功率約為O(n2)*2-24，TKIP的攻擊成功率約為O(n3)*2-48，這兩個(gè)加密協(xié)議都沒有達(dá)到提供預(yù)期的安全強(qiáng)度。 3.提出了TKIP算法的一種改進(jìn)算法。在該

4、算法中把TKIP序列計(jì)數(shù)器(TSC)值由原來(lái)的48比特?cái)U(kuò)大到128比特，使其安全強(qiáng)度比RC4算法提高了約3個(gè)數(shù)量級(jí)。 4.證明了CCMP加密協(xié)議的安全性和可靠性。分析表明，當(dāng)AES算法的攻擊成功率為O(n2)*2-128時(shí)，CCMP的可靠性和機(jī)密性對(duì)應(yīng)的攻擊成功率分別為O(n)*2-64和O(n2)*2-128，達(dá)到了預(yù)期的設(shè)計(jì)目標(biāo)，可以滿足公共無(wú)線局域網(wǎng)的安全需求。 5.利用Bellare-Rogoway模型，對(duì)密碼交