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.
|