Formalization of Public Key Infrastructures

Abstract

Public key technology within a Public Key Infrastructure (PKI) has been widely promoted to support secure digital communications. However, imprecise specifications for PKIs, which are usually written in a natural language, have led to varying implementation and interpretations of conformance. There have also been cases where defects have been identified years later, some of which were serious and could cause incorrect acceptance of certification paths. In this paper we provide a formal solution to the PKI specification dilemma by introducing a state-based model for the description of the architecture of a PKI and related functions. We propose a formal approach to the representation of, and reasoning about, the behavior and security properties of PKIs, and also give a framework for mechanizing our theory in the Isabelle theorem prover. With our method, the essential aspects of PKIs can be clearly formulated, facilitating the testing and analysis of their implementations in a more rigorous and well defined way.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 2001
Accession Number
ADA392288

Entities

People

  • Chuchang Liu
  • Marie Henderson
  • Maris Ozols
  • Tony Cant

Organizations

  • Defence Science and Technology Group

Tags

Communities of Interest

  • C4I
  • Cyber
  • Space

DTIC Thesaurus Topics

  • Authentication
  • Computer Network Security
  • Computer Networks
  • Computers
  • Cryptography
  • Cybersecurity
  • Data Transmission Security
  • Digital Communications
  • Electronic Commerce
  • Engineering
  • Identities
  • Information Security
  • Information Systems
  • Language
  • Secure Communications
  • Security Protocols
  • Standardization

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Cybersecurity.
  • Software Engineering.