Secure Reactive Systems

We introduce a precise definition of the security of reactive systems following the simulatability approach in the synchronous model. No simulatability definition for reactive systems has been worked out in similar detail and generality before. Particular new aspects are a precise switching model that allows us to discover timing vulnerabilities, a precise treatment of the interaction of users and adversaries, and independence of the trust model.

We present several theorems relating the definition to other possible variants. They substantiate which aspects of such a definition do and do not make a real difference and are useful in larger proofs. We also have a methodology for defining the security of practical systems by simulation of an ideal system, although they typically have imperfections tolerated for efficiency reasons.

We sketch several examples to show the range of applicability, and present a very detailed proof of one example, secure reactive message transmission. Its main purpose is to validate the model by an example of a class that has also been considered in other models, but we did encounter new problems related to our strict requirements on timing security.