Annales Des Télécommunications

, Volume 62, Issue 11–12, pp 1365–1387 | Cite as

Automated verification of a key management architecture for hierarchical group protocols

  • Mohamed Salah Bouassida
  • Najah Chridi
  • Isabelle Chrisment
  • Olivier Festor
  • Laurent Vigneron


Emerging applications require secure group communications involving hierarchical architecture protocols. Designing such secure hierarchical protocols is not straightforward, and their verification becomes a major issue in order to avoid any possible security attack and vulnerability. Several attempts have been made to deal with formal verification of group protocols, but to our knowledge, none of them did address the security of hierarchical ones. In this paper, we present the specific challenges and security issues of hierarchical secure group communications, and the work we did for their verification. We show how the AtSe back-end of the avispa tool was used to verify one of these protocols.


Communication security Key management Hierarchical system Multicast Program proof Formal language 

Vérification Automatique des Protocoles de Gestion de Clé de Groupe Hiérarchiques


De nouvelles applications requièrent des communications de groupe, intégrant des protocoles hiérarchiques. La conception de ce genre de protocoles n’est pas aisée et leur vérification devient une véritable problématique pour éviter toute éventuelle attaque de sécurité. Plusieurs travaux de recherche se sont focalisés sur la vérification formelle des protocoles de groupe. Néanmoins, à notre connaissance, aucun d’eux n’a adressé les protocoles hiérarchiques. Ce papier présente les défis spécifiques et les problématiques de sécurité des communications de groupes hiérarchiques, ainsi que le travail effectué en vue de leur vérification. Nous montrons comment le back-end AtSe de l’outil de vérification des protocoles de sécurité avispa, a été utilisé pour valider l’un de ces protocoles.


Sécurité communication Gestion clé Système hiérarchisé Diffusion groupée Preuve programme Langage formel 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Armando A., Basin D., Boichut Y., Chevalier Y., Compagna L., Cuellar J., Hankes Drielsma P., Héam P.-C., Mantovani J., Mödersheim S., Von Oheimb D., Rusinowitch M., Santos Santiago J., Turuani M., Vigano L., Vigneron L., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In K. Etessami and S. Rajamani, editors, 17th International Conference on Computer Aided Verification, cav’2005, volume 3576 of Lecture Notes in Computer Science, pages 281–285, Edinburgh, Scotland, 2005. Springer.CrossRefGoogle Scholar
  2. [2]
    Armando A., Compagna L., SATMC: A SAT-based Model Checker for Security Protocols. In 9th European Conference on Logics in Artificial Intelligence (JELIA), volume 3229 of Lecture Notes in Computer Science, pages 730–733. Springer, 2004.Google Scholar
  3. [3]
    Apvrille L., Courtiat J.P., Lohr C., de Saqui-Sannes P.. Turtle: A Realtime UML Profile Supported by a Formal Validation Toolkit, IEEE Transactions on Software Engineering, 307):473–487, July 2004.Google Scholar
  4. [4]
    Asokan N., Ginzboorg P., Key Agreement in ad hoc Networks, Computer Communications, 2317): 1627–1637, 2000.Google Scholar
  5. [5]
    Ateniese G., Steiner M., Tsudik G.. New Multiparty Authentication Services and Key Agreement Protocols, IEEE Journal on Selected Areas in Communications, 184):628–639, 2000.Google Scholar
  6. [6]
    Basin D., Mödersheim S., Vigano L., OFMC: A Symbolic Model Checker for Security Protocols, International Journal of Information Security, 43): 181–208, 2005.Google Scholar
  7. [7]
    Boichut Y., Heam P.-C., Kouchnarenko O., Oehl E., Improvements on the Genet and Klay Technique to Automatically Verify Security Protocols. In Int. Workshop on Automated Verification of Infinite-State Systems (AVIS), joint to ETAPS’04, pages 1–11, Barcelona, Spain, 2004. The final version will be published in EN in Theoretical Computer Science, Elsevier.Google Scholar
  8. [8]
    Bouassida M. S., Chrisment I., Festor O., BALADE: Diffusion multicast sécurisée d’un flux multimédia multi-sources séquentielles dans un environnement ad hoc. In R. Castanet, editor, CFIP 2005, Hermès Lavoisier, pages 531–546, Bordeaux, France, Mars 2005.Google Scholar
  9. [9]
    Bouassida M. S., Chrisment I., Festor O., Diffusion multicast sécurisée dans un environnement ad-hoc (1 vers n séquentiel). Rapport de recherche 5310, INRIA, Septembre 2004.Google Scholar
  10. [10]
    Bresson E., Chevassut O., Essiari A., Pointcheval D., Mutual Authentication and Group Key Agreement for Low-power Mobile Devices. Journal of Computer Communications, 2717):1730–1737, July 2004. Special Issue on Security and Performance in Wireless and Mobile Networks. Elsevier Science.Google Scholar
  11. [11]
    Chevalier Y., Compagna L., Cuellar J., Drielsma P-H., Mantovani J., Mödersheim S., Vigneron L., A High Level Protocol Specification Language for Industrial Security-sensitive Protocols. In Workshop on Specification and Automated Processing of Security Requirements (saps), Linz, Austria. 2004.Google Scholar
  12. [12]
    Clark J. A., Jacob J. L., A Survey of Authentication Protocol Literature. Technical Report 1.0, 1997.Google Scholar
  13. [13]
    Delicata R., Schneider S., A Formal Approach for Reasoning about a Class of Diffie-Hellman Protocols. In 3d International Workshop on Formal Aspects in Security and Trust, pages 34–36, 2005.Google Scholar
  14. [14]
    Denker G., Millen J., Modeling Group Communication Protocols using Multiset Term Rewriting. Electr. Notes Theor. Comput. Sci., volume 71. 2002.Google Scholar
  15. [15]
    Diffie W., Hellman M.E., New Directions in Cryptography, IEEE Transactions on Information Theory, 226):644–654, 1976.MathSciNetMATHGoogle Scholar
  16. [16]
    Dondeti L., Mukherjee S., Samal A., Scalable Secure One-to-many Group Communication using Dual Encryption. In Computer Communicatin Journal, number 23, November 1999.Google Scholar
  17. [17]
    Hassan H., Bouabdallah A., Bettahar H., Challal Y., HI-KD: Hash-Based Hierarchical Key Distribution for Group Communication, IEEE Infocom Poster, 2005.Google Scholar
  18. [18]
    Ingemarson I., Tang D., Wong C., A Conference Key Distribution System. In IEEE transactions on information theory, 285), 1982, 714–720. September 1982.Google Scholar
  19. [19]
    Kim Y., Perrig A., Tsudik G., Simple and Fault-tolerant Key Agreement for Dynamic Collaborative Groups. In CCS ’00: Proceedings of the 7th ACM conference on Computer and communications security, pages 235–244, New York, NY, USA, 2000. ACM Press.CrossRefGoogle Scholar
  20. [20]
    Meadows C., Extending Formal Cryptographic Protocol Analysis Techniques for Group Protocols and Low-level Cryptographic Primitives. In P. Degano, editor, the First Workshop on Issues in the Theory of Security, pages 87–92, Geneva, Switzerland, July 2000.Google Scholar
  21. [21]
    Mittra S., Iolus: A Framework for Scalable Secure Multicasting. In sigcomm, pages 277–288, 1997.CrossRefGoogle Scholar
  22. [22]
    McGrew D., Sherman A., Key Establishement in Large Dynamic Groups using One-way Functions Trees, May 1998.Google Scholar
  23. [23]
    Meadows C., Syverson P., Formalizing GDOI Group Key Management Requirements in NPATRL. In CCS ’01: Proceedings of the 8th ACM conference on Computer and Communications Security, pages 235–244, New York, USA, 2001. ACM Press.CrossRefGoogle Scholar
  24. [24]
    Nam J., Kim S., Won D., Attacks on Bresson-Chevassut-Essiari-Pointcheval’s Group Key Agreement Scheme for Low-power Mobile Devices. Cryptology ePrint Archive, Report 2004/251, 2004.Google Scholar
  25. [25]
    Pereira O., Quisquater J.-J., Some Attacks upon Authenticated Group Key Agreement Protocols. Journal of Computer Security, 114):555–580, 2003.Google Scholar
  26. [26]
    Pereira O., Quisquater J.-J., Generic Insecurity of Cliques-type Authenticated Group Key Agreement Protocols. In CSFW, pages 16–19, 2004.Google Scholar
  27. [27]
    Steel G., Bundy A.. Attacking Group Multicast Key Management Protocols using coral. In A. Armando and L. Vigano, editors, Proceedings of the ARSPA Workshop, volume 125 of ENTCS, pages 125–144, 2004.Google Scholar
  28. [28]
    Steel G., Bundy A., Maidl M., Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures. In D. Basin and M. Rusinowitch, editors, Proceedings of the International Joint Conference on Automated Reasoning, volume 3097 of LNAI, pages 137–151, Cork, Ireland, July 2004. Springer.Google Scholar
  29. [29]
    Steiner M., Tsudik G., Waidner M.. Cliques: A New Approach to Group Key Agreement. In 18th International Conference on Distributed Computing Systems, pages 380–387. 1998. IEEE Computer Society Press.Google Scholar
  30. [30]
    Taghdiri M., Jackson D.. A Lightweight Formal Analysis of a Multicast Key Management Scheme. In 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), pages 240–256. 2003.CrossRefGoogle Scholar
  31. [31]
    Tsudik G., Rhee K., Park Y.. A Group Key Management Architecture for Mobile Ad Hoc Wireless Networks. Journal of Information Science and Enfineering, 21:415–428, 2005.Google Scholar
  32. [32]
    Tanaka S., Sato F., A Key Distribution and Rekeying Framework with Totally Ordered Multicast Protocols. In 15th International Conference on Information Networking, page 831. 2001.CrossRefGoogle Scholar
  33. [33]
    Turuani M., The CL-Atse Protocol Analyser. In F. Pfenning, editor, 17th International Conference on Term Rewriting and Applications (RTA), volume 4098 of Lecture notes in Computer Science, pages 277–286. Springer, August 2006.Google Scholar
  34. [34]
    Wong C., Gouda M., Lam S., Secure Group Communications using Key Graphs. In ACM SIGCOMM, pages 68–79, 1998.Google Scholar

Copyright information

© Institut Telecom / Springer-Verlag France 2007

Authors and Affiliations

  • Mohamed Salah Bouassida
    • 1
  • Najah Chridi
    • 1
  • Isabelle Chrisment
    • 1
  • Olivier Festor
    • 1
  • Laurent Vigneron
    • 1
  1. 1.Campus scientifiqueLORIAVandoeuvre-lès-Nancy CedexFrance

Personalised recommendations