DHCPv6（Dynamic Host Configuration Protocol for IPv6）作为下一代互联网IPv6的地址自动配置协议,其安全性极其重要。然而,DHCPv6存在着源地址验证、隐私保护和身份认证三大问题。IETF（Internet Engineering Task Force）提出了SAVI-DHCP（Source Address Validation Improvement Solution for DHCP）,它是一种细粒度的接入网源地址验证方案,可以防止伪造IP攻击。此外DHCPv6Sec被学者提出用来来解决隐私和认证问题,是一种基于混合密码体制的认证协议。但是两个协议的安全性还未被严格分析,本文基于CSP（Communicational Sequential Processess）对这两个安全协议进行形式化分析并验证。对于SAVI-DHCP协议,本文考虑到它的复杂性和环境的不确定性,我们首先定义了一个典型场景,并忽略一些对建模无关的细节,这可以很大程度缩小状态空间。然后基于上面建立的场景,我们对其中的客户端、服务器、非SAVI设备三类实体以及实体间的通信行为形式化分析,之后我们采用钻石模型从受害者和能力的角度对系统中可能存在的攻击行为进行分析,并为伪造和迁移两个典型的攻击建立了攻击者模型,至此我们已经建立了建模框架。在此建模框架之上我们对SAVI设备进程进行分析,将它分为六个子进程进行建模,同时引入前面建立的攻击者模型形成SAVI-DHCP系统模型。最后使用PAT（Process Analysis Toolkit）对系统模型的相关性质进行验证,结果显示模型会受到非直连客户端的伪造攻击。对于DHCPv6Sec协议,我们首先将协议中的客户端、服务器、路由器三类实体描述为CSP的三个进程,并对进程中各自的请求与响应行为进行建模形成DHCPv6Sec模型。然后基于Dolev-Yao模型建立具有拦截、分解、伪造、重放消息等行为的攻击者模型,并完善了引入攻击者的DHCPv6Sec模型。最后我们使用PAT中对DHCPv6Sec模型的安全性质验证,结果发现模型满足抗重放性和客户端消息的保密性,不满足服务器不可伪造性。