设计和分析双方密钥交换协议,目前已提出多个可证安全模型。为保障密钥交换协议所需的安全特性,形成一个统一的安全模型是非常必要的。本文评估了eCK′,eCK和CK模型,证明了eCK′模型是当前最强的密钥交换可证安全模型,并形式化分析了这些模型的强弱关系。此外,对于模型间存在的蕴含关系还提供了形式化证明,并对非蕴含关系给出了反例。 Designing and analyzing the key exchange protocol between the two parties, so far, several verifiable security models have been proposed. In order to protect the security features required by the key exchange protocol, it is necessary to form a unified security model. This paper evaluates the eCK ’, eCK and CK models and proves that the eCK’ model is the strongest current key exchange verifiable security model and formally analyzes the strength and weakness of these models. In addition, formal proofs are provided for implicated relationships among models and counter-examples for implied relationships.