Language Generation and Verification in the NRL Protocol Analyzer

Abstract

The NRL Protocol Analyzer is a tool for proving security properties of cryptographic protocols, and for finding flaws if they exist. It is used by having the user first prove a number of lemmas stating that infinite classes of states are unreachable, and then performing an exhaustive search on the remaining state space. One main source of difficulty in using the tool is in generating the lemmas that are to be proved. In this paper we show how we have made the task easier by automating the generation of lemmas involving the use of formal languages.

Open PDF

Document Details

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

Entities

People

  • Catherine Meadows

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Algorithms
  • Analyzers
  • Cryptography
  • Databases
  • Demographic Cohorts
  • Formal Languages
  • Generators
  • Guarantees
  • Identities
  • Information Operations
  • Language
  • Military Research
  • Notation
  • Optimization
  • Security Protocols
  • Transitions

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Cybersecurity.
  • Educational Psychology
  • Graph Algorithms and Convex Optimization.

Technology Areas

  • Space