TY - JOUR
T1 - Computationally sound and effective symbolic analysis of group key exchange protocols
AU - Zhang, Zi Jian
AU - Zhu, Lie Huang
AU - Wang, Feng
AU - Liao, Le Jian
PY - 2012/4
Y1 - 2012/4
N2 - The computational soundness of symbolic analysis is always argued, because the cryptographic primitives are viewed as black boxes, and the specific security properties of those cryptographic primitives have not been considered yet. Moreover, this kind of approaches is ineffective, when it is used to analyze group key exchange protocols with a large number of participants. This paper considers those problems above, and proposes computationally sound and effective symbolic analysis of group key exchange protocols. More specifically, we design a pattern function for symbolic expression, so as to define the concrete security properties that modular exponentiation operation needs satisfy. Based on that, we prove the symbolic analysis of Burmester-Desmedt protocol is computationally sound in universally composable security framework. Furthermore, we use mathematical inductive method to prove the security of Burmester-Desmedt protocol is unrelated to the number of participants. The number of the participants does not affect symbolic analysis. As a result, the efficiency of symbolic analysis is improved.
AB - The computational soundness of symbolic analysis is always argued, because the cryptographic primitives are viewed as black boxes, and the specific security properties of those cryptographic primitives have not been considered yet. Moreover, this kind of approaches is ineffective, when it is used to analyze group key exchange protocols with a large number of participants. This paper considers those problems above, and proposes computationally sound and effective symbolic analysis of group key exchange protocols. More specifically, we design a pattern function for symbolic expression, so as to define the concrete security properties that modular exponentiation operation needs satisfy. Based on that, we prove the symbolic analysis of Burmester-Desmedt protocol is computationally sound in universally composable security framework. Furthermore, we use mathematical inductive method to prove the security of Burmester-Desmedt protocol is unrelated to the number of participants. The number of the participants does not affect symbolic analysis. As a result, the efficiency of symbolic analysis is improved.
KW - Computationally sound
KW - Effective
KW - Group key exchange
KW - Symbolic analysis
KW - Universally composable
UR - http://www.scopus.com/inward/record.url?scp=84862019799&partnerID=8YFLogxK
U2 - 10.3724/SP.J.1016.2012.00664
DO - 10.3724/SP.J.1016.2012.00664
M3 - Article
AN - SCOPUS:84862019799
SN - 0254-4164
VL - 35
SP - 664
EP - 672
JO - Jisuanji Xuebao/Chinese Journal of Computers
JF - Jisuanji Xuebao/Chinese Journal of Computers
IS - 4
ER -