Computationally sound and effective symbolic analysis of group key exchange protocols

Zi Jian Zhang, Lie Huang Zhu*, Feng Wang, Le Jian Liao

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)664-672
Number of pages9
JournalJisuanji Xuebao/Chinese Journal of Computers
Volume35
Issue number4
DOIs
Publication statusPublished - Apr 2012

Keywords

  • Computationally sound
  • Effective
  • Group key exchange
  • Symbolic analysis
  • Universally composable

Fingerprint

Dive into the research topics of 'Computationally sound and effective symbolic analysis of group key exchange protocols'. Together they form a unique fingerprint.

Cite this