论文部分内容阅读
IPv4的局限性随着Internet的飞速发展日益显现，而IPv6引入了许多新特性，比如地址空间的扩大、报头格式的简化、对安全性支持的增强等，这些使得它必将成为新一代的IP协议标准。本文首先对IPv6的地址结构、报头格式、邻居发现、IPsec安全机制、路由协议等关键技术进行了介绍，为后面的分析做基础。协议的安全是网络安全性的保证，为了尽可能找出协议中潜在的安全漏洞以改进协议的安全性，需要对协议的安全性进行分析。分析方法有两类：非形式化方法和形式化方法，非形式化方法又叫攻击检验方法；形式化方法提供了一个框架，其本质是基于数学的方法来描述目标软件系统属性的一种技术。本文对IPv6协议的安全性分析中，首先利用常规的分析方法，也就是攻击检验方法对IPv6的若干关键技术的安全性进行分析，依据协议的运行步骤、参与方等分析协议存在的问题，分析漏洞存在的可能性，然后在分析的基础上，尽可能的提出改进的措施，这是本文中，我工作内容的一个方面。本文中，我另外的工作部分是参与SPIN模型检测工具的改进。在对协议安全性分析的形式化方法中，因为对大规模协议验证的支持和自动化程度高的优势，模型检测有着广泛的应用。本文首先概括的说明了协议分析的形式化方法；进一步对形式化方法中的模型检测的相关技术研究点—模型检测工具SPIN、建模语言Promela进行了介绍，重点描述了我们团队对SPIN的改进。我的第三个工作部分是利用我们改进后的模型检测工具对IPv6的安全机制——IPsec协议提供的安全性进行形式化验证。对IPsec安全性进行形式化验证主要以ESP的安全性验证为主，其中对ESP协议进行Promela建模仿真是对ESP协议安全性验证的关键，建立攻击者模型则又是建立ESP协议Promela模型的关键。在建立ESP协议的Promela模型中，我尽可能的采用了原子操作，这样可以尽可能地减少协议模型验证过程产生许多不必要的状态空间，提高验证的时间、空间效率。最后根据验证结果尽可能提出改进措施。