论文题目：SAVI-DHCP协议的形式化建模与分析

摘要：随着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协议机制的可用性。

关键词：IPv6;SAVI-DHCP协议;安全协议;形式化分析与验证;源地址验证

学科专业：工程硕士（专业学位）

摘要

abstract

第一章 绪论

1.1 研究背景及意义

1.2 研究现状与相关工作

1.3 研究贡献与研究内容

1.4 本文组织

第二章 SAVI-DHCP与形式化验证方法

2.1 DHCPv6协议

2.1.1 DHCPv6消息类型

2.1.2 DHCPv6工作原理

2.2 SAVI-DHCP协议

2.2.1 SAVI-DHCP协议概述

2.2.2 绑定状态表BST

2.2.3 DHCP-Snooping过程的有效事件

2.3 形式化方法CSP理论与模型检测工具PAT

2.3.1 通信顺序进程CSP

2.3.2 模型检测工具PAT

2.4 本章小结

第三章 SAVI-DHCP的形式化建模

3.1 架构抽象

3.1.1 模型主体

3.1.2 消息通道

3.2 DHCPv6客户端和服务器模型

3.2.1 客户端、服务器消息建模

3.2.2 DHCPv6Client()进程和DHCPv6Sever()进程建模

3.3 SAVIBST()进程建模

3.3.1 内部系统消息建模

3.3.2 辅助队列与管道建模

3.3.3 SAVILaunch()进程建模

3.3.4 SAVIAPI()进程建模

3.3.5 SAVIProcessor()进程建模

3.3.6 BSTDictionary()进程建模

3.3.7 内部系统SAVIBST()建模

3.4 SAVI-DHCP整体系统建模

3.4.1 SAVI设备消息建模

3.4.2 SAVI()进程建模

3.4.3 SAVI-DHCP整体系统建模

3.5 本章小结

第四章 SAVI-DHCPv6的模型验证

4.1 SAVI-DHCP内部系统性质验证

4.1.1 性质分析

4.1.2 模型实现

4.1.3 性质验证与验证结果

4.2 SAVI-DHCP整体系统性质验证

4.2.1 性质分析

4.2.2 模型实现

4.2.3 性质验证与验证结果

4.3 本章小结

第五章 案例实验

5.1 案例背景分析

5.2 添加入侵者的案例建模

5.3 优化方案

5.4 案例验证与验证结果

5.5 本章小结

第六章 总结与展望

6.1 总结

6.2 展望

参考文献

致谢