A Formal Method for Analyzing the Authenticity Properties

of Procedures for Preserving Digital Records

William E. Underwood

Georgia Tech Research Institute

Atlanta, Georgia USA

william.underwood@gtri.gatech.edu

ABSTRACT

The rapid obsolescence of computing technologies creates difficulties for those concerned with the long-term preservation of records in digital form. The potential need to migrate these records across hardware and software technologies raises questions related to the records' authenticity. How can one ensure that sets of digital records have not been intentionally or inadvertently modified? How can one ensure that long-term preservation methods do not compromise the authenticity of digital records?

A formal method is described for analyzing records management and archival procedures and systems to determine whether they maintain and preserve authentic records over time. The analysis procedure is based on a formalization of archival and diplomatic concepts and principles as definitions and axioms. Concepts such as digital record, record series, and archival integrity are defined and axioms characterizing authentic documents and authentic records are formulated.

Verification of the authenticity of electronic records that are stored in computer systems and transmitted between computing systems requires the capability to reason about communications protocols and authentication mechanisms. Hence, a logical theory of communications is described that has been used to analyze the authentication and confidentiality properties of communications protocols.

Verification of the authenticity of electronic records stored in computing systems cannot be on the basis of complete information. Rather, it involves assumptions about the trustworthiness of record creating agents, record keeping systems and archival systems. It requires assumptions about shared secrets and authentic private keys used for digital signatures. Consequently, a theory of belief is described that allows us to reason and reach conclusions based on incomplete knowledge.

A procedure is described for storing and retrieving the digital records of a record creator that incorporates elements to ensure the integrity and authenticity of the records. The theories of record integrity and authenticity, communications security and belief are used to prove that the procedure achieves its goal of preserving the integrity and authenticity of the stored and retrieved digital records. This demonstrates the formal method of analysis.