Formal verification in Joux tripartite Drffie-Hellman protocol

Security analysis of cryptographic protocols has been widely studied for many years. As 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 cryptography. Recently, Canetti and Herzog have proposed Universally Compos able Symbolic Analysis (UCSA) of two-party mutual authentication and key exchange protocol which is based on the symmetric encryption schemes. This scheme can analyze the protocols automatically and guarantee the soundness of cryptography. Therefore, we discuss group key exchange protocol which is based on Joux Tripartite Diffie-Hellman (JTDH) using UCSA Our contribution is analyzing group key exchange protocol effectively without damaging the soundness of cryptography.