Paper 2004/082

The Reactive Simulatability (RSIM) Framework for Asynchronous Systems

Michael Backes, Birgit Pfitzmann, and Michael Waidner


We define \emph{reactive simulatability} for general asynchronous systems. Roughly, simulatability means that a real system implements an ideal system (specification) in a way that preserves security in a general cryptographic sense. Reactive means that the system can interact with its users multiple times, e.g., in many concurrent protocol runs or a multi-round game. In terms of distributed systems, reactive simulatability is a type of refinement that preserves particularly strong properties, in particular confidentiality. A core feature of reactive simulatability is \emph{composability}, i.e., the real system can be plugged in instead of the ideal system within arbitrary larger systems; this is shown in follow-up papers, and so is the preservation of many classes of individual security properties from the ideal to the real systems. A large part of this paper defines a suitable system model. It is based on probabilistic IO automata (PIOA) with two main new features: One is \emph{generic distributed scheduling}. Important special cases are realistic adversarial scheduling, procedure-call-type scheduling among colocated system parts, and special schedulers such as for fairness, also in combinations. The other is the definition of the \emph{reactive runtime} via a realization by Turing machines such that notions like polynomial-time are composable. The simple complexity of the transition functions of the automata is not composable. As specializations of this model we define security-specific concepts, in particular a separation beween honest users and adversaries and several trust models. The benefit of IO automata as the main model, instead of only interactive Turing machines as usual in cryptographic multi-party computation, is that many cryptographic systems can be specified with an ideal system consisting of only one simple, deterministic IO automaton without any cryptographic objects, as many follow-up papers show. This enables the use of classic formal methods and automatic proof tools for proving larger distributed protocols and systems that use these cryptographic systems.

Available format(s)
Publication info
Published elsewhere. Accepted at Information and Computation
reactive systemsreactive simulatability
Contact author(s)
backes @ cs uni-sb de
2007-05-07: revised
2004-03-16: received
See all versions
Short URL
Creative Commons Attribution


      author = {Michael Backes and Birgit Pfitzmann and Michael Waidner},
      title = {The Reactive Simulatability (RSIM) Framework for Asynchronous Systems},
      howpublished = {Cryptology ePrint Archive, Paper 2004/082},
      year = {2004},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.