基于攻击者行为能力的SVO协议分析

SVO原逻辑不适用于证明基于证书的认证与密钥交换协议安全性问题。为此，提出2个SVO逻辑相关公理，对证书真实性与会话密钥安全性进行判断及验证，并结合Dolev-Yao安全模型，从攻击者行为能力的角度评估密码协议的安全性。经分析证明Mangipudi协议未能提供前向安全且存在假冒攻击的安全缺陷，因此给出一个在Dolev-Yao安全模型下可证明安全的解决方案。

Analysis of SVO Protocol Based on Attacker Behavior Capability

According to the fact that SVO logic lacks relative axioms of judging and verifying the validity of certificates and the security proof of authenticaled exchange protocols, this paper advices to estimate the protocols security from the aspect of ability of attackers by combining Dolev-Yao threat model with the extension of SVO logic which proves that Mangipudi protocol is not immune from impersonation attack and has no the security property of forward secrecy. Then a provable security scheme which overcomes all above flaws in the Dolev-Yao threat model is orooosed.