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.
"Proceedings of 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2007)", Timisoara, Romania, 26-29 September 2007, to appear.