Formal verification of secure group communication protocols modelled in UML

1. Armando A, Basin D, Boichut Y, Chevalier Y, Compagna L, Cuellar J, Hankes Drielsma P, Héam PC, Kouchnarenko O, Mantovani J, Mödersheim S, Von Oheimb D, Rusinowitch M, Santos Santiago J, Vigano L, Turuani M, Vigneron L (2005) The AVISPA tool for the automated validation of internet security protocols and applications. In: Proceedings of 17th international conference on computer aided verification (CAV’05). Springer-Verlag (LNCS 3576). Edinburgh, Scotland, pp. 281–285

2. Apvrille L, Courtiat J-P, Lohr C, de Saqui-Sannes P (2004) TURTLE: a real-time UML profile supported by a formal validation toolkit. IEEE Trans Softw Eng 30(7): 473–487

   Article  Google Scholar 

3. Dolev D, Yao AC (1983) On the security of public-key protocols. IEEE Trans Inform Theory 29(2): 198–208

   Article  MATH  MathSciNet  Google Scholar 

4. Mota S (2008) Protocol modeling and verification for secured group communications. PhD thesis, University of Toulouse (in French)

5. Bouassida MS, Chrisment I, Festor O (2008) Group key management in MANETs. Int J Netw Secur IJNS 6(1): 67–79

   Google Scholar 

6. Steiner M, Tsudik G, Waidner M (1998) CLIQUES: a new approach to group key agreement. In: Proceedings of the 18th IEEE international conference on distributed computing system, Amsterdam, pp 380–387

7. Meadows C (2000) Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives. In: Proceedings of the first workshop on issues in the theory of security. Degano P, Geneva, Switzerland, pp 87–92

8. Taghdir M, Jackson D (2003) A lightweight formal analysis of a multicast key management scheme. In: Proceedings of 23rd IFIP international conference on formal techniques for networked and distributed systems, FORTE’03, pp 240–256

9. Steel G, Bundy A, Maidl M (2004) Attacking a protocol for group key agreement by refuting incorrect inductive conjectures. In: Proceedings of the international joint conference on automated reasoning. Springer-Verlag (LNAI 3097), pp 137–151

10. Tanaka S, Sato F (2001) A key distribution and rekeying framework with totally ordered multicast protocols. In: Proceedings of 15th IEEE international conference on information networking, ICOIN’01, pp 831–838

11. Steel G, Bundy A (2004) Attacking group multicast key management protocols using CORAL. In: Proceedings of the ARSPA workshop. ENTCS, vol. 125, no 1, pp 125–144

12. Mittra S (1997) Iolus: a framework for scalable secure multicasting. In: Proceedings of ACM, SIGCOMM’97, pp 277–288

13. Meadows C, Syverson P (2001) Formalizing GDOI group key management requirements in NPATRL. In: Proceedings of the 8th ACM conference on computer and communications security, pp 235– 244

14. Corin R, Etalle S, Hartel PH, Mader A (2004) ADER, timed analysis of Security Protocols. In: Proceedings of ACM workshop on formal methods in security engineering, Washington DC, USA, pp 26–32

15. Chick T, Teo JCM (2006) Energy-efficient ID-based group key agreement protocols for wireless networks. In: Proceedings of 20th parallel and distributed processing symposium

16. Wu B, Wu J, Fernandez B, Ilyas M, Magliveras S (2007) Secure and efficient key management in mobile ad hoc networks. J Netw Comput Appl 30(3): 937–954

    Article  Google Scholar 

17. Bohio M, Miri A (2004) Authenticated secure communications in mobile ad hoc networks. Proc IEEE Conf Electr Comput Eng 3: 1689–1692

    Google Scholar 

18. Birman KP, Hayden M, Ozkazap O, Xiao Z, Bidiu M, Minsky Y (1999) Bimodal multicast. ACM Trans Comput Syst 17(2): 41–88

    Article  Google Scholar 

19. Birman KP, Hayden M, Hickey J, Kreitz C, van Renesse R, Rodeh O, Vogels W (2000) The Horus and Ensemble projects: accomplishments and limitations. In: Information survivability conference and exposition DISCEX ’00, vol 1, pp 149–161

20. Whetten B, Kaplan S, Montgomery T (1994) A high performance totally ordered multicast protocol. In: Proceedings of the workshop on theory and practice in distributed systems

21. Amir Y, Dolev D, Kramer S, Malki D (1992) Transis: a communication sub-system for high availability. In: Proceedings of 22nd annual international symposium on fault tolerant computing, pp 76–84

22. Amir Y, Moser LE, Melliar-Smith PM, Agarwal DA, Ciarfella P (1995) The totem single-ring ordering and membership protocol. ACM Trans Comput Syst 13(4): 311–342

    Article  Google Scholar 

23. van Renesse R, Birman KP, Maffeis S (1996) HORUS: a flexible group communication system. Commun ACM 39(4): 76–83

    Article  Google Scholar 

24. Gong L (1997) Enclaves: enabling secure collaboration over the internet. IEEE Trans Selected Areas Commun 15(3): 567–575

    Article  Google Scholar 

25. Hiltunen MA, Schlichting RD (1996) Adaptative distributed and fault-tolerant systems. Comput Syst Sci Eng 11(5): 125–133

    Google Scholar 

26. Irrer J, Prakash A, McDaniel P (2003) Antigone: policy-based secure group communication system and AMirD: antigone-based secure file mirroring system. In: Proceedings of the DARPA information survivability conference and exposition DISCEX, pp 44–46

27. Almeida C (2004) Handling QoS in a dynamic real-time environment. In: Proceedings of the 8th IEEE international workshop on object-oriented real-time dependable systems, pp 217–224

28. Gutierrez-Nolasco S, Stehr M, Talcott C, Venkata N (2004) Exploring adaptability of secure group communication using formal prototyping techniques. In: Proceedings of 3rd workshop on adaptative and reflective middleware, Toronto, Canada

29. Jürjens J, Schreck J, Bartmann P (2008) Model-based security analysis for mobile communications. In: 30th international conference on software engineering (ICSE’08), Leipzig, Germany

30. Morimoto S, Cheng J (2005) Pattern protection profiles by UML for security specifications. In: International conference on computational intelligence for modelling control and automation (CIMCA-IAWTIC’05), Vienna, Austria

31. Abie H, Aredo DB, Kristoffersen T, Mazaber S, Raguin T (2005) Integrating a Security requirement Language with UML. In: 7th international conference on the unified modeling language (UML 2004), Lisbon, Portugal, LNCCS, vol 3273, pp 350–364

32. Woodside M et al (2009) Performance analysis of security aspects by weaving scenarios extracted from UML models. J Syst Softw 82(1): 56–74

    Article  Google Scholar 

Download references