随着3G网络与无线局域网的普及,无线网络通信技术已经在我们的日常生活中无处不在了。无线Mesh网(Wireless Mesh Network)简称WMN作为一种新型的无线网络,由于其自组织,自适应,成本低,多跳,与其他网络兼容好等特点逐渐成为下一代无线通信的核心技术。尽管现在的无线网络中有很多安全机制来保障网络安全,但由于无线 Mesh网自身的特点,这些安全机制不能完全地应用到无线Mesh网中。路由安全是无线Mesh网安全的一个重要方面,网络的安全传输,离不开路由协议的安全保障,恶意节点通过攻击路由协议,假冒正常的节点并且插入伪造路由信息来攻击网络,一旦路由协议受到攻击,其余的安全措施都变得毫无意义。　　安全协议的形式化验证方法是指用数学或者逻辑模型对所建立的模型进行分析验证,从而在理论上证明其安全性。颜色Petri网是一种图形化的建模语言,采用颜色 Petri网对安全问题进行建模分析具有很多独特的优点。比如,颜色Petri网有自动化分析工具如CPN Tool;可以采用状态空间分析和关联矩阵分析;用颜色 Petri网建模可以有效地验证安全协议的安全性,颜色 Petri网不但可以检测出模型中存在攻击,当安全协议中没有攻击时,颜色Petri网可以有效地证明其安全性。因此研究基于颜色Petri网的无线Mesh网安全协议建模和验证具有重要的理论意义和应用价值。　　本文通过分析研究现有无线 Mesh网路由协议的运行机制和各种形式化验证方法,首次提出了用颜色 Petri网对无线 Mesh网路由协议 HWMP进行建模和安全验证。通过对HWMP路由协议进行建模分析,Petri网模型可以有效地模拟仿真HWMP路由协议按需路由建立过程。用状态空间方法和CPN Tool仿真实验分析该模型,可以证明该模型中是否存在黑洞攻击。对于存在黑洞攻击的模型,通过研究现有的基于密码机制的安全路由方案和基于信任和检测机制的安全路由方案,本文提出了一种基于公开密钥加密机制的安全路由算法,用NS2对基于公开密钥机制的安全方案进行仿真实验,实验结果说明该安全方案可以有效地防止黑洞攻击对网络造成的影响。用颜色Petri网对该安全路由算法重新建模分析,通过状态空间方法和CPN Tool仿真实验,证明模型中不存在黑洞攻击,从而证明该基于公开密钥加密机制模型的安全性。