Formalization And Analysis Of SAVI-DHCP Protocol

With the development of IPv6 networks,new security issues brought about by new features,and they become more complex.Now,security protocols are still one of the important guarantees of network security.However,the reliability of the security protocol cannot be guaranteed at the time of design.Therefore,formal analysis and verification of security protocols are usually required.DHCPv6 is one of the ways to obtain an IPv6 address.However,the security of the protocol has not been considered since the DHCPv6 protocol was proposed.SAVI(Source Address Validation Improvements)is one of the important ways to solve network security problems for IPv6 access networks.The SAVI-DHCP standard is the research object of this article.It is a source address verification mechanism for obtaining addresses through DHCPv6 in IPv6 networks.There is no research on the formalization of SAVI-DHCP,so there may be potential security threats.This article conducts formal modeling,analysis and verification for the part of DHCPv6 in SAVI-DHCP.We use CSP(Communicating Sequential Processes)to build the model of SAVI-DHCP protocol,including the abstraction and description of the subject,channel,message,and communication process.We establish a two-layer system model,including a internal system——the BST binding table dictionary process,and a external system——the overall system composed of client/server,which fully describes the communication behavior in the SAVI-DHCP protocol.Then,we use the PAT(Process Analysis Toolkit)tool to verify the above model.First,we expand and modify the C#interface function library which provided by PAT.Then we use PAT to encode the above model,and then we automate the verification,and finally we give the verification result.We verify the deadlock-free,atomicity,isolation and optimism of the internal system,and verify the deadlock-free,authentication,authorization and usability of the overall system.In addition to availability,other properties are satisfied.We have proved that the SAVI-DHCP protocol can communicate normally but it has flaws.Finally,starting from the real network environment,we provide an intruder case for the SAVI-DHCP protocol.We build the model of intruder and propose two optimization strategies for availability issues.Then we verify whether the optimized system can meet the availability.The results show that the optimization of adding the LRU strategy is effective and it can strengthen availability and security of SAVI-DHCP protocol.