Author(s)

Amjad Gawanmeh, Sofiène Tahar, Leila Jemni Ben Ayed

Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada.
Department of Electrical and Computer Engineering, Khalifa University of Science, Technology and Research, Sharjah, UAE.
Ecole Nationale des Sciences de l’Informatique, University of la Manouba, Tunis, Tunisia.

Group key security protocols play an important role in today’s communication systems. Their verification, however, remains a great challenge because of the dynamic characteristics of group key construction and distribution protocols. Security properties that are well defined in normal two-party protocols have different meanings and different interpretations in group key distribution protocols, specifically, secrecy properties, such as group secrecy, forward secrecy, backward secrecy, and key independence. In this paper, we present a method to verify forward secrecy properties for group-oriented protocols. The method is based on a correct semantical link between group key protocols and event-B models and also uses the refinement process in the B method to model and verify group and forward secrecy. We use an event-B first-order theorem proving system to provide invariant checking for these secrecy properties. We illustrate our approach on the Tree based Group Diffie-Hellman protocol as case study.

Group Key Protocols; Formal Verification; Forward Secrecy; Secrecy; Event-B

A. Gawanmeh, S. Tahar and L. Ayed, "Formal Verification of Secrecy in Group Key Protocols Using Event-B," International Journal of Communications, Network and System Sciences, Vol. 5 No. 3, 2012, pp. 165-177. doi: 10.4236/ijcns.2012.53021.