IPv6協(xié)議的安全性分析與驗證.pdf

1、IPv4的局限性隨著Internet的飛速發(fā)展日益顯現(xiàn)，而IPv6引入了許多新特性，比如地址空間的擴大、報頭格式的簡化、對安全性支持的增強等，這些使得它必將成為新一代的IP協(xié)議標準。本文首先對IPv6的地址結構、報頭格式、鄰居發(fā)現(xiàn)、IPsec安全機制、路由協(xié)議等關鍵技術進行了介紹，為后面的分析做基礎。
　　協(xié)議的安全是網(wǎng)絡安全性的保證，為了盡可能找出協(xié)議中潛在的安全漏洞以改進協(xié)議的安全性，需要對協(xié)議的安全性進行分析。分析方法有兩類

2、：非形式化方法和形式化方法，非形式化方法又叫攻擊檢驗方法；形式化方法提供了一個框架，其本質(zhì)是基于數(shù)學的方法來描述目標軟件系統(tǒng)屬性的一種技術。本文對IPv6協(xié)議的安全性分析中，首先利用常規(guī)的分析方法，也就是攻擊檢驗方法對 IPv6的若干關鍵技術的安全性進行分析，依據(jù)協(xié)議的運行步驟、參與方等分析協(xié)議存在的問題，分析漏洞存在的可能性，然后在分析的基礎上，盡可能的提出改進的措施，這是本文中，我工作內(nèi)容的一個方面。
　　本文中，我另外的工作

3、部分是參與 SPIN模型檢測工具的改進。在對協(xié)議安全性分析的形式化方法中，因為對大規(guī)模協(xié)議驗證的支持和自動化程度高的優(yōu)勢，模型檢測有著廣泛的應用。本文首先概括的說明了協(xié)議分析的形式化方法；進一步對形式化方法中的模型檢測的相關技術研究點—模型檢測工具SPIN、建模語言Promela進行了介紹，重點描述了我們團隊對SPIN的改進。
　　我的第三個工作部分是利用我們改進后的模型檢測工具對 IPv6的安全機制——IPsec協(xié)議提供的安全性