认证密钥交换协议主要用于用户间安全密钥的分发，为用户进一步使用会话密钥进行安全通信提供安全基础，是一种重要的密码学原语构件。本研究重点关注于设计攻击者能力更强的协议安全模型，及设计可抗量子攻击的认证密钥交换协议。本文以密钥交换协议可证明安全技术及格密码技术为基础，对强信息泄露环境进行形式化，设计新型协议安全模型，使用基于格的困难问题展开协议设计，并完成如下工作。　　设计攻击者能力更强的新模型。为了对现实环境的协议攻击者能力进行形式化，我们首先设立协议的实现环境，根据协议执行过程的环境将涉及的数据进行分类，并严格将各类数据与攻击者获取该数据的行为一一对应，最后，我们使用预言机查询对攻击者的行为进行形式化。值得注意的是，该模型同时支持临时密钥泄露查询和会话状态泄露查询，本文提出的模型同时比Canetti-Krawczyk（简记CK）模型和扩展Canetti-Krawczyk（extended CK，简记eCK）模型更强。　　设计在新模型下可证明安全的经典协议。新模型同时允许会话状态和临时密钥泄露，传统协议如HMQV和NAXOS等协议的证明中均只允许其中一种泄露查询，因此我们需要设计新的协议，在新模型下可证明安全。我们在OAKE协议的基础上，应用NAXOS技术，严格规范协议的执行过程，并对协议安全性进行证明。从在线效率来看，协议只需要一次指数运算和若干哈希运算。此外，基于新模型，我们给出了NAXOS技术的现实应用场景，对其合理性进行了阐述。　　设计在新模型下可证明安全的基于格的协议。基于格的困难问题目前能抵抗量子攻击，本文首先给出一个基于格的被动安全的密钥交换协议，并结合“质询-应答”构件，得到基于格的隐式认证密钥交换协议。区别于Fujioka等人的通用构造，该协议不需要额外借助选择密文安全的密钥封装机制，并且在构造中使用的模数对于安全参数为多项式大小，实现高效。最后，我们给出了该协议在新模型下的安全性证明。　　总而言之，本研究整合CK和eCK模型，提出一个攻击者能力更强的安全模型，并且分别设计了一个经典安全协议以及一个基于格的安全协议，均在新模型下可证明安全。上述工作具有以下创新意义。　　将经典安全模型-CK模型和eCK模型进行整合，得到描述能力比之前两个模型严格更强，并且也更加清晰的新的AKE安全模型。　　提出在新模型下可证明安全的强安全经典协议，该协议具有比HMQV协议、NAXOS协议更优的在线执行效率。　　基于格困难问题设计在强安全模型下可证明安全的协议，该协议实现隐式认证，使协议具有很好的匿名性和可否认性;此外，不需要借助选择密文安全的黑盒构件，安全性直接基于格上困难问题假设。