随着移动通信技术的快速发展,移动通信系统为人们提供了越来越多的新业务。这些新业务在丰富人们生活的同时,自身的安全问题也日益暴露出来。越来越多的攻击者通过伪基站攻击方式,破坏信息的安全传递和网络资源的合法使用。为了应对这些攻击和破坏,第三代移动通信系统应用认证与密钥协商协议(Authentication and Key Agreement, AKA)作为接入域的安全措施,这对保护移动通信网络的安全起到了重要的作用。AKA协议是国际移动电信组织3GPP(The Third Generation Partnership Project)在研究2G安全脆弱性的基础上,针对3G接入域安全需求提出的安全规范。AKA使用挑战应答机制,完成用户和网络间的身份认证,同时基于身份认证对通信加密密钥进行协商。通过认证和加密手段更好的预防攻击行为,保护移动通信网络资源的安全。但该协议仍然有不足之处,而且关于AKA协议脆弱性的研究方法也比较单一局限,在协议建模、攻击建模、方案的改进和有效性证明等方面有待进一步研究。本文在系统研究3G安全体系理论基础上,对3G系统中的认证与密钥协商协议进行了详尽深入的研究,分析了该协议的不足之处,在AKA协议建模、AKA协议攻击建模、攻击模型有效性证明和AKA协议认证方案的改进方面提出了新的设计和实现方法,其成果将为建立一个安全的3G网络接入域提供理论基础。论文主要工作如下：1、在3G安全协议方面,深入研究了3G的安全体系结构、AKA协议的安全机制和AKA协议的认证过程,分析了AKA协议存在的脆弱性。同时深入研究了以SVO逻辑为代表的形式化分析方法。2、在AKA协议建模方面,基于有限状态机理论,建立了AKA协议状态机模型,对AKA协议的功能和协议参与实体的行为进行了建模分析,将原来分散的协议功能、行为、认证信息进行了形式化描述,大大规范了协议的实现,为AKA协议的安全性分析打下坚实的基础。3、在建立攻击模型方面,在分析AKA协议中存在的弱点的基础上,针对AKA认证过程,提出了中间人拒绝服务攻击模型。从攻击角度对AKA协议在无线域和有线域中所面临的安全威胁进行分析。攻击模型覆盖了有线域和无线域,因此具有普遍性,有助于在理论基础上分析AKA协议的脆弱性。4、在攻击模型有效性证明方面,根据建立的AKA协议状态机模型,证明了文中提出的中间人拒绝服务攻击模型的有效性,该证明过程有助于改进AKA协议的安全机制。5、在AKA协议认证方案的改进和形式化证明方面,针对AKA面临的攻击威胁,提出了一种基于随机数、非对称密码体制和签名机制的认证方案。同时对改进的方案进行了SVO逻辑形式化证明,证明改进的协议具有较强的安全性,为构筑安全的3G网络接入域提供理论支持。