Composition and integrity preservation of secure reactive systems

11 years 9 months ago
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 ...
Birgit Pfitzmann, Michael Waidner
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where CCS
Authors Birgit Pfitzmann, Michael Waidner
Comments (0)