无线移动Ad hoc网络(MANET,以下简称Ad Hoc网络)作为没有基础设施的网络,在军事和民用方面具有广阔的应用前景,是目前网络研究中的热点问题。随着近年对Ad hoc网络安全的研究,相关的Ad hoc网络协议也在不断的改进和完善中,网络中的攻击者以及协议无穷多个会话的并发交叠运行使得协议运行时往往难以实现它的设计目标,对协议的安全性分析和验证显得至关重要。形式化的方法已被证明是分析和验证安全协议的有效手段,但常规的形式化方法,如Needham等人提出的BAN逻辑以及后来改进的AT逻辑及SVO逻辑、Perti模型、有限状态模型(FSM)及随机预言机模型等方法大都是理想状态空间的理论推导,逻辑性、理论性都较强,验证过程需要很长的推理步骤,为了直观而又严密的验证协议,我们采用了AVISPA协议验证工具。本文以Ad hoc网络协议安全性的形式化验证为研究对象,以有效的形式化验证方法为主要研究内容。本文的创新点如下:1、通过分析比较几种常用的形式化分析方法的优点与缺点,选择AVISPA工具集作为协议安全的形式化分析工具。2、针对相关文献上讨论的ARAN协议能否防御内部节点攻击的问题,采用HLSPL语言对ARAN协议建立了抽象模型,利用AVISPA工具集形式化验证分析了ARAN协议的安全性问题,证实了ARAN协议在存在恶意节点攻击的情况下能够成功抵御这类攻击。3、随着网络编码技术在Ad hoc网络中的应用,网络编码协议的安全性验证也成为一个新的研究课题。针对网络编码同态签名方案抵御内部恶意节点攻击的安全性验证问题,本文构建了一个基于网络编码同态签名算法的网络传输协议,然后利用HLPSL语言对该网络传输协议建立了抽象验证模型,首次利用AVISPA工具验证了这种协议的安全性。