Composition and integrity preservation of secure reactive systems

We consider compositional properties of reactive systems that are secure in a cryptographic sense. We follow the wellknown simulatability approach, i.e., the specification is an ideal system and a real system should in some sense simulate it. We recently presented the first detailed general definition concept for reactive systems that allows abstraction and enables proofs of efficient real-life systems like secure channels or certified mail. We prove two important properties of this definition, preservation of integrity and secure composition: First, a secure real system satisfies all integrity requirements (e.g., safety requirements expressed in temporal logic) that are satisfied by the ideal system. Secondly, if a composed system is designed using an ideal subsystem, it will remain secure if a secure real subsystem is used instead. Such a property was so far only known for non-reactive simulatability. Both properties are important for putting formal verification methods for ...

• Type: Conference
• Year: 2000
• Where: CCS
• Authors: Birgit Pfitzmann, Michael Waidner
• Keywords: CCS 2000, Reactive Systems, Secure Real Subsystem, Security Privacy, Wellknown Simulatability Approach