ad hoc网协议安全性的形式化验证研究.pdf

摘要 无线移动Ad Hoc网络)作为没有基础设施 hoc网络(MANET，以下简称Ad 的网络，在军事和民用方面具有广阔的应用前景，是目前网络研究中的热点问 题。随着近年对Adhoc网络安全的研究，相关的Adhoc网络协议也在不断的改进 和完善中，网络中的攻击者以及协议无穷多个会话的并发交叠运行使得协议运 行时往往难以实现它的设计目标，对协议的安全性分析和验证显得至关重要。 形式化的方法已被证明是分析和验证安全协议的有效手段，但常规的形式化方 模型、有限状态模型(FSM)及随机预言机模型等方法大都是理想状态空间的 理论推导，逻辑性、理论性都较强，验证过程需要很长的推理步骤，为了直观 而又严密的验证协议，我们采用了AVISPA协议验证工具。 本文以Adhoc网络协议安全性的形式化验证为研究对象，以有效的形式化验 证方法为主要研究内容。本文的创新点如下： 1、通过分析比较几种常用的形式化分析方法的优点与缺点，选择AVISPA 工具集作为协议安全的形式化分析工具。 2、针对相关文献上讨论的ARAN协议能否防御内部节点攻击的问题，采用 析了ARAN协议的安全性问题，证实了ARAN协议在存在恶意节点攻击的情况 下能够成功抵御这类攻击。 3、随着网络编码技术在Adhoc网络中的应用，，网络编码协议的安全性验证 也成为一个新的研究课题。针对网络编码同态签名方案抵御内部恶意节点攻击 的安全性验证问题，本文构建了一个基于网络编码同态签名算法的网络传输协 议，然后利用HLPSL语言对该网络传输协议建立了抽象验证模型，首次利用 AVISPA工具验证了这种协议的安全性。 关键字：Adhoc网络，ARAN，AVISPA，形式化验证，网络编码 Abstract for akind hocnetworks short)is mobileAdhocnetwork(MANET,Ad Wireless hocnetworks fixedinfrastructure·Ad ofmobile networkswithout self-organized to and becausewere military f-0cuSin ofnetworksthey widelyapplied bec锄ea study Adhoc Oil of networks，therouting withtheresearch civilian security fields．Along andthe and networkattacks were perfected．However improved protocolsrapidly