Formalization And Verification Of DHCPv6 Security Protocol Based On CSP

DHCPv6(Dynamic Host Configuration Protocol for IPv6)is the next-generation Internet IPv6 address automatic configuration protocol,and its security is extremely important.However,DHCPv6 has three major problems: source address verification,privacy protection,and identity authentication.IETF(Internet Engineering Task Force)proposed SAVI-DHCP(Source Address Validation Improvement Solution for DHCP),which is a fine-grained access network source address verification solution that can prevent forged IP attacks.In addition,DHCPv6 Sec is proposed by scholars to solve privacy and authentication problems.It is an authentication protocol based on a hybrid cryptosystem.However,the security of the two protocols has not been rigorously analyzed.This paper analyzes and verifies the two security protocols based on CSP(Communicational Sequential Processess).For the SAVI-DHCP protocol,considering its complexity and environmental uncertainty,we first define a typical scenario and ignore some details that are irrelevant to modeling,which can greatly reduce the state space.Then based on the scenarios established above,we formally analyze the three types of entities of the client,server,and non-SAVI devices,as well as the communication behavior between entities.Then we use the diamond model to analyze the possible existence of the system from the perspective of victims and capabilities.The attack behavior is analyzed,and the attacker model is established for the two typical attacks of forgery and migration.So far we have established a modeling framework.Based on this modeling framework,we analyze the SAVI equipment process,divide it into six sub-processes for modeling,and introduce the previously established attacker model to form the SAVI-DHCP system model.Finally,PAT(Process Analysis Toolkit)is used to verify the relevant properties of the system model,and the results show that the model will be subject to forgery attacks from non-directly connected clients.For the DHCPv6 Sec protocol,we first describe the client,server,and router entities in the protocol as the three processes of the CSP,and model the respective request and response behaviors in the process to form a DHCPv6 Sec model.Then based on the Dolev-Yao model,an attacker model that intercepts,decomposes,forges,and replays messages is established,and the DHCPv6 Sec model that introduces attackers is perfected.Finally,we used the PAT to verify the security properties of the DHCPv6 Sec model,and found that the model satisfies the anti-replay property and the confidentiality of client messages,but does not satisfy the unforgeability of the server.