Composability of secrecy

Abstract

Modularity has been seen to be very useful in system development. Unfortunately, many security properties proposed in the literature are not composable (in contrast to other system properties), which is required to reason about them in a modular way. We present work supporting modular development of secure systems by showing a standard notion of secrecy to be composable wrt. the standard composition in the specification framework Focus (extended with cryptographic primitives). Additionally, the property is preserved under the standard refinement. We consider more fine-grained conditions useful in modular verification of secrecy.