An Iterative Approach for the Satisfaction of Security Using the Intransitive Non-Interference Property

In this paper, we derive an iterative approach for the design of systems and protocols that are secure, with respect to intransitive non-interference (INI), a basic security property, assuring the non-devulgation of information through covert channels. Obviously, a system that does not satisfy INI, is, in some ways, not secure. Our iterative approach is composed of three steps : system design and modeling (1), INI verification (2), and INI satisfaction (3). The basic idea, is that a system's designer during the first step of design, is focused on developing the core and necessary functionality, perhaps, while paying little attention to INI. Then, security of the system is verified, and if INI is not satisfied, the system must be modified in order it to make it secure. These modifications must be carried out, in a minimal way, as to preserve, in as much as possible, its core behavior. Our approach uses formulas for computing the minimal superlangage satisfying the INI property. We also investigate the implementation of these formulas based on automata models. Our approach can be applied to all systems and protocols with a three level security lattice, typically, sufficient for systems using cryptographic protocols. We also give a case study that illustrates our approach applicability to cryptographic protocols and systems.