Ueli Maurer and Renato Renner
In the spirit of algebraic abstraction, this paper advocates the definition and use of higher levels of abstraction in cryptography (and beyond). If contrasted with the standard bottom-up approach to defining models of computation, algorithms, complexity, efficiency, and then security of cryptographic schemes, our approach is top-down and axiomatic, where lower abstraction levels inherit the definitions and theorems (e.g. a composition theorem) from the higher level, but the definition or concretization of low levels is not required for proving theorems at the higher levels. The goal is to strive for simpler definitions, higher generality of results, simpler proofs, improved elegance, possibly better didactic suitability, and to derive new insights from the abstract viewpoint.
In particular, we propose a general framework for defining and proving that a system satisfying an (abstract or ideal) specification is constructed from some systems satisfying certain (concrete or real) specifications. This puts the well-known ``ideal-world real-world'' paradigm on a new theoretical foundation, applicable in various cryptographic settings. Existing frameworks for proving composable security can be explained as special cases of our framework, thereby allowing to distinguish between relevant and less relevant aspects of the underlying technical definitions and to prove a single common composition theorem.
Some properties of our framework are as follows. It is independent of particular models of computation, communication, and adversary behavior. It can be instantiated in many different ways, for example to arrive at different notions of security or of efficiency and infeasibility. It can precisely capture settings with no central adversary where entities have potentially conflicting goals (e.g. a coercion scenario). The relation between the ideal and the real setting is tight, via an isomorphism notion for settings. The (desired) asymmetry between real and ideal is captured in a formal abstraction notion (the ideal setting is an abstraction of the real setting). A main theorem states that such an abstraction statement can be proved by using local (as opposed to monolithic) simulators.