Nondeterministic noninterference and deducible information ow

We dene two alternative notions related to the security of information ow. The rst one is a weaker form of non-interference, which we call nondeterministic noninterfer-ence. It gives the view of the high-level user (Harry) on the requirements a system must satisfy in order for infor-mation about his activity not to be leaked to low-level. The second one is based on a semantic framework for dening the deductions that the low-level user makes by observing system behavior, and especially on the fact that a new de-duction does not contradict a previous one. This second notion gives the low-level user (Larry’s) view on the char-acterization of the systems which do not allow him to gain information about high-level activity. We then show that the two views are equivalent. The nondeterministic noninterference is based on a re-statement of the principle of noninterference. The main novelty in this notion is that it takes into consideration the possibility for the system to restrict Harry’s choices with-out impending on information ow. This makes our notion strictly weaker than existing notions like the Generalized Noninterference, Forward Correctability, the Perfect Secu-rity Property and others. In our framework, Harry’s choices are dened as strate-gies for Harry to interact with the system, in order to in-corporate system nondeterminism that is inherent in possi-bilistic trace models. Hence, our restatement of noninterfer-ence is that different high-level strategies should not lead to different observations by low-level users. Alternatively, and equivalently, we propose Larry’s view of this princi-ple, which would be that high-level strategies should not be deduced by low-level users. The equivalence of the two notions gives strong evidence that our framework might lay more solid foundations for a theory of information ow. We also give an algorithm for deciding whether a nite