A Unified Cryptographic Protocol Logic

Abstract

We present a logic for analyzing cryptographic protocols. This logic is based on a unification of four of its predecessors in the BAN family of logics, namely those given in [GNY90], [AT91], [vO93b], and BAN itself [BAN89]. The logic herein captures the desirable features of its predecessors and more; nonetheless, as a logic it is relatively simple and simple to use. We also present a model-theoretic semantics, and we prove soundness for the logic with respect to that semantics. We illustrate the logic by applying it to the Needham- Schroeder protocol, revealing that BAN analysis of it may lead to inappropriate conclusions in some settings. We also use the logic to analyze two key agreement protocols, examining an attack on one of them.

Open PDF

Document Details

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

Entities

People

  • Paul C. Van Oorschot
  • Paul Syverson

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Algorithms
  • Asymetric Encryption
  • Computational Complexity
  • Computations
  • Computer Programs
  • Computer Science
  • Computers
  • Cryptography
  • Cybersecurity
  • Formal Languages
  • Language
  • Notation
  • Reasoning
  • Reliability
  • Security Protocols
  • Theorems

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Artificial Intelligence
  • Computer Engineering
  • Theoretical Analysis.