A Formal Language for Cryptographic Protocol Requirements

Abstract

In this paper we present a formal language for specifying and reasoning about cryptographic protocol requirements. We give sets of requirements for key distribution protocols and for key agreement protocols in that language. We look at a key agreement protocol due to Aziz and Diffe that might meet those requirements and show how to specify it in the language of the NRL Protocol Analyzer. We also show how to map our formal requirements to the language of the NRL Protocol Analyzer and use the Analyzer to show that the protocol meets those requirements. In other words, we use the Analyzer to assess the validity of the formulae that make up the requirements in models of the protocol. Our analysis reveals an implicit assumption about implementations of the protocol and reveals subtleties in the kinds of requirements one might specify for similar protocols.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1996
Accession Number
ADA465327

Entities

People

  • Catherine Meadows
  • Paul Syverson

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Agreements
  • Algorithms
  • Analyzers
  • Asymetric Encryption
  • Computations
  • Cryptography
  • Denial Of Service Attack
  • Digital Communications
  • Environment
  • Explosives Initiators
  • Formal Languages
  • Information Operations
  • Language
  • Mobile Phones
  • Notation
  • Secure Communications
  • Security Protocols

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Cybersecurity.
  • Software Engineering.