计算可靠的Diffie-Hellman密钥交换协议自动证明  

Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols

作　　者：冯超[1] 张权[1] 唐朝京[1] 

机构地区：[1]国防科技大学电子科学与工程学院,湖南长沙410073

出　　处：《通信学报》2011年第10期118-126,共9页Journal on Communications

基　　金：国家自然科学基金资助项目(60872052)~~

摘　　要：针对Diffie-Hellman密钥交换协议,提出了采用观测等价关系的建模方法,证明了该方法的可靠性,并利用该方法扩展了自动工具CryptoVerif的验证能力。发现了对公钥Kerberos协议自动证明中敌手能力模型的缺陷,并提出了修正方法。利用扩展的CryptoVerif自动证明了基于Diffie-Hellman的Kerberos协议的安全性,验证了该扩展方法的有效性。与现有大部分证明方法不同的是,该证明方法既保留了自动证明工具的易用性,又保证了计算模型下的强可靠性。A computationally observational equivalence model for the Diffe-Hellman key agreement primitive was pro-posed and the soundness of the model was proved.Compared with prior works,this model can extend the power of the mechanized prover CryptoVerif 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 vali-dated by verifying the public-key Kerberos in Diffie-Hellman mode with CryptoVerif automatically.Being different from current approaches,the verification procedure is both automatic and computationally sound.

关 键 词：密码协议 Diffie-Hellman原语 KERBEROS协议 自动化证明 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]