On the composition of secure systems

When complex systems are constructed from simpler components it is important to know how properties of the components behave under composition. We present various compositionality results for security properties. In particular we introduce a novel security property and show that this property is, in general, composable although it is weaker than forward correctability. Moreover we demonstrate that certain nontrivial security properties emerge under composition and illustrate how this fact can be exploited. All compositionality results that we present are verified with the help of a single, quite powerful lemma. Basing on this lemma, we also re-prove several already known compositionality results with the objective to unify these results. As a side effect, we obtain a classification of known compositionality results for security properties.