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 \({\mathbb F}_{2^m}\). 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 \({\mathbb F}_{2^m}\). 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.
Authors were supported in part by the Department of Homeland Security under grant FA8750-08-2-0091.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)
Cortier, V., Warinschi, B.: Computationally Sound, Automated Proofs for Security Protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157–171. Springer, Heidelberg (2005)
Canetti, R., Herzog, J.C.: Universally Composable Symbolic Analysis of Mutual Authentication and Key-Exchange Protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)
Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (pcl). Electr. Notes Theor. Comput. Sci. 172, 311–358 (2007)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140–154. IEEE Computer Society (2006)
Micciancio, D., Warinschi, B.: Completeness theorems for the abadi-rogaway language of encrypted expressions. Journal of Computer Security 12(1), 99–130 (2004)
Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. In: FOCS, pp. 372–383. IEEE Computer Society (2003)
Parikh, R.: Existence and feasibility in arithmetic. J. Symb. Log. 36(3), 494–508 (1971)
Buss, S.R.: Bounded arithmetic, proof complexity and two papers of parikh. Ann. Pure Appl. Logic 96(1-3), 43–55 (1999)
Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90–101 (2009)
Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-Aided Security Proofs for the Working Cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)
Pereira, O., Lynch, N., Liskov, M., Kaynar, D., Cheung, L., Segala, R., Canetti, R.: Analyzing Security Protocols Using Time-Bounded Task-PIOAs. Discrete Event Dynamic Systems 18, 111–159 (2008)
Ramanathan, A., Mitchell, J., Scedrov, A., Teague, V.: Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 468–483. Springer, Heidelberg (2004)
Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y., Laporte, V.: On the Equality of Probabilistic Terms. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 46–63. Springer, Heidelberg (2010)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: FOCS, pp. 136–145 (2001)
Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game or a completeness theorem for protocols with honest majority. In: STOC, pp. 218–229. ACM (1987)
Canetti, R., Gajek, S.: Universally composable symbolic analysis of diffie-hellman based key exchange. Cryptology ePrint Archive, Report 2010/303 (2010), http://eprint.iacr.org/
Jutla, C.S., Roy, A.: A completeness theorem for pseudo-linear functions with applications to UC security. In: Electronic Colloquium on Computational Complexity (ECCC), vol. 17, p. 92 (2010)
Bellovin, S.M., Merritt, M.: Augmented encrypted key exchange: A password-based protocol secure against dictionary attacks and password file compromise. In: ACM Conference on Computer and Communications Security, pp. 244–250 (1993)
Canetti, R., Halevi, S., Katz, J., Lindell, Y., MacKenzie, P.: Universally Composable Password-Based Key Exchange. In: Cramer, R. (ed.) EUROCRYPT 2005. LNCS, vol. 3494, pp. 404–421. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jutla, C.S., Roy, A. (2012). Decision Procedures for Simulatability. In: Foresti, S., Yung, M., Martinelli, F. (eds) Computer Security – ESORICS 2012. ESORICS 2012. Lecture Notes in Computer Science, vol 7459. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33167-1_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-33167-1_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33166-4
Online ISBN: 978-3-642-33167-1
eBook Packages: Computer ScienceComputer Science (R0)