Accession Number:

ADA465466

Title:

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

Descriptive Note:

Corporate Author:

NAVAL RESEARCH LAB WASHINGTON DC

Personal Author(s):

Report Date:

1999-01-01

Pagination or Media Count:

17.0

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.

Subject Categories:

  • Computer Systems Management and Standards
  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE