Ipv6 Protocol Security Analysis And Verification

With the rapid development of the Internet, the limitations of the IPv4protocolhave become increasingly notable. While the IPv6protocol introduces many newfeatures, such as the expansion of address space, the simplified header format and theenhanced security support, etc, which make it replace IPv4as the standard of theInternet IP protocol. At the first part of this thesis, I introduce the address structure ofthe IPv6protocol, the format of the datagram header, the neighbor discovery protocol,the IPSec security mechanisms, the routing protocols, which are key technologies of theIPv6protocol.The security of the Internet is inseparable from the assurance of protocol’s security.It’s an important way to reveal whether the protocol has security vulnerabilities toanalyze the protocol. There are two ways to analyze protocol: Attack test methods andFormal analysis methods. The Formal methods provide a framework, and they are basedon mathematical methods to describe the target attributes of the target software system.In the thesis, first, the attack test methods are used to analyze the security of several keytechnologies of the IPv6protocol, according to the steps and the participants of theProtocol. Analyze wether the protocol is vulnerable. And then, according to the resultsof the analysis, I make recommendations to make up the vulnerability as possible as Ican, which is one part of my works.The second part of my work was improving the performance of the SPIN softwaresystem as a participant of our team. Among Formal analysis methods, because of thesupport of the large-scale system verification and the high degree automation, modelchecking has been widely applied. In this thesis, I make a general introduction of theformal methods of protocol analysis; then I introduce the SPIN software system, thePromela language and our improvement on the performance of the SPIN softwaresystem which is an more important aspect of this these.In this thesis, the third part of my work is to verify the security of the IPsecprotocol using the SPIN software system improved by our team. It’s an important aspect of verifying the IPsec protocol to verify the security of the ESP protocol. And, it’s acritical work to make the Promela model simulation of the ESP protocol, of which, thecritical work is make the Promela model simulation of the attacker participating amongthe protocol. I make use of the atomic key word in establishing the model as many aspossible, which can improve the efficiency of the verification. At the end of the thesis, Imake recommendations to make up the vulnerability based on the results of theverification as possible as I can, then validate the effect of the improvement.