A Logical Language for Specifying Cryptographic Protocol Requirements

Abstract

In this paper we present a formal language for specifying and reasoning about cryptographic protocol requirements. We give examples of simple sets of requirements in that language. We look at two versions of a protocol that might meet those requirements and show how to specify them in the language of the NRL Protocol Analyzer. [Mea91] [Mea92] We also show how to map one of our sets of formal requirements to the language of the NRL Protocol Analyzer and use the Analyzer to show that one version of the protocol meets those requirements. In other words, we use the Analyzer as a model checker to assess the validity of the formulae that make up the requirements.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1993
Accession Number
ADA463014

Entities

People

  • Catherine Meadows
  • Paul Syverson

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Materials and Manufacturing Processes
  • Sensors

DTIC Thesaurus Topics

  • Abstracts
  • Analyzers
  • Asymetric Encryption
  • Authentication
  • Computers
  • Cryptography
  • Formal Languages
  • Guarantees
  • Information Operations
  • Language
  • Military Research
  • Security
  • Security Protocols
  • Sequences
  • Transitions

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computer Engineering
  • Software Engineering.