Welcome to the resource topic for
**2004/082**

**Title:**

The Reactive Simulatability (RSIM) Framework for Asynchronous Systems

**Authors:**
Michael Backes, Birgit Pfitzmann, Michael Waidner

**Abstract:**

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.

**ePrint:**
https://eprint.iacr.org/2004/082

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

**Example resources include:**
implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .