Strategy-Based and Knowledge-Based Models of Information Flow: Equivalence and Decidability

We show that two notions of information flow, one which is strategy-based and the other knowledge-based, are equivalent. The first notion models the possibilities that a high-level user has to send information to the low-level user by distinctly observable runs, whereas the second notion models information leak as variations in the knowledge of the low-level user during his observation of the system behavior. We also give an algorithm for deciding whether a finite-state system has no information flow in our setting, by reducing the problem to a reachability problem in finite automata.