Extending intransitive noninterference with probabilities in information flow security

Probabilistic information flow security properties such as probabilistic noninterference ensure that different behaviors of the high part of the system do not affect the probability distribution of the low events. However, to deal with real applications, it is necessary to cope with intransitive flow policies like channel control and secure downgrading of probabilistic information. In this paper, we introduce the concept of trust domain into Probabilistic Secure Process Algebra (PSPA), and then extend intransitive noninterference to probabilistic systems which is modeled by PSPA. Based on weak probabilistic bisimulation equivalence, we propose security properties for intransitive flow for probabilistic systems, in particular two properties which are persistent, in the sense that if a system is secure then all of its reachable states are secure too. Moreover, we show that such persistent intransitive probabilistic properties can be characterized in terms of unwinding conditions which demand properties of individual actions.