可证明安全是一种证明密码学方案安全性的形式化方法，它将密码学方案的安全性规约为公认的计算难题，并已成为现代密码学领域中理论工作的主线。本文主要研究密钥分配协议的可证明安全，这包括它们的各种形式化安全定义以及达到这些安全性定义的方案构造。并且研究这些模型在设计和分析现实中的一些密钥管理方案方面的具体应用。本文得到的主要结果如下：1.对当前主流的分析密钥分配协议的可证明安全的随机预言机模型方法进行分析总结，并讨论其在设计和证明密钥分配协议安全性方面的密码学用途。2.对中国无线局域网国家标准WAPI中用户身份鉴别和密钥管理方案进行分析，发现其存在的两个安全缺陷，改进后得到一个可证明安全的身份鉴别和密钥管理方案。=3.针对无线传感器网络存在的一系列安全问题，基于CK模型，形式化地提出一种快速、高效且适用于大规模传感器网络的密钥管理方案。4.填补SIP描述中缺乏具体安全机制的空白，提出一种基于挑战－应答的SIP安全机制，实现了消息的双向认证，并且利用可证明安全技术证明了方案的安全性，较其他同类方案具有密钥规模小、计算速度快等明显优势。