论文部分内容阅读
随着计算机通信与网络技术的发展，网络协议的稳定性和安全性发挥着越来越重要的作用，所以对网络协议的研究有重要意义。形式化的方法将成为分析网络协议的重要方法，目前有很多研究网络协议的理论和方法，比较重要的理论有BAN逻辑，定理证明和模型检测等，而模型检测作为形式化分析理论方法中的一种，有着自动化和提供反例等优点，基于此，我们采用形式化方法和模型检测工具来检测网络协议的漏洞也是很有意义的，从而达到提高网络协议安全性和稳定性的目的。
本文首先在介绍网络协议、形式化方法和模型检测工具及其应用的基础上，通过不同的安装环境对SIPN工具使用做了介绍，并对形式化描述的几种语言进行比较；其次，介绍了OSPF路由协议的概念、特性和协议的操作及工作过程，同时采用形式化方法的FSM分析了OSPF协议；接着重点分析了OSPF网络类型、报文头部、报文处理流程和LSA处理流程；紧接着通过SPIN模型检测工具对OSPF协议进行抽象化建模，描述了OSPF协议的LTL性质，并刚XSPIN模型检测工具进行了检测验证，得到了运行轨迹，在此基础上又采刚稳定状态验证的方法从可行性和正确性等方面验证了OSPF路由协议；最后总结本文的主要工作并对尚需完善的工作进行展望。
本文采用的主要方法和技术如下：⑴采用形式化的分析方法，对OSPF协议分析；⑵SPIN适用于并行系统，本文探讨了在Windows、Java、Cygwin等环境下对SPIN工具的安装和使用，并详细介绍了SPIN的图形界面工具XSPIN的安装过程和功能的使用，并通过AB协议进行分析、验证，从而得到协议不容易发现错误，模型检测工具的使用作为本文的主要技术支持。
本文的特色和创新之处在于：①采用形式化的方法分析网络协议，并用有限状态系统的描述语言Promela对OSPF协议进行建模；描述了OSPF协议的LTL性质，用XSPIN模型检测工具进行了检测验证，得到了运行轨迹；②采取稳定状态验证的方法从可行性和正确性等方面验证。