Abstract
We consider a class of two-party function evaluation protocols in which the parties are allowed to use ideal functionalities as well as a set of powerful primitives, namely commitments, homomorphic encryption, and certain zero-knowledge proofs. With these it is possible to capture protocols for oblivious transfer, coin-flipping, and generation of multiplication-triples.
We show how any protocol in our class can be compiled to a symbolic representation expressed as a process in an abstract process calculus, and prove a general computational soundness theorem implying that if the protocol realises a given ideal functionality in the symbolic setting, then the original version also realises the ideal functionality in the standard computational UC setting. In other words, the theorem allows us to transfer a proof in the abstract symbolic setting to a proof in the standard UC model.
Finally, we have verified that the symbolic interpretation is simple enough in a number of cases for the symbolic proof to be partly automated using the ProVerif tool.
The authors acknowledge support from the Danish National Research Foundation and The National Science Foundation of China (under the grant 61061130540) for the Sino-Danish Center for the Theory of Interactive Computation, and also from the CFEM research centre (supported by the Danish Strategic Research Council) within which part of this work was performed.
Chapter PDF
Similar content being viewed by others
Keywords
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115. ACM Press, New York (2001)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15, 103–127 (2002)
Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. In: Symposium on Logic in Computer Science (LICS 2005), pp. 331–340. IEEE (2005)
Bendlin, R., Damgård, I., Orlandi, C., Zakarias, S.: Semi-homomorphic encryption and multiparty computation. In: Paterson, K.G. (ed.) EUROCRYPT 2011. LNCS, vol. 6632, pp. 169–188. Springer, Heidelberg (2011)
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)
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing 5(4), 193–207 (2008)
Backes, M., Maffei, M., Mohammadi, E.: Computationally sound abstraction and verification of secure multi-party computations. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). LIPIcs, vol. 8, pp. 352–363. Schloss Dagstuhl (2010)
Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the needham-schroeder-lowe public-key protocol. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 1–12. Springer, Heidelberg (2003)
Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable dolev-yao style cryptographic library. In: Computer Security Foundations Workshop (CSFW 2004), pp. 204–218. IEEE (2004)
Backes, M., Pfitzmann, B.: On the cryptographic key secrecy of the strengthened yahalom protocol. In: Fischer-Hübner, S., Rannenberg, K., Yngström, L., Lindskog, S. (eds.) Security and Privacy in Dynamic Environments. IFIP, vol. 201, pp. 233–245. Springer, Boston (2006)
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Computer and Communications Security (CCS 2003), pp. 220–230. ACM, New York (2003)
Böhl, F., Unruh, D.: Symbolic universal composability. In: Computer Security Foundations (CSF 2013), pp. 257–271. IEEE (2013)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Foundations of Computer Science (FOCS 2001), pp. 136–145. IEEE Computer Society (2001)
Canetti, R.: Composable formal security analysis: Juggling soundness, simplicity and efficiency. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 1–13. Springer, Heidelberg (2008)
Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Computer and Communications Security (CCS 2008), pp. 109–118. ACM (2008)
Canetti, R., Gajek, S.: Universally composable symbolic analysis of diffie-hellman based key exchange. IACR Cryptology ePrint Archive, 2010:303 (2010)
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)
Comon-Lundh, H., Hagiya, M., Kawamoto, Y., Sakurada, H.: Computational soundness of indistinguishability properties without computable parsing. In: Ryan, M.D., Smyth, B., Wang, G. (eds.) ISPEC 2012. LNCS, vol. 7232, pp. 63–79. Springer, Heidelberg (2012)
Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. Journal of Automated Reasoning 46, 225–259 (2011)
Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (PCL). Electronic Notes in Theoretical Computer Science 172, 311–358 (2007)
Delaune, S., Kremer, S., Pereira, O.: Simulation based security in the applied pi calculus. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009), vol. 4, pp. 169–180 (2009)
Damgård, I., Nielsen, J.B., Orlandi, C.: Essentially optimal universally composable oblivious transfer. In: Lee, P.J., Cheon, J.H. (eds.) ICISC 2008. LNCS, vol. 5461, pp. 318–335. Springer, Heidelberg (2009)
Laud, P., Ngo, L.: Threshold homomorphic encryption in the universally composable cryptographic library. In: Baek, J., Bao, F., Chen, K., Lai, X. (eds.) ProvSec 2008. LNCS, vol. 5324, pp. 298–312. Springer, Heidelberg (2008)
Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science 353(1-3), 118–164 (2006)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)
Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. of IEEE Symposium on Security and Privacy, pp. 184–200 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 International Association for Cryptologic Research
About this paper
Cite this paper
Dahl, M., Damgård, I. (2014). Universally Composable Symbolic Analysis for Two-Party Protocols Based on Homomorphic Encryption. In: Nguyen, P.Q., Oswald, E. (eds) Advances in Cryptology – EUROCRYPT 2014. EUROCRYPT 2014. Lecture Notes in Computer Science, vol 8441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-55220-5_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-55220-5_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-55219-9
Online ISBN: 978-3-642-55220-5
eBook Packages: Computer ScienceComputer Science (R0)