随着计算机网络的广泛应用,人们对网络的依赖程度越来越高,与此同时网络安全问题也变得越来越重要。尤其近年来,新兴的移动Ad Hoc网络快速发展,由于其采用了更为开放的网络体系结构和传输媒介,任何在网络覆盖范围内的人员都可以发送或接收信息报文等,其网络安全将面临更严重的威胁。安全路由协议是构建移动Ad Hoc网络安全环境的基础,其安全性对整个网络环境的安全起着至关重要的作用。设计和分析安全路由协议已经成为一项极为重要的研究课题,也是一项富有挑战性的任务。因为传统网络的安全技术不能直接应用到移动Ad Hoc网络中,而且表面是安全的路由协议可能包含攻击者可以利用的微妙的缺点,大量的事实表明,有许多安全路由协议即使经过安全专家的仔细分析设计后仍然存在漏洞。为了保证安全路由协议的安全性,研究人员提出使用形式化分析方法指导移动Ad Hoc网络安全路由协议的设计和分析。其中,串空间模型就是典型形式化分析方法,给安全协议的设计与分析带来了极大的变革,本文将通过对串空间模型的研究来解决移动Ad Hoc网络安全路由协议的安全方面的问题。本论文首先阐述了安全协议和形式化分析方法的相关知识,在此理论基础上,后文重点研究串空间模型形式化分析方法。通过对串空间模型进行深入的分析研究和扩展,并利用简单的应用实例说明串空间模型在分析安全协议的安全性上所具有的优点:简洁、明了、有效。最后,对移动Ad Hoc网络的安全路由协议及其形式化分析方法进行了分析研究。通过攻击实例来分析现存的移动Ad Hoc网络安全DSR路由协议(SRP安全路由协议和Ariadne安全路由协议)的安全性存在的漏洞,在此基础上,提出新的DSR安全路由协议模型—Ariadne-S模型,并使用串空间模型形式化分析方法对该路由协议模型的安全性进行分析证明。