Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer

Abstract

In this paper we show how the NRL Protocol Analyzer, a special-purpose formal methods tool designed for the verification of cryptographic protocols, was used in the analysis of the Internet Key Exchange (IKE) protocol. We describe some of the challenges we faced in analyzing IKE, which specifies a set of closely related subprotocols, and we show how this led to a number of improvements to the Analyzer. We also describe the results of our analysis, which uncovered several ambiguities and omissions in the specification which would have made possible attacks on some implementations that conformed to the letter, if not necessarily the intentions, of the specifications.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1999
Accession Number
ADA465466

Entities

People

  • Catherine Meadows

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Cyber

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Analyzers
  • Computer Communications
  • Computer Networks
  • Cryptography
  • Denial Of Service Attack
  • Formal Languages
  • Information Operations
  • Internet
  • Language
  • Materials
  • Network Protocols
  • Networks
  • Secure Communications
  • Security Protocols
  • Standards

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Computer Networking
  • Systems Analysis and Design