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

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

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

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

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