Decision procedures for simulatability

Abstract

We address the question of automatically proving security theorems in the universally composable (UC) model for ideal and real functionalities composed of if-then-else programs with uniform random number generation and data objects from the additive group of double-struck F 2m. We prove that for this restricted yet powerful language framework, there is an effective procedure to decide if a real functionality realizes an ideal functionality, and this procedure is in computational time independent of m, which is essentially the security parameter. To this end, we consider multivariate pseudo-linear functions, which are functions computed by branching programs over data objects from the additive group of double-struck F 2m. The conditionals in such programs are built from equality constraints over linear expressions, closed under negation and conjunction. Let f 1, f 2,..., f k be k pseudo-linear functions in n variables, and let f be another pseudo-linear function in the same n variables. We show that if f is a function of the given k functions, then it must be a pseudo-linear function of the given k functions. This generalizes the straightforward claim for just linear functions. Proceeding further, we generalize the theorem to randomized pseudo-linear functions. We also prove a more general theorem where the k functions can in addition take further arguments, and prove that if f can be represented as an iterated composition of these k functions, then it can be represented as a probabilistic pseudo-linear iterated composition of these functions. Additionally, we allow f itself to be a randomized function, i.e. we give a procedure for deciding if f is a probabilistic sub-exponential (in m) time iterated function of the given k randomized functions. The decision procedure runs in computational time independent of m. © 2012 Springer-Verlag.