Secrecy in multiagent systems

We introduce a general framework for reasoning about secrecy requirements in multiagent systems. Because secrecy requirements are closely connected with the knowledge of individual agents of a system, our framework employs the modal logic of knowledge within the context of the well-studied runs and systems framework. Put simply, "secrets" are facts about a system that low-level agents are never allowed to know. The framework presented here allows us to formalize this intuition precisely, in a way that is much in the spirit of Sutherland\´s notion of nondeducibility. Several well-known attempts to characterize the absence of information flow, including separability, generalized noninterference, and nondeducibility on strategies, turn out to be special cases of our definition of secrecy. However, our approach lets us go well beyond these definitions. It can handle probabilistic secrecy in a clean way, and it suggests generalizations of secrecy that may be useful for dealing with resource-bounded reasoning and with issues such as downgrading of information.