认证密钥交换协议旨在为用户分发安全的会话密钥，使用户能借助安全的会话密钥以及相应的密码算法进行安全通信。近年来，该类协议被广泛应用于保密通信、安全认证以及电子商务等领域，是密码学领域的重要研究内容之一。传统研究往往假设协议用户的所有计算都在受保护的设备中进行。然而，在实际应用中，协议常在带泄露的计算环境中执行，即用户的长期私钥保存在低计算性能的可信设备，而用户的临时计算则在较高计算性能的非可信设备中完成。已知文献指出，非可信设备上的临时计算结果(也称临时状态)的泄露破坏了一些经典协议的安全性，并为协议的设计与分析带来了新的挑战。因此，设计与分析抗临时状态泄露的认证密钥交换协议是极具理论意义和实用价值。　　分析现有协议在攻击模型下的安全性，弱化现有协议的安全假设，以及设计标准模型下可证明安全的协议，都是制约着设计实用密码协议的关键问题。本文借助可证明安全技术对该领域展开研究，并取得如下成果：　　1、为描述会话秘密元泄露下的协议安全性，本文基于Canetti-Krawczyk模型提出vCK模型，并在vCK模型下形式化分析Ustaoglu在ProvSec2009上提出的UP协议，指出该协议存在密钥泄漏伪装攻击和秘密复制攻击。进一步地，通过绑定协议秘密元与相应的会话，本文设计UP协议的增强版本(UP+协议)，以对抗上述两类攻击。在随机预言模型下，UP+协议基于GapDiffie-Hellman(GDH)问题可证明安全。UP+协议的执行效率与原协议相当，但其具有更强的安全属性。　　2、利用孪生技术(TwinningTechnique)与HMQV密钥派生算法相结合设计TMQV协议。与现有工作不同的是，TMQV协议一方面不依赖GDH假设，另一方面能对抗临时状态泄露攻击。在安全证明过程中，借助陷门测试技术，摆脱协议对GDH假设的依赖；利用seCK模型刻画临时状态泄露下的协议安全性，并证明TMQV协议符合seCK模型的安全定义，从而得出TMQV协议在临时状态泄露下的可证明安全性。通过与相关工作相比，TMQV协议借助较弱的安全假设得到更强的安全属性，而且协议依然具有较高的执行效率。　　3、基于LaMacchia等人提出的eCK模型，本文提出模块化的协议设计与分析方法，定义模块化的eCK模型(简称meCK模型)，以构造出不依赖随机预言模型的协议。借助该模块化设计与分析思想，本文设计了一种高效且在标准模型下可证明安全的认证密钥交换协议(称为UPS协议)。与其它标准模型下可证明安全的协议相比，UPS协议所需的密码假设更弱、更标准，且协议的指数运算次数降低了50％～67％。最后，UPS协议的构造与安全性验证了所提出的模块化方法的合理性和有效性，并解决了ProvSec09上的一个公开问题。