Accession Number:

ADA465575

Title:

The Epistemic Representation of Information Flow Security in Probabilistic Systems

Descriptive Note:

Conference paper

Corporate Author:

NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)

Personal Author(s):

Report Date:

1995-06-01

Pagination or Media Count:

16.0

Abstract:

We set out a logic for reasoning about multilevel security of probabilistic systems. This logic includes modalities for time, knowledge, and probability. In earlier work we gave syntactic definitions of multilevel security and showed that their semantic interpretations are equivalent to independently motivated information-theoretic definitions. This paper builds on that earlier work in two ways. First, it substantially recasts the language and model of computation into the more standard Halpern-Tuttle framework for reasoning about knowledge and probability. Second, it brings together two distinct characterizations of security from that work. One was equivalent to the information-theoretic security criterion for a system to be free of covert channels but was difficult to prove. The other was a verification condition that implied the first it was more easily provable but was too strong. This paper presents a characterization that is syntactically very similar to our previous verification condition but is proven to be semantically equivalent to the security criterion. The new characterization also means that our security criterion is expressible in a simpler logic and model.

Subject Categories:

  • Computer Programming and Software
  • Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE