A Lightweight Formal Analysis of a Multicast Key Management Scheme

  • Mana Taghdiri
  • Daniel Jackson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


This paper describes the analysis of Pull-Based Asynchronous Rekeying Framework (ARF), a recently proposed solution to the scalable group key management problem in secure multicast. A model of this protocol is constructed in Alloy, a lightweight relational modeling language, and analyzed using the Alloy Analyzer, a fully automatic simulation and checking tool for Alloy models. In this analysis, some critical correctness properties that should be satisfied by any secure multicast protocol are checked. Some flaws, previously unknown to the protocol’s designers are exposed, including one serious security breach. To eliminate the most serious flaw, some fixes are proposed and checked using the Alloy Analyzer. The case study also illustrates a novel modeling idiom that supports better modularity and is generally simpler and more intuitive than the conventional idiom used for modeling distributed systems.


Lightweight modeling formal specification Alloy secure multicast key management asynchronous rekeying 


  1. 1.
    Baugher, M., Hardjono, T., Harney, H., Weis, B.: Group domain of interpretation for ISAKMP (2001),
  2. 2.
    Clarke, E.M., Marrero, W.: Using formal methods for analyzing security. Information Survivability Workshop (ISW) (October 1998) Google Scholar
  3. 3.
    Guttag, J., Horning, J., Modet, A.: Report on the Larch Shared Language: Version 2.3. Digital Equipment Corporation, Systems Research Center, report 58 (1990) Google Scholar
  4. 4.
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5) (1997)Google Scholar
  5. 5.
    Jackson, D.: Automating first-order relational logic. In: Proc. of the 8th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2000) Google Scholar
  6. 6.
    Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: Proc. of the joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2001)Google Scholar
  7. 7.
    Jackson, D., Wing, J.: Lightweight formal methods. IEEE Computer (1996)Google Scholar
  8. 8.
    Jones, C.B.: Systematic Software Development using VDM. Prentice Hall International, Englewood Cliffs (1990)zbMATHGoogle Scholar
  9. 9.
    Meadows, C.: A system for the specification and analysis of key management protocols. In: Proc. of 1991 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 182–195 (1991)Google Scholar
  10. 10.
    Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)CrossRefzbMATHGoogle Scholar
  11. 11.
    Meadows, C., Syverson, P., Cervesato, I.: Formalizing GDOI group key management requirements in NPATRL. In: Proc. of the 8th ACM Conference on Computer and Communications Security, pp. 235–244 (2001)Google Scholar
  12. 12.
    Mittra, S.: Iolus: A framework for scalable secure multicasting. In: Proc. of ACM SIGCOMM 1997, pp. 277–288 (1997)Google Scholar
  13. 13.
    Sato, F., Tanaka, S.: A push-based key distribution and rekeying protocol for secure multicasting. In: Proc. of International Conference on Parallel and Distributed Systems, pp. 214–219 (2001)Google Scholar
  14. 14.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)zbMATHGoogle Scholar
  15. 15.
    Taghdiri, M.: Lightweight modelling and automatic analysis of multicast key management schemes. Master’s thesis, MIT, EECS Department (December 2002) Google Scholar
  16. 16.
    Tanaka, S., Sato, F.: A key distribution and rekeying framework with totally ordered multicast protocols. In: Proc. of the 15th International Conf. on Information Networking, pp. 831–838 (2001)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Mana Taghdiri
    • 1
  • Daniel Jackson
    • 1
  1. 1.MIT Laboratory for Computer ScienceUSA

Personalised recommendations