Invariant Generation Techniques in Cryptographic Protocol Analysis

Abstract

The growing interest in the application of formal methods of cryptographic protocol analysis has led to the development of a number of different techniques for generating and describing invariants that are defined in terms of what messages an intruder can and cannot learn. These invariants, which can be used to prove authentication as well as secrecy results, appear to be central to many different tools and techniques. However, since they are usually developed independently for different systems, it is often not easy to see what they have in common with each other, or to tell whether or not they can be used in systems other than the ones for which they were developed. In this paper we attempt to remedy this situation by giving an overview of several of these techniques, discussing their relationships to each other, and developing a simple taxonomy. We also discuss some of the implications for future research.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2000
Accession Number
ADA464088

Entities

People

  • Catherine Meadows

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Analyzers
  • Authentication
  • Communication Systems
  • Communications Protocols
  • Computer Communications
  • Control Systems
  • Cryptography
  • Demographic Cohorts
  • Generators
  • Identities
  • Language
  • Military Research
  • Security
  • Security Protocols
  • Sequences
  • Specifications
  • Transitions

Fields of Study

  • Computer science

Readers

  • Calculus or Mathematical Analysis
  • Cybersecurity.
  • Systems Analysis and Design