On Deducible Information Flow in Synchronous Models

We revisit the synchronous model of Wittbold and Johnson of information flow, by investigating the relationship between two notions of information flow: a notion based on counting differently-observable high-level strategies and a notion based on the deductions that the low-level user makes on high-level activity while observing system behavior. We then relate our results to some known models of information flow: we show that bisimulation-based equivalence checking is too strong, since it labels variations in the observation due to system nondeterminism as information flow.We also show that a synchronous, trace-based statement of Generalized Noninterference does not properly capture information flow either. Finally we give a decision procedure for detecting information flow for finitestate systems.