Formalizing GDOI group key management requirements in NPATRL

ABSTRACT

Although there is a substantial amount of work on formal requirements for two and three-party key distribution protocols, very little has been done on requirements for group protocols. However, since the latter have security requirements that can differ in important but subtle ways, we believe that a rigorous expression of these requirements can be useful in determining whether a given protocol can satisfy an application's needs. In this paper we make a first step in providing a formal understanding of security requirements for group key distribution by using the NPATRL language, a temporal requirement specification language for use with the NRL Protocol Analyzer. We specify the requirements for GDOI, a protocol being proposed as an IETF standard, which we are formally specifying and verifying in cooperation with the MSec working group.

REFERENCES

• 1: M.Baugher,T.Hardjono,H.Harney,and B.Weis. Group domain of interpretation for ISAKMP. available at http://search.ietf.org/internet-drafts/ draft-irtf-smug-gdoi-01.txt ,January 2001.
• 2: R.Canetti,J.Garay,G.Itkis,D.Micciancio, M.Naor,and B.Pinkas.Multicast security:A taxonomy and some e .cient constructions.In Proc.of INFOCOM '99,vol.2 ,pages 708 -716,March 1999.
• 3: Brian F.Chellas.Modal Logic:An Introduction . Cam ridge University Press,1980.
• 4: Danny Dolev and Andrew C.Yao.On the security of public-key protocols.IEEE Transactions on Information Theory ,2(29):198 -208,March 1983. Preliminary version in Proc.22nd Annual IEEE Symp. Foundations of Computer Science,1981,350 -357.
• 5: Naganand Doraswamy , Dan Harkins, IPSec: The New Security Standard for the Internet, Intranets, and Virtual Private Networks, Prentice Hall PTR, Upper Saddle River, NJ, 1999
• 6: Robert Goldblatt, Logics of time and computation, Center for the Study of Language and Information, Stanford, CA, 1987
• 7: D.Harkins and D.Carrel.The Internet Key Exchange (IKE).RFC 2409,IETF,Novem er 1998.available at ftp://ftp.isi.edu/in-notes/rfc2409.txt .
• 8: G.E.Hughes and M.J.Creswell.A New Introduction to Modal Logic .Routledge,1996.
• 9: Catherine Meadows , Paul F. Syverson, A Formal Specification of Requirements for Payment Transactions in the SET Protocol, Proceedings of the Second International Conference on Financial Cryptography, p.122-140, February 23-25, 1998
• 10: Catherine Meadows.A model of computation for the NRL Protocol Analyzer.In Proceedings of the 7th Computer Security Foundations Workshop ,pages 84 -89.IEEE CS Press,June 1994.
• 11: Catherine Meadows.The NRL Protocol Analyzer:An overview.Journal of Logic Programming , 26(2):113 -131,February 1996.
• 12: Catherine Meadows, A cost-based framework for analysis of denial of service in networks, Journal of Computer Security, v.9 n.1-2, p.143-164, Jan. 1,2001
• 13: Michael Steiner , Gene Tsudik , Michael Waidner, Key Agreement in Dynamic Peer Groups, IEEE Transactions on Parallel and Distributed Systems, v.11 n.8, p.769-780, August 2000 [doi>10.1109/71.877936]
• 14: Paul Syverson , Cathernine Meadows, A Logical Language for Specifying Cryptographic Protocol Requirements, Proceedings of the 1993 IEEE Symposium on Security and Privacy, p.165, May 24-26, 1993
• 15: P.Syverson and C.Meadows.Formal requirements for key distribution protocols.In A.De Santis,editor, Advances in Cryptology -EUROCRYPT '94 ,pages 32 -331.Springer-Verlag,LNCS 950,1994.
• 16: Paul Syverson , Catherine Meadows, A Formal Language for Cryptographic Protocol Requirements, Designs, Codes and Cryptography, v.7 n.1-2, p.27-59, Jan. 1996 [doi>10.1007/BF00125075]

INDEX TERMS

Primary Classification:
  E. Data
  E.3 DATA ENCRYPTION
      Subjects: Public key cryptosystems

Additional Classification:
  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Electronic data interchange (EDI)
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Authentication

General Terms:
Algorithms, Performance, Security