A taxonomy of trace-based security properties for CCS

Several information flow security definitions, proposed in the literature, are generalized and adapted to the model of labelled transition systems. This very general model has been widely used as a semantic domain for process algebras, such as Milner´s CCS. As a by-product, we provide CCS with a set of security notions, hence relating these two areas of concurrency research. A classification of these generalised security definitions is presented, taking into account also some additional properties, such as input totality, which can influence this taxonomy. We also show that some of these security properties are composable w.r.t. the operators of parallellism and action restriction