International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: Sound and Fine-grain Specification of Cryptographic Tasks

Juan A. Garay
Aggelos Kiayias
Hong-Sheng Zhou
Search ePrint
Search Google
Abstract: The Universal Composability (UC) framework, introduced by Canetti, allows for the design of cryptographic protocols satisfying strong security properties, such as non-malleability and preservation of security under (concurrent) composition. In the UC framework (as in several other frameworks), the security of a protocol carrying out a given task is formulated via the ``trusted-party 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 UC framework the program run by the trusted party is called an {\em ideal functionality}. However, while this simulation-based security formulation provides strong security guarantees, its usefulness is contingent on the properties and correct specification of the realized 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. On the other hand, the more traditional, {\em gamed-based} definitions of cryptographic tasks, although providing a less satisfying level of security (stand-alone executions, or executions in very controlled settings), have been successful in terms of formalizing as well as capturing the underlying task's natural properties. In this paper we address this gap in the security modeling of cryptographic properties, and introduce a general methodology for translating game-based definitions of properties of cryptographic tasks to syntactically concise ideal functionality programs. Moreover, taking advantage of a suitable algebraic structure of the space of our ideal functionality programs, we are able to ``accumulate'' ideal functionalities based on many different game-based security notions. In this way, we can obtain a well-defined mapping of all the game-based security properties of a cryptographic task to its corresponding UC counterpart. In addition, the methodology allows us to ``debug'' existing ideal functionalities, establish relations between them, and make some critical observations about the modeling of the ideal process in the UC framework. We demonstrate the power of our approach by applying our methodology to a variety of basic cryptographic tasks, including commitments, digital signatures, public-key encryption, zero-knowledge proofs, and oblivious transfer. Instrumental in our translation methodology is the new notion of a {\em canonical functionality class} for a cryptographic task which is endowed with a bounded semilattice structure. This structure allows the grading of ideal functionalities according to the level of security they offer as well as their natural joining, enabling the modular combination of security properties.
  title={Sound and Fine-grain Specification of Cryptographic Tasks},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols / universal composability, security definitions, lattices and partial orders},
  note={ 13963 received 24 Mar 2008},
  author={Juan A. Garay and Aggelos Kiayias and Hong-Sheng Zhou},