Sound and Finegrain Specification of Ideal Functionalities

Theoretical Foundations of Practical Information Security

计算机科学;物理学

Juan A. Garay ∗ Aggelos Kiayias † Hong-Sheng Zhou†

PID  :  82170

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Nowadays it is widely accepted to formulate the security of a protocol carrying out a given task via the “trustedparty paradigm,” where the protocol execution is compared with an ideal process where the outputs are computed by a trusted party that sees all the inputs. A protocol is said to securely carry out a given task if running the protocol with a realistic adversary amounts to “emulating” the ideal process with the appropriate trusted party. In the Universal Composability (UC) framework the program run by the trusted party is called an ideal functionality. While this simulationbased security formulation provides strong security guarantees, its usefulness is contingent on the properties and correct specification of the ideal functionality, which, as demonstrated in recent years by the coexistence of complex, multiple functionalities for the same task as well as by their “unstable” nature, does not seem to be an easy task. In this paper we address this problem, by introducing a general methodology for the sound specification of ideal functionalities. First, we introduce the class of canonical ideal functionalities for a cryptographic task, which unifies the syntactic specification of a large class of cryptographic tasks under the same basic template functionality. Furthermore, this representation enables the isolation of the individual properties of a cryptographic task as separate members of the corresponding class. By endowing the class of canoni cal functionalities with an algebraic structure we are able to combine basic functionalities to a single final canonical functionality for a given task. Effectively, this puts forth a bottomup approach for the specifica tion of ideal functionalities: first one defines a set of basic constituent functionalities for the task at hand, and then combines them into a single ideal functionality taking advantage of the algebraic structure. In our framework, the constituent functionalities of a task can be derived either directly or, following a translation strategy we introduce, from existing gamebased definitions; such definitions have in many cases captured desired individual properties of cryptographic tasks, albeit in less adversarial settings than universal composition. Our translation methodology entails a sequence of steps that derive a corresponding canonical functionality given a gamebased definition. In this way, we obtain a welldefined mapping of gamebased security properties to their corresponding UC counterparts. Finally, we demonstrate the power of our approach by applying our methodology to a variety of basic cryptographic tasks, including commitments, digital signatures, zeroknowledge proofs, and oblivious trans fer. While in some cases our derived canonical functionalities are equivalent to existing formulations, thus attesting to the validity of our approach, in others they differ, enabling us to “debug” previous definitions