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 .