密钥协商协议是在开放网络中实现安全通信的重要手段。借助密钥协商协议，两个或多个参与者通过利用其长期私钥和在开放网络中交换的临时消息能够生成一个共享会话密钥。此共享的秘密会话密钥被用于后续的安全通信。认证密钥协商协议不仅允许参与者建立起共享会话密钥，而且确保协议涉及参与者的认证性。认证密钥协商协议可以在多种密码体制下实现。目前，基于PKI的认证密钥协商协议获得了深入研究和广泛应用。但这类传统公钥密码体制下协议的实施需要维护、传递和验证用户公钥证书，系统开销巨大。基于身份和无证书的密码体制消除了公钥证书，避免了一个庞大PKI的需要，极大地简化了公钥的管理。由此，对基于身份和无证书密码体制下认证密钥协商协议的研究具有重要的学术价值和广阔的应用前景。同时，基于计算复杂性理论的可证明安全技术也已成为分析这两类新型认证密钥协商协议安全性的一种必要手段。本文重点对基于身份和无证书的认证密钥协商协议进行研究，其工作围绕着可证明安全协议的设计、分析及其安全模型的研究展开。主要研究内容和成果如下：1.对认证密钥协商协议的基本设计规范进行了总结，并且归纳了认证密钥协商协议的基本设计需求。2.运用双线性配对构造了两个新的基于身份的两方认证密钥协商协议，并在基于身份的eCK模型框架下进行了严格的形式化证明。利用Cash、Kiltz和Shoup在Eurocrypt2008上提出的陷门测试技术证实了第一个协议的安全性基于标准的CBDH假设，明显弱于先前某些同类协议安全性所基于的Gap假设。第二个协议的安全性虽然基于GBDH假设却具有更低的计算开销。eCK模型是目前针对两方认证密钥协商协议的赋予敌手最强攻击能力的安全模型。当前仅有少量基于身份的认证密钥协商协议是在强的eCK模型下可证明安全的。与以往大多数同类方案相比，新协议能够提供更强的安全保证；与已有eCK模型下安全的同类方案相比，在考虑离线预先计算的情形下，新协议更为高效，安全证明也更加简练和直观。3.对原始eCK模型进行适当改造，使之适合于可托管基于身份的情形；然后在此eCK模型框架下，运用双线性配对设计了四个可证明安全的可托管基于身份的两方认证密钥协商协议。利用陷门测试技术证实了其中一些协议的安全性基于标准的CBDH假设，明显弱于先前某些同类协议安全性所基于的Gap假设。与已有可托管协议相比，新协议具备更强的安全性。据我们所知，这些新方案是首批强的eCK模型下可证明安全的可托管基于身份的认证密钥协商协议。4.利用CK模型设计了一个新的适用于SIP的无双线性配对基于身份的认证密钥协商机制。新提案能够防止当前SIP认证机制及以往提案可能遭受的各种攻击。通过引入无证书密码体制中的一些设计思想，新提案不但成功避免了庞大PKI的需要，而且也解除了先前基于身份提案所存在的密钥托管缺陷。与以往使用计算代价较高的配对的基于身份和无证书提案相比，无配对的新提案由标准椭圆曲线加群构造，计算效率更高。5.在基于身份的eCK模型框架下构造了两个可证明安全的无双线性配对基于身份的两方认证密钥协商协议。利用陷门测试技术证实了第一个协议的安全性基于标准的CDH假设，明显弱于先前某些同类协议安全性所基于的Gap假设。第二个协议的安全性虽然基于GDH假设却具有更低的计算开销。新方案只需要两消息的通信，并可基于标准椭圆曲线加群来实施。目前，大多数基于身份的认证密钥协商协议需要计算复杂度较高的双线性配对操作；同时，仅有少量基于身份的认证密钥协商协议是在强的eCK模型下可证明安全的，而这其中eCK模型下安全的无配对方案更为罕见。与以往同类协议相比，新方案在安全性、效率或在这两方面都更具优势。6.通过对原始eCK模型进行扩展提出了一个用于无证书两方认证密钥协商协议研究的强安全模型，并在该模型框架下运用双线性配对构造了一个可证明安全的无证书两方认证密钥协商协议。利用陷门测试技术证实了新协议的安全性基于标准的CDH假设和CBDH假设，明显弱于先前某些同类协议安全性所基于的Gap假设。在无证书两方认证密钥协商的安全模型中，Lippold、Boyd和Nieto在Pairing2009上提出的模型被认为是目前最强的安全模型，新模型的强度可与此模型相媲美。当前在无证书密钥协商协议领域的研究相对有限，而其中仅有极少量协议在类似的强模型下是安全的。与以往同类方案相比，新协议在安全性或效率方面更具优势。