Back to Search
Start Over
The reactive simulatability (RSIM) framework for asynchronous systems
- Source :
-
Information & Computation . Dec2007, Vol. 205 Issue 12, p1685-1720. 36p. - Publication Year :
- 2007
-
Abstract
- Abstract: We define 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 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 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 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 between 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. [Copyright &y& Elsevier]
- Subjects :
- *SIMULATION methods & models
*SYSTEMS design
*DATA encryption
*ROBOTS
Subjects
Details
- Language :
- English
- ISSN :
- 08905401
- Volume :
- 205
- Issue :
- 12
- Database :
- Academic Search Index
- Journal :
- Information & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 27334366
- Full Text :
- https://doi.org/10.1016/j.ic.2007.05.002