第三代移动通信系统(3G)是一个在全球范围内覆盖与使用的网络系统,它向用户提供高质量多媒体通信,不仅支持传统的话音与数据业务,还支持交互式业务与分布式业务,如多媒体业务、电子商务等,这种全新的业务环境对网络系统的安全性提出了更高的要求。本文着重研究了第三代移动通信系统中EAP-AKA(Extensive Authentication Protocol Authentication and Key Agreement)协议,用串空间理论基础上建立的认证测试方法来验证EAP-AKA协议在终端(Peer)和EAP服务器端认证的正确性。首先研究了3G系统对认证协议的安全需求,描述了3G通信系统的安全体系结构和安全原则以及针对系统的攻击方法,详细分析了3G鉴权和认证过程。然后,分析了3G系统对认证协议的安全需求和认证协议面临的安全威胁;详细分析了EAP-AKA协议的流程和安全性,通过改变密钥长度改进EAP-AKA协议,利用串空间理论和认证测试构建出形式化验证方法;最后,在上述分析的基础上利用认证测试的形式化方法证明了EAP-AKA协议在终端和EAP服务器端可以实现相互的安全认证,证明了该协议在WLAN环境下为移动终端和3GPP服务器端实现安全的身份认证和密钥分发服务。