认证密钥交换协议是广泛应用于开放网络环境的重要密码学构件，其目的是让通信实体之间通过协商共享会话密钥建立起安全的通信信道。　　认证密钥交换协议的安全性分析依赖于形式化的安全模型。安全模型通过定义攻击者能力和协议安全性来刻画信息泄露和安全需求，是指导协议设计与分析的基础性理论工具。在原始Bellare-Rogaway模型的基础上催生了许多新的安全模型，但是这些安全模型对会话状态的描述过于笼统和片面，导致某些重要的攻击类型难以刻画，大大降低了协议的安全需求。因此，如何定义合理且便于协议分析的安全模型是本文的主要研究内容。　　完备前向安全和可否认性是认证密钥交换协议重点考擦的安全属性，长期得到学界的关注。一方面，完备前向安全要求用户长期私钥的泄露不会暴露之前分发的会话密钥;另一方面，可否认性要求报文接收方不能向第三方证明某用户曾与自己协商过会话密钥，用于保护用户通信的隐私性。因此，如何设计满足完备前向安全和可否认性的认证密钥交换协议是本文考察的另一个重点。　　本文对认证密钥交换协议及其安全模型进行深入研究，研究成果主要包括:　　1.本文提出了统一标准化的安全模型。该模型对信息泄露类型进行细致的划分，严格规定攻击者的能力，保证在合理范围内最大化信息泄露程度，为协议的安全性分析提供统一的标准。另外，为了展示该模型的合理性和实用性，本文对NAXOS协议进行适当修改，充分展示协议在随机预言机模型和GapDiffie-Hellman假设形式化下满足统一标准化安全模型的安全性定义。　　2.本文应用显式认证方法设计满足完备前向安全的基于身份的认证密钥交换协议。该协议结合了IB-KA协议和Schnorr-like签名体制，通过数字签名的不可伪造性有效排除了主动攻击。另外，借助随机预言机模型和计算性Diffie-Hellman假设充分证明协议在Canetti-Krawczyk模型下提供完备前向安全，证明过程简洁易懂，无需依赖非标准假设。　　3.本文借助非交互式指定验证方知识证明体制设计了同时具备前向安全和可否认性的AKE协议。文章首先形式化定义了AKE协议的可否认性和非交互式指定验证方知识证明。在此基础上提出了高效的非交互式指定验证方知识证明体制，充分展示该体制在随机预言机模型和计算性Diffie-Hellman假设下满足非交互式指定验证方知识证明的所有安全属性。最后结合原始Diffife-Hellman协议和非交互式指定验证方知识证明体制提出了满足完备前向安全和可否认性的AKE协议，在随机预言机模型和计算性Diffie-Hellman假设下证明了协议的相关安全属性。