An algorithmic approach to verification of intransitive non-interference in security policies

In this paper, we generalize our algorithmic approach to the problem of verification of the property of intransitive non-interference (INI) using tools and concepts of discrete event systems (DES) that we first proposed in Hadj-Alouane, N., et al. (2004). The reason that we are interested in INI is that it can be used to solve several important security problems in systems and protocols. We have shown that the notion of iP-observability captures precisely the property of INI. In Hadj-Alouane, N., et al. (2004), we have developed algorithms to check iP-observability by indirectly checking P-observability. This indirect method works only for systems with at most three security levels. In this paper, we develop a direct method for checking iP-observability, which is based on an insightful observation that iP-purge is a left-congruence in terms of relations on formal languages. This directly method can be used for systems with more than three security levels. To demonstrate the application of our approach, in the full version of this paper, we propose a formal method to detect denial of service vulnerabilities in security protocols based on INI. This method is illustrated using the TCP/IP protocol.