The epistemic representation of information flow security in probabilistic systems

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