Secure Reactive Systems
Birgit Pfitzmann, Matthias Schunter, Michael Waidner · 2000
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...