在移动自主网络中协议是主要的研究领域之一,由于移动自主网络的性质与传统有线网络比较起来又形成了许多新的挑战,已存在的路由协议大多是资源集中型的,不适合于移动自主网的特点和应用,针对移动自主网的特点,应用不同的方法来解决移动自主网的路由协议已被提出,安全路由协议也正在研究和提出,IETF(互联网络工程任务组)针对此目标也成立一个MANET工作小组。安全路由协议的分析是一个复杂的问题,安全路由协议的安全性满足与否直接影响到移动自主网的推广与应用。在安全路由设计的早期工作中若没有相应的方法来检测路由协议的安全性,潜在的协议漏洞没有合适的方法来检测,则网络操作很容易被攻击而不能工作,就会造成许多不必要的浪费。针对此目的,目前已有许多推理方法应用于安全路由协议的分析,但这些方法大都是模拟方法以及逻辑推理和状态空间搜索,通过对有限的状态、结点分析得出结论。这些方法至少得到下面这两个不令人满意的方面:(一)没有明确的“安全”路由的定义,所以不同的作者应用不同的方法来解释安全性,并且应用不同的需要来设计他们的安全路由协议,结果不同的方法的属性难以比较;(二)没有严格的数学方法来证明一个提出的安全路由协议。事实上许多被提出的协议如SRP和Kerberos都有缺陷,在一定意义上都没有达到作者所声称的安全属性;明显的原因是缺乏充分的证明技术。 应用形式化分析安全路由的方法还很少,应用进程代数的来分析的方法更少。应用进程代数的方法来分析安全路由的安全性,能克服非形式化中不必要的人为干预和经验推理,能严格按照数学的语法、语义来实现安全目标的分析。 本文研究基于SPI演算的移动自主网络的安全路由协议分析是把进程代数中SPI演算引入到MANET中,并进行安全路由协议分析,主要是由于SPI演算具有丰富的语法、语义和成熟的推理过程,使得安全路由协议的分析有一个严格的算法过程。 对著名的SRP路由协议我们用SPI演算来分析其过程,在本文提出的攻