自从Bellare和Rogaway提出随机预言模型(Random Oracle Model, ROM)方法论,并将可证明安全的思想首次带入安全协议的形式化分析中以来,许多学者也相继应用ROM对提出的安全协议进行了形式化安全证明。ROM方法论的出现,使得过去仅作为纯理论研究的可证明安全性理论,迅速在实际应用领域取得了重大进展,具有重要理论应用价值。本文主要研究面向AKE协议的可证明安全性模型。AKE协议因其具有同时实现通信各方生成共享会话密钥并完成相互身份认证两大目标的优点,得到了人们的广泛关注。本文的主要研究内容如下：(1)提出一则包括服务器和三个客户端在内的基于威尔配对的四方口令AKE协议。(2)分析并讨论4PAKE协议在改进的BPR2000敌手通信模型中的安全性。通过形式化敌手的攻击能力,并定义协议安全目标,利用“混合”技巧和游戏理论证明敌手攻破4PAKE协议的优势是可忽略的,4PAKE协议是可证明安全的。(3)针对当前主流敌手模型的不完备性,提出一个面向AKE协议新的敌手通信模型：在具有一般攻击能力的基础上,丰富敌手可能进行的攻击类型,充分考虑敌手的攻击场景,并据此给出新模型下的强安全性定义。在新模型下,发现4PAKE协议的安全缺陷,并针对每个缺陷给出修改方案,改进后形成新4PAKE协议。新的4PAKE协议较其他同类方案具有密钥规模小、计算速度快、通信代价低等明显优势,且在新敌手模型中被证明是安全的。本文的研究结果表明,具有强安全性定义的新敌手模型在对AKE协议设计和安全性分析方面和主流模型相比适用范围更广。