A Formal Analysis of Some Properties of Kerberos 5 Using MSR

Abstract

We formalize aspects of the Kerberos 5 authentication protocol in the Multi-Set Rewriting formalism (MSR) on two levels of detail. The more detailed formalization reflects the intricate structure of the Kerberos 5 specification, taking into account several protocol features which have not been previously considered. In the abstract formalization, we prove an authentication property about Kerberos 5. We discovered three anomalies, one of which occurs on both levels of detail, while the other two rely on the richer structure of the detailed formalization. We also discuss how the addition of checksums (some of which are in the protocol specification and some of which are not) may eliminate some of these anomalies.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2002
Accession Number
ADA484162

Entities

People

  • Aaron D. Jaggard
  • Andre Scedrov
  • Frederick Butler
  • Iliano Cervesato

Organizations

  • University of Pennsylvania

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Authentication
  • Cryptography
  • Cybersecurity
  • Databases
  • Demographic Cohorts
  • Denial Of Service Attack
  • Information Operations
  • Language
  • Mathematics
  • Security Protocols
  • Specifications
  • Standards
  • Test Beds

Fields of Study

  • Computer science

Readers

  • Cybersecurity.
  • Fault Tolerant Diagnosis of Black and White Balloon Isolation Tests Using ¥.
  • Systems Analysis and Design