可证明思想起源于1984年Goldwasser和Micali等学者的开创性工作,他们提出了语义安全性定义,将可证明安全的思想首次带入安全协议的形式化分析中。随后,越来越多的学者采用可证明安全性理论对提出的安全协议进行形式化安全性证明。这使得可证明安全性的密码协议成为了研究热点。目前,可证明性安全可分为两大类：一类是在随机预言模型(ROM)中能证明其安全性,另一类是在标准模型中能证明其安全性。本文主要研究认证密钥交换(AKE)协议的可证明安全性。AKE协议因其具有同时实现通信各方生成共享会话密钥并完成相互身份认证两大目标的优点,得到了人们的广泛关注。本文的主要研究内容如下：(1)针对一般口令认证密钥交换协议中容易遭受服务器泄露攻击和口令猜测攻击,提出了一个基于验证值的N方密钥交换协议,VB-nPAKE。在随机预言模型中,利用“混合”技巧和游戏理论,证明敌手攻破该协议的优势是可忽略的。(2)提出两个新的具有很强灵活性和适应性的身份基认证密钥交换协议IBK-1和IBK-2,针对随机预言模型在现实中可能存在的不安全性,依据归约证明思想,给出协议在标准模型下基于判定性q-BDHI假设的安全性证明。(3)以计算上可隐藏的承诺算法,Smooth投影哈希函数和DDH假设为基础,提出一个通用的AKE协议模型,并在标准模型下给出模型的安全性证明。另外,本文还对两方的通用模型进行了扩展,提出了单服务器与跨域模式下可证明安全的三方AKE协议通用模型。