基于串空間理論的安全協(xié)議研究.pdf

1、隨著網(wǎng)絡(luò)技術(shù)的飛速發(fā)展，網(wǎng)絡(luò)安全問題日趨嚴(yán)重。安全協(xié)議是信息安全的一個(gè)重要研究方向，它是構(gòu)建網(wǎng)絡(luò)安全環(huán)境的基石，其安全性對整個(gè)網(wǎng)絡(luò)環(huán)境的安全起到了至關(guān)重要的作用。雖然安全協(xié)議的設(shè)計(jì)和分析已歷經(jīng)了三十余年的發(fā)展，但是由于安全協(xié)議設(shè)計(jì)的復(fù)雜性、網(wǎng)絡(luò)攻擊方式的多樣性和運(yùn)行環(huán)境的差異性，使得安全協(xié)議的設(shè)計(jì)和分析仍然面臨諸多困難和挑戰(zhàn)。
　　形式化分析方法是安全協(xié)議分析中最重要的工具之一。隨著安全協(xié)議研究的發(fā)展，出現(xiàn)了各種各樣的驗(yàn)證模型和分

2、析方法。雖然這些形式化方法已經(jīng)成功地發(fā)現(xiàn)了許多安全協(xié)議的漏洞和攻擊，但是它們都有各自的局限性。有些分析方法不完善，定義的結(jié)構(gòu)簡單，無法對復(fù)雜協(xié)議進(jìn)行分析；有些分析方法在設(shè)計(jì)時(shí)，自身就存在安全隱患。在諸多的形式化分析方法中，串空間理論以簡潔、嚴(yán)謹(jǐn)和高效等特點(diǎn)成為近年來形式化分析領(lǐng)域的研究熱點(diǎn)，它將安全協(xié)議的形式化分析方法的研究推向了一個(gè)新的高度。
　　本文以串空間理論為基礎(chǔ)，對經(jīng)典認(rèn)證協(xié)議、無線網(wǎng)絡(luò)安全協(xié)議，Ad hoc網(wǎng)絡(luò)安全路由

3、協(xié)議和群組密鑰協(xié)商協(xié)議的設(shè)計(jì)和分析進(jìn)行了深入研究，取得了一些重要的研究成果。
　　對串空間理論在典型安全協(xié)議中的應(yīng)用進(jìn)行了研究，使用串空間理論分析了Yahalom-Paulson協(xié)議的安全性，發(fā)現(xiàn)協(xié)議在認(rèn)證性上存在缺陷。針對協(xié)議存在的攻擊，對協(xié)議進(jìn)行了重新設(shè)計(jì)，給出了改進(jìn)后的協(xié)議，改進(jìn)協(xié)議在認(rèn)證性方面彌補(bǔ)了Yahalom-Paulson協(xié)議的不足。
　　使用串空間理論對CCITTX.509(3)協(xié)議的安全性進(jìn)行了分析，發(fā)現(xiàn)協(xié)

4、議中存在認(rèn)證缺陷，并給出了針對協(xié)議漏洞的攻擊過程。
　　對串空間理論的設(shè)計(jì)進(jìn)行了深入研究，在攻擊者模型中添加了攻擊者行為，豐富了攻擊者跡和密碼學(xué)原語，重新定義了串空間理論中的相關(guān)概念，并對衍生出的命題、定理、推論等進(jìn)行了證明。針對sever-specific MAKEP協(xié)議存在的安全缺陷，提出了一個(gè)新的雙向認(rèn)證和密鑰交換協(xié)議(Eserver-specific MAKEP協(xié)議)。使用擴(kuò)展的串空間理論分析了Esever-specifi

5、c MAKEP協(xié)議的安全性，證明了協(xié)議不但能夠抵御未知的密鑰共享攻擊，而且能夠避免服務(wù)器對生成共享密鑰的控制。
　　使用擴(kuò)展的串空間理論對SNEP的節(jié)點(diǎn)間密鑰協(xié)商協(xié)議的安全性進(jìn)行了分析，發(fā)現(xiàn)了協(xié)議在認(rèn)證性上存在安全缺陷，即攻擊者可以冒充合法用戶完成密鑰協(xié)商。針對此缺陷，對協(xié)議進(jìn)行了重新設(shè)計(jì)，給出了一個(gè)改進(jìn)協(xié)議。使用擴(kuò)展的串空間理論分析了改進(jìn)協(xié)議的安全性，證明了改進(jìn)協(xié)議能夠滿足認(rèn)證性和保密性兩個(gè)安全目標(biāo)。通過對以上協(xié)議的分析和證明，

6、也說明了擴(kuò)展的串空間理論的正確性，擴(kuò)大了串空間理論的應(yīng)用范圍。
　　對Ad hoc網(wǎng)絡(luò)安全路由協(xié)議的設(shè)計(jì)和分析進(jìn)行了深入研究。為了能夠使用串空間理論分析Ad hoc網(wǎng)絡(luò)路由協(xié)議的安全性，針對Ad hoc網(wǎng)絡(luò)安全路由協(xié)議的特點(diǎn)，擴(kuò)展了串空間理論中的“正確性”概念，增加了攻擊者的行為。使用擴(kuò)展的串空間理論分析了ARAN路由協(xié)議的安全性，發(fā)現(xiàn)了該協(xié)議存在重放和合謀兩種攻擊。提出了一個(gè)新的Ad hoc網(wǎng)絡(luò)安全路由協(xié)議(eARAN協(xié)議)，使

7、用擴(kuò)展的串空間理論證明了eARAN協(xié)議的安全性。由此可見，基于擴(kuò)展的串空間理論分析Ad hoc網(wǎng)絡(luò)安全路由協(xié)議的新方法是有效的，成功地將串空間理論的應(yīng)用范圍拓展到分析Ad hoc網(wǎng)絡(luò)安全路由協(xié)議領(lǐng)域。
　　對群組密鑰協(xié)商協(xié)議的設(shè)計(jì)和分析進(jìn)行了深入研究。分析了基于身份的群組密鑰協(xié)商協(xié)議HTK協(xié)議的安全性，發(fā)現(xiàn)了HTK協(xié)議無法抵御組內(nèi)合法用戶的共謀攻擊(insider attack)。分析了認(rèn)證群組密鑰協(xié)商協(xié)議DB協(xié)議存在的安全缺陷，