认证与密钥协商协议(Authenticated Key Agreement, AKA)是密码学的一个重要领域，它允许两个或者多个用户在不安全的网络信道上进行身份/消息认证并协商出一个共享密钥，从而建立一个安全的信道进行通信。由于AKA协议在各个现实网络中都具有着非常广泛的应用，因此它也受到了学者和工业界的高度关注。可证明安全理论是一种公理化的研究方法，它将密码协议的安全性规约到复杂的数学难题或者一些密码学基础理论。如果该数学问题被公认是难解的或者该基础理论是正确，那么基于这些困难问题或者理论所构造的密码协议就被认为是计算上安全的。目前使用可证明安全理论对AKA协议进行研究已成为国际上公认的较为有效的方法。本文以可证明安全理论为基础从理论和实际应用两个方面对AKA协议及其安全模型进行了分析和设计。理论研究方面包括对两方、三方以及群组口令AKA协议及安全模型的研究、一轮强前向安全AKA协议及其安全模型的研究。实际应用方面包括对会话初始化协议(SIP)的研究以及无线漫游认证协议的研究。取得的成果如下：(1)对一个基于口令和智能卡的两方匿名AKA协议进行了分析，指出该协议会遭受离线字典攻击以及密钥泄露伪装(KCI)攻击。给出了一个改进协议，改进协议增加了用户的不可追踪安全属性。在椭圆曲线间隙Diffie-Hellman假设(ECGDH假设)下证明了所提出协议的安全性。同已有的基于口令和智能卡的两方匿名协议相比较，所提出协议在安全性、计算消耗以及存储消耗上具有一定优势。(2)将AKA协议所需的一种强安全属性——抗临时密钥泄露攻击引入到基于口令和智能卡的AKA协议中，分别提出了基于智能卡的两方强安全AKA协议和三方强安全AKA协议。同时，给出了包含临时密钥泄露攻击的基于口令和智能卡的AKA协议的安全模型，并在该模型下给出所提协议的安全性证明。此外，文中还分析了抗临时密钥泄露攻击不能在仅使用口令的AKA协议中实现的原因。(3)对标准模型下基于口令的群组密钥协商协议进行了研究，基于平滑投影哈希函数提出了一个使用不同口令的群组AKA协议。由于不同用户使用不同口令，避免了一旦群组内的一个用户被攻陷，那么整个系统都将崩溃的危险。在平滑投影哈希函数、非交互不可展承诺方案以及DDH假设下，新的协议在标准模型下是可证明安全的。(4)对基于公钥的一轮强前向安全的AKA协议进行了研究，将密钥泄露伪装攻击进一步区分为强密钥泄露伪装攻击和弱密钥泄露伪装攻击。同时给出了一个包含该攻击的具有强前向安全属性的安全模型。在著名的mOT(MinimalOkamoto-Tanaka)协议的基础上使用NAXOS方法给出了mOT+协议并基于一个弱的假设给出了mOT++协议，在所提出模型下给出了两个协议的安全性证明。(5)从实际应用出发，对跨域SIP协议进行了研究，基于无证书公钥密码学提出了一个适用于SIP协议的跨域无证书AKA协议。新的协议允许不在同一个密钥产生中心的两个用户安全的运行SIP协议。基于间隙双线性Diffie-Hellman(GBDH)假设在随机预言模型下证明了协议的安全性。该协议中所使用的方法适用于其他跨域间用户认证，可以使得点到点通信得以实现。(6)对无线漫游认证协议进行了研究，提出了一个具有隐私保护属性的漫游协议认证框架。该框架中包含了用户和外地服务器之间的认证协议以及跨域间的用户认证协议。使用AVISPA工具对协议进行了安全性分析。结果表明所提出的认证协议具有AKA协议所应具有的安全属性。文中所用的方法可以看做是一种通用的方法，可用于无线Mesh网络以及车载网络等分布式网络。