A logical formalization of secrecy

A formal definition is given of what must be considered as secret in a multilevel computer system. The author´s point of view drastically differs from the classical approaches since it advocates that all the information contained in the sequence of high level inputs need not be considered as secret. The approach is based on an extended logic involving epistemic and deontic modal operators. This leads to a new security property called nondisclosure on inputs that must really be considered as secret. The author refines this first definition to obtain a stronger property simply called nondisclosure which protects both high level strategies and high level outputs. Finally, a suggestion is given on how one could combine the causality and nondisclosure properties to obtain a decision procedure for analyzing the security of computer systems