随着无线网络在各领域的广泛应用和不断发展，人们越来越关注无线网络的安全问题。无线信道的开放性和不稳定性使得无线网络面临着较大的安全风险；移动终端在硬件资源上不同程度的限制也决定了某些密码技术无法适用于无线环境；不同类型和用途的无线网络也对安全性和相关实现技术有着不同的要求。由于和有线网络的巨大差异，现有众多的安全方案和技术并不能直接用于无线网络，而且无线网络环境的复杂性和不稳定性也使得安全目标的实现困难重重。 安全协议作为网络安全通信系统的核心技术，其重要性不言而喻。然而，如何分析安全协议的安全性，从而证明安全协议的有效性？如何设计安全协议，从而确保所设计协议的安全性？这些则都是需由安全协议形式化方法来解决的问题。安全协议的形式化方法作为安全协议分析和设计的理论基础，自Dolev和Yao的开创性工作以来，目前已有了较大的发展，形成了两大流派，其中典型的有串空间模型理论等。然而，在如何应用抽象的形式化理论或方法来研究现行通信系统中大型、复杂并行系统的安全协议，发现其安全缺陷或证明其安全性？在如何扩展现有形式化理论，使之能够解决网络中出现的新的威胁？以及在如何应用形式化理论指导安全协议的设计等几个方面还有待进一步的研究。 鉴于此，本文基于串空间模型理论，针对无线网络中上述的问题进行了深入的研究，并提出了一些有效的解决方案，得到了一些研究成果。主要工作有： 1.基于扩展的串空间模型，对IEEE802.lli协议进行分析，发现了四步握手协议在协议可用性上存在的漏洞，并提出了修改方案，最后对修改后的协议进行形式化证明； 2.基于扩展的串空间模型，对IEEE802.16e相关安全协议进行了分析，发现了IEEE802.16ePKMv2_EAP_TLS认证的一个安全漏洞，并提出相应修改，同时也对修改后的协议进行形式化验证； 3.提出了基于串空间模型指导的安全协议设计方法，并设计一个目标用于GSM网络语音通道端剑端安全通信的认证与密钥交换协议，并对其做出形式化安全性分析，证明了其安全性。