通信学报2011，Vol.32Issue(10)：118-126,9.
计算可靠的Diffie-Hellman密钥交换协议自动证明
Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols
摘要
Abstract
A computationally observational equivalence model for the Diffe-Hellman key agreement primitive was proposed and the soundness of the model was proved. Compared with prior works, this model can extend the power of the mechanized prover Crypto Verif directly. When applying the model to proving the public-key Kerberos, the deficiency of the adversary's capability was uncovered and an enhanced model for the adversary was presented. The model was validated by verifying the public-key Kerberos in Diffie-Hellman mode with Crypto Verif automatically. Being different from current approaches, the verification procedure is both automatic and computationally sound.关键词
密码协议/Diffie-Hellman原语/Kerberos协议/自动化证明Key words
security protocols/ Diffie-Hellman primitives/ Kerberos protocol/ mechanized proofs分类
信息技术与安全科学引用本文复制引用
冯超,张权,唐朝京..计算可靠的Diffie-Hellman密钥交换协议自动证明[J].通信学报,2011,32(10):118-126,9.基金项目
国家自然科学基金资助项目(60872052) （60872052）
