随着网络技术的飞速发展,网络安全问题日趋严重。安全协议是信息安全的一个重要研究方向,它是构建网络安全环境的基石,其安全性对整个网络环境的安全起到了至关重要的作用。虽然安全协议的设计和分析已历经了三十余年的发展,但是由于安全协议设计的复杂性、网络攻击方式的多样性和运行环境的差异性,使得安全协议的设计和分析仍然面临诸多困难和挑战。形式化分析方法是安全协议分析中最重要的工具之一。随着安全协议研究的发展,出现了各种各样的验证模型和分析方法。虽然这些形式化方法已经成功地发现了许多安全协议的漏洞和攻击,但是它们都有各自的局限性。有些分析方法不完善,定义的结构简单,无法对复杂协议进行分析；有些分析方法在设计时,自身就存在安全隐患。在诸多的形式化分析方法中,串空间理论以简洁、严谨和高效等特点成为近年来形式化分析领域的研究热点,它将安全协议的形式化分析方法的研究推向了一个新的高度。本文以串空间理论为基础,对经典认证协议、无线网络安全协议,Ad hoc网络安全路由协议和群组密钥协商协议的设计和分析进行了深入研究,取得了一些重要的研究成果。对串空间理论在典型安全协议中的应用进行了研究,使用串空间理论分析了Yahalom-Paulson协议的安全性,发现协议在认证性上存在缺陷。针对协议存在的攻击,对协议进行了重新设计,给出了改进后的协议,改进协议在认证性方面弥补了Yahalom-Paulson协议的不足。使用串空间理论对CCITTX.509(3)协议的安全性进行了分析,发现协议中存在认证缺陷,并给出了针对协议漏洞的攻击过程。对串空间理论的设计进行了深入研究,在攻击者模型中添加了攻击者行为,丰富了攻击者迹和密码学原语,重新定义了串空间理论中的相关概念,并对衍生出的命题、定理、推论等进行了证明。针对sever-specific MAKEP协议存在的安全缺陷,提出了一个新的双向认证和密钥交换协议(Eserver-specific MAKEP协议)。使用扩展的串空间理论分析了Esever-specific MAKEP协议的安全性,证明了协议不但能够抵御未知的密钥共享攻击,而且能够避免服务器对生成共享密钥的控制。使用扩展的串空间理论对SNEP的节点间密钥协商协议的安全性进行了分析,发现了协议在认证性上存在安全缺陷,即攻击者可以冒充合法用户完成密钥协商。针对此缺陷,对协议进行了重新设计,给出了一个改进协议。使用扩展的串空间理论分析了改进协议的安全性,证明了改进协议能够满足认证性和保密性两个安全目标。通过对以上协议的分析和证明,也说明了扩展的串空间理论的正确性,扩大了串空间理论的应用范围。对Ad hoc网络安全路由协议的设计和分析进行了深入研究。为了能够使用串空间理论分析Ad hoc网络路由协议的安全性,针对Ad hoc网络安全路由协议的特点,扩展了串空间理论中的“正确性”概念,增加了攻击者的行为。使用扩展的串空间理论分析了ARAN路由协议的安全性,发现了该协议存在重放和合谋两种攻击。提出了一个新的Ad hoc网络安全路由协议(eARAN协议),使用扩展的串空间理论证明了eARAN协议的安全性。由此可见,基于扩展的串空间理论分析Ad hoc网络安全路由协议的新方法是有效的,成功地将串空间理论的应用范围拓展到分析Ad hoc网络安全路由协议领域。对群组密钥协商协议的设计和分析进行了深入研究。分析了基于身份的群组密钥协商协议HTK协议的安全性,发现了HTK协议无法抵御组内合法用户的共谋攻击(insider attack)。分析了认证群组密钥协商协议DB协议存在的安全缺陷,提出了个新的动态认证群组密钥协商协议(EDB协议)。基于串空间理论的基本思想,提出了一个分析群组密钥协商协议静态和动态安全性的新方法,应用该方法分析了EDB协议中密钥协商子协议、用户加入子协议和用户退出子协议的安全性,证明了协议满足保密性和认证性两个安全目标。通过对群组密钥协商协议的成功分析,也证明了基于串空间理论分析群组密钥协商协议安全性的新方法是正确、有效的,进一步扩大了串空间理论的应用范围。