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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2001
Accession Number
ADA465153

Entities

People

  • Catherine Meadows
  • Iliano Cervesato
  • Paul Syverson

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Analyzers
  • Authentication
  • Computer Access Control
  • Cryptography
  • Denial Of Service Attack
  • Explosives Initiators
  • Guarantees
  • Hierarchies
  • Information Operations
  • Language
  • Learning
  • Materials
  • Security
  • Security Protocols
  • Specifications
  • Standards

Fields of Study

  • Computer science

Readers

  • Computer Networking
  • Organic Chemistry
  • Software Engineering.