随着IPv6不断走向成熟和普及,由IPv6新特性带来的新的网络安全问题也变得更加复杂,目前安全协议依然是网络安全的重要保障之一,但安全协议的可靠性无法在设计之时就得到保证,所以通常需要对其进行形式化分析与验证。IPv6地址配置方式之一是通过DHCPv6方式配置,但DHCPv6协议在提出时就未考虑协议的安全性问题。SAVI（Source Address Validation Improvements）源地址验证方案是针对IPv6接入网场景的,是目前解决IPv6网络安全问题的重要途径之一,其中SAVI-DHCP标准就是针对IPv6网络中通过DHCP配置地址的源地址验证机制,也是本文的研究对象。SAVI-DHCP协议机制缺少形式化方面的研究,可能会存在潜在的安全威胁,本文针对SAVI-DHCP协议中DHCPv6的部分进行形式化建模、分析与验证。本文使用通信顺序进程 CSP（Communicating Sequential Processes）方法对 SAVI-DHCP 协议涉及的主体、信道、消息、通信过程等,进行了全面的抽象、分析与刻画,建立了双层系统模型,包括内部系统BST绑定表字典进程和外部系统客户端服务器模型构成的整体系统,全面刻画了 SAVI-DHCP协议的中的通信行为。然后,本文使用模型检测工具PAT（Process Analysis Toolkit）,对其提供的C#接口函数库中的函数进行拓展和修改后,再对上述CSP模型进行编码,并进行自动化验证,然后给出验证的结果并进行分析。本文验证了 SAVI-DHCP协议内部系统的无死锁性、原子性、隔离性和乐观性,验证了 SAVI-DHCP协议整体系统的无死锁性、认证性、授权性和可用性。除了可用性以外其他性质均满足,本文证明了SAVI-DHCP协议能通信正常但存在漏洞。最后,本文从真实网络环境出发,为SAVI-DHCP协议提供了一个具有入侵者的案例,对入侵者进行建模,并针对可用性问题提出了两点优化方案,然后对优化后的系统是否能满足可用性进行验证。结果表明,加入了 LRU策略的优化方案有效,可以加强SAVI-DHCP协议机制的可用性。