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

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

2、析方法。雖然這些形式化方法已經成功地發現了許多安全協議的漏洞和攻擊，但是它們都有各自的局限性。有些分析方法不完善，定義的結構簡單，無法對復雜協議進行分析；有些分析方法在設計時，自身就存在安全隱患。在諸多的形式化分析方法中，串空間理論以簡潔、嚴謹和高效等特點成為近年來形式化分析領域的研究熱點，它將安全協議的形式化分析方法的研究推向了一個新的高度。
　　本文以串空間理論為基礎，對經典認證協議、無線網絡安全協議，Ad hoc網絡安全路由

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

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

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

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

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