CryptoDB
The Reactive Simulatability (RSIM) Framework for Asynchronous Systems
| Authors: | |
|---|---|
| Download: | |
| 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. |
BibTeX
@misc{eprint-2004-12055,
title={The Reactive Simulatability (RSIM) Framework for Asynchronous Systems},
booktitle={IACR Eprint archive},
keywords={foundations / reactive systems, reactive simulatability, security analysis of cryptographic protocols},
url={http://eprint.iacr.org/2004/082},
note={Accepted at Information and Computation backes@cs.uni-sb.de 13640 received 15 Mar 2004, last revised 7 May 2007},
author={Michael Backes and Birgit Pfitzmann and Michael Waidner},
year=2004
}