安全协议的设计极其容易出错,而且其缺陷也很隐蔽。利用形式化方法验证安全协议在发现漏洞、改进设计、保证安全功能等方面具有不可或缺的作用。随着新兴网络类型的出现和网络应用的发展,安全协议的种类和目标也越来越多样化,对形式化验证提出了进一步的要求。首先,形式系统需要语法构件对安全协议中出现的新的计算和通信行为进行规范;其次,在形式系统中协议的安全属性应该易于规范和验证。目前针对移动自组织网络安全协议验证的研究相对于安全协议本身的设计研究来说还显得非常不足。本文针对移动自组织网安全协议对安全路由、匿名路由的形式化验证分别进行了深入的研究,并且将研究的方法学延伸至可信信道的安全评估中去。具体来说,其贡献可概括为以下几点。　　 (1)提出了受拓扑限制的邻域通信演算(NCCC)以及相应的类型系统。NCCC支持对邻域通信和存储行为的建模;分析了安全路由属性并将其规范于NCCC的类型系统中,相对已有安全路由的研究,本文对安全路由的界定更加精炼,有效地降低了验证的复杂性:在类型推理中利用协议消息格式约束了攻击者模型,保证验证过程的可终止性。对SAODV协议的分析证明了方法的有效性。　　 NCCC通过受类型约束的存储变量实现了对存储行为的建模。在基于规约的操作语义中网络拓扑被规范为一个用来约束通信进程规约的边集,实现了对邻域广播的建模。在类型系统中处于不同方位(相对恶意节点)的通信节点被赋以不同的节点类型,一次安全的路由被定义为具有源节点侧类型的节点的存储符合网络拓扑,这个判断体现在类型系统中:如果具有源节点侧类型的节点存储了不符合网络拓扑的项,即产生一个类型错误——安全路由的失败。攻击者的建模是基于协议消息格式进行的,根据欲验证协议的消息格式来构造攻击者在协议运行过程中可能掌握和生成的消息,消息格式把那些因为格式原因而不会被正常节点接收的消息从攻击者的知识集合中过滤掉,从而使推理时面临的可能性空间显著缩小。　　 (2)提出了支持并发存储行为的对象演算(SCCO)及控制流分析理论。SCCO可以作为ad hoc网络安全协议的规范语言,支持对存储更新行为的建模,此特点使其能够更准确地对ad hoc协议的多路径路由请求的运行模式建模。本文给出了在控制流分析中集成攻击者模型的方法,使安全分析可以直接利用控制流分析的技术而无需显式地规范攻击者的行为。　　 利用SCCO规范移动自组织网安全协议时,对象可以是节点或网络,节点存储由对象的可重写常数方法表示,节点对象可以与网络对象通过异步的方法调用交换消息。SCCO的形式语义是基于堆存储的操作语义,为保证存储更新的一致性,对象的改写和扩展实际上是针对堆中对象集合在身份等价关系下的等价类进行的。因为网络对象的存在,控制流分析中的函数调用约束规则中的信息流可以模拟攻击者和正常节点间的信息流。　　 (3)提出了验证匿名路由协议的Epistemic Cord Logic(ECL)。ECL对匿名路由协议验证的贡献在于两点:ECL着重于对攻击者辨别消息、追踪消息传播能力的建模,在此基础上我们定义了匿名路由的属性规范;ECL支持模块化验证方法,明确了匿名路由协议的安全属性组成结构,将匿名路由从其它匿名需求中独立出来。我们对ANODR协议进行了验证,指出其不能满足路径匿名的要求。　　 移动自组织网匿名路由协议的验证相对传统安全协议而言有着不同的特点:协议的匿名性不是一个单纯的目标,而是由数个子目标构成,比如发送匿名、接收匿名以及路径匿名。这个特点使其非常适合先分解、再验证的方法。我们扩展了Cord Logic的语法,重新构造了语义模型,显式地在cord空间中增加了节点知识集,节点知识集允许利用重解释函数来判别攻击者在既得信息下对加密消息的辨别能力。　　 (4)提出了模块化验证的方法并将其应用在安全评估中。为了在安全评估中能够应用协议分析的成果,提出了可信信道的评估体系;基于现有应用级别协议的构造方式提出了分解协议分量和构造证明的方法。对SSH协议的评估说明这种模块化的验证方法使可信信道安全评估的复杂性维持在一个可操作的水平上,并且由于整个评估建立在可靠的公理证明系统之上评估的可靠性也都得到了保证。　　 协议的分解是基于协议构成方式进行的,将待评估协议分解为若干个较为简单的协议分量,这些分量相对独立同时又有一定的依赖关系;每个分量可以利用协议分析技术单独验证,然后把验证结果按分解结构综合起来。另外,根据分析对象的不同我们可以在保证逻辑可靠性的前提下扩充整个逻辑的原语、语义模型以及公理系统,这使安全评估具有了灵活性的特点。