Formal Verification in 3oux Tripartite Diffie-Hellman Protocol

作     者：祝烈煌 张子剑 王峰 郭聪 袁彩霞 

作者机构：Beijing Laboratory of Intelligent Information TechnologySchool of Computer ScienceBeijing Institute of Technology Naval Academy of Armament Beijing University of Posts and Telecommunications 

出 版 物：《China Communications》 (中国通信（英文版）)

年 卷 期：2012年第9卷第3期

页      面：153-163页

核心收录：

学科分类：0810[工学-信息与通信工程] 0839[工学-网络空间安全] 08[工学] 081001[工学-通信与信息系统] 

基　　金：supported by the National Natural Science Foundation of China under Grants No.61003262,No.60873237,No.61100205,No.60873001 the Fundamental Research Funds for the Central Universities under Grant No.2009RC0212 

主　　题：UCSA computationally sound JTDH group key exchange protocol 

摘      要：Security analysis of cryptographic protocols has been widely studied for many *** far as we know,we have not found any methods to effectively analyze group key exchange protocols for the three parties yet,which did not sacrifice the soundness of ***,Canetti and Herzog have proposed Universally Composable Symbolic Analysis(UCSA) of two-party mutual authentication and key exchange protocol which is based on the symmetric encryption *** scheme can analyze the protocols automatically and guarantee the soundness of ***,we discuss group key exchange protocol which is based on Joux Tripartite Diffie-Hellman(JTDH) using *** contribution is analyzing group key exchange protocol effectively without damaging the soundness of cryptography.