We consider compositional properties of reactive systems that are secure in a cryptographic sense. We follow the well-known 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 of this 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 verificaiton methods for systems using cryptography on a sound basis.
By: B. Pfitzmann, M. Waidner
Published in: RZ3234 in 2000
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .