Login | Register

Formal Verification of Secrecy in Group Key Protocols Using Event-B

Title:

Formal Verification of Secrecy in Group Key Protocols Using Event-B

Gawanmeh, Amjad, Tahar, Sofiène and Ben Ayed, Leila Jemni (2012) Formal Verification of Secrecy in Group Key Protocols Using Event-B. Int'l J. of Communications, Network and System Sciences, 05 (03). pp. 165-177. ISSN 1913-3715

[thumbnail of IJCNS-2012.pdf]
Preview
Text (application/pdf)
IJCNS-2012.pdf - Accepted Version
260kB

Official URL: http://dx.doi.org/10.4236/ijcns.2012.53021

Abstract

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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Gawanmeh, Amjad and Tahar, Sofiène and Ben Ayed, Leila Jemni
Journal or Publication:Int'l J. of Communications, Network and System Sciences
Date:2012
Digital Object Identifier (DOI):10.4236/ijcns.2012.53021
Keywords:Group Key Protocols; Formal Verification; Forward Secrecy; Secrecy; Event-B
ID Code:977360
Deposited By: Danielle Dennie
Deposited On:14 Jun 2013 13:23
Last Modified:18 Jan 2018 17:44

References:

[1] Y. Kim, A. Perrig and G. Tsudik, “Tree-Based Group Key Agreement,” ACM Transactions on Information and Systems Security, Vol. 7, No. 1, 2004, pp. 60-96. doi:10.1145/984334.984337
[2] J. Abrial, “Modelling in Event-B: System and Software Engineering,” Cambridge University Press, Cambridge, 2009.
[3] J. Abrial, “The B-Book: Assigning Programs to Meanings,” Cambbridge University Press, Cambridge, 1996. doi:10.1017/CBO9780511624162
[4] C. Metayer, J. Abrial and L. Voisin, “RODIN Deliverable 3.2: Event-B Language,” Technical Report Project IST-511599, School of Computing Science, University of Newcastle, Newcastle, 2005.
[5] A. Gawanmeh, L. J. B. Ayed and S. Tahar, “Event-B Based Invariant Checking of Secrecy in Group Key Protocols,” Local Computer Networks, IEEE Computer Society Press, New York, 2008, pp. 950-957.
[6] M. Steiner, G. Tsudik and M. Waidner, “Diffie-Hellman Key Distribution Extended to Group Communication,” Conference on Computer and Communications Security, ACM Press, London, 1996, pp. 31-37.
[7] J. Abrial, M. Butler, S. Hallerstede and L. Voisin, “An Open Extensible Tool Environment for Event-B,” International Conference on Formal Methods and Software Engineering, Lecture Notes in Computer Science, Springer-Verlag, Berlin, Vol. 4789, 2006, pp. 588-605.
[8] “Rodin Platform,” 2011. http://www.event-b.org
[9] F. F′abrega, “Strand Spaces: Proving Security Protocols Correct,” IOS Journal of Computer Security, Vol. 7, No. 2-3, 1999, pp. 191-230.
[10] L. Paulson, “The Inductive Approach to Verifying Cryptographic Protocols,” IOS Journal of Computer Security, Vol. 6, No. 1-2, 1998, pp. 85-128.
[11] F. Crazzolara and G. Winskel, “Events in Security Protocols,” ACM Conference on Computer and Communications Security, ACM Press, London, 2001 pp. 96-105.
[12] C. Cremers and S. Mauw, “Operational Semantics of Security Protocols,” Scenarios: Models, Transformations and Tools, LNCS, Springer-Verlag, Berlin, Vol. 3466, 2005, pp. 66-89. doi:10.1007/11495628_4
[13] A. Gawanmeh, A. Bouhoula and S. Tahar, “Rank Functions Based Inference System for Group Key Management Protocols Verification,” International Journal of Network Security, Vol. 8, No. 2, 2009, pp. 207-218.
[14] N. Stouls and M. Potet, “Security Policy Enforcement through Refinement Process,” Formal Specification and Development in B, LNCS, Springer-Verlag, Berlin, Vol. 4355, 2007, pp. 216-231. doi:10.1007/11955757_18
[15] N. Benaissa, D. Cansell and D. Mery, “Integration of Security Policy into System Modeling,” Formal Specification and Development in B, LNCS, Springer-Verlag, Berlin, Vol. 4355, 2007, pp. 232-247. doi:10.1007/11955757_19
[16] A. Abou El Kalam, R. E. Baida, P. Balbiani, S. Benferhat, F. Cuppens, Y. Deswarte, A. Miege, C. Saurel and G. Trouessin, “Organization Based Access Control,” International Workshop on Policies for Distributed Systems and Networks, IEEE Computer Society Press, New York, 2003, pp. 120-131.
[17] D. Bert, M. Potet and N. Stouls, “GeneSyst: A Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties,” Formal Specification and Development in Z and B, LNCS, Springer-Verlag, Berlin, Vol. 3455, 2005, pp. 299-318. doi:10.1007/11415787_18
[18] M. Butler, “On the Use of Data Refinement in the Development of Secure Communications Systems,” Formal Aspects of Computing, Vol. 14, No. 1, 2002, pp. 2-34. doi:10.1007/s001650200025
[19] N. Chridi, M. Turuani and M. Rusinowitch, “Decidable analysis for a Class of Cryptographic Group Protocols with Unbounded Lists,” Computer Security Foundations Symposium, IEEE Computer Society Press, New York, 2009, pp. 277-289.
[20] N. Dalal, J. Shah, K. Hisaria and D. Jinwala, “A Comparative Analysis of Tools for Verification of Security Protocols,” International Journal of Communications, Network and System Sciences, Vol. 3, No. 10, 2010, pp. 779-787. doi:10.4236/ijcns.2010.310104
[21] Y. Li and J. Pang, “Extending the Strand Space Method with Timestamps: Part I the Theory,” International Journal of Communications, Network and System Sciences, Vol. 1, No. 2, 2010, pp. 45-55.
[22] J. Abrial, “Extending B without Changing It (for Developing Distributed Systems),” 1st Conference on the B method, Putting into Practice Methods and Tools for Information System Design, Institut de Recherche en Informatique de Nantes, 1996, pp. 169-190.
[23] T. Hoang and J. Abrial, “Reasoning about Liveness Properties in Event-B,” International Conference on Formal Engineering Methods, Lecture Notes in Computer Science, Springer-Verlag, Berlin, Vol. 6991, 2011, pp. 456-471.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top