Abstract
Both the formal and the computational models of cryptography contain the notion of message equivalence or indistinguishability. An encryption scheme provides soundness for indistinguishability if, when mapping formal messages into the computational model, equivalent formal messages are mapped to indistinguishable computational distributions. Previous soundness results are limited in that they do not apply when key-cycles are present. We demonstrate that an encryption scheme provides soundness in the presence of key-cycles if it satisfies the recently-introduced notion of key-dependent message (KDM) security. We also show that soundness in the presence of key-cycles (and KDM security) neither implies nor is implied by security against chosen ciphertext attack (CCA-2). Therefore, soundness for key-cycles is possible using a new notion of computational security, not possible using previous such notions, and the relationship between the formal and computational models extends beyond chosen-ciphertext security.
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Jürjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 82–94. Springer, Heidelberg (2001)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology 15(2), 103–127 (2002); Prelim. version in IFIP TCS 2000
Adão, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. In: Proc. 18-th IEEE Computer Security Foundations Workshop (CSFW), pp. 170–184. IEEE Comp. Soc. Press, Los Alamitos (2005)
Backes, M., Jacobi, C.: Cryptographically sound and machine-assisted verification of security protocols. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 675–686. Springer, Heidelberg (2003)
Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schröeder-Lowe public-key protocol. IEEE J. Selected Areas in Communications 22(10), 2075–2086 (2004); Prelim. version in FSTTCS 2003
Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17-th IEEE Computer Security Foundations Workshop, CSFW (2004); Full version on ePrint 2004/059
Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 271–290. Springer, Heidelberg (2003), Extended version on ePrint 2003/145
Backes, M., Pfitzmann, B., Waidner, M.: Secure asynchronous reactive systems. ePrint 2004/082
Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. IEEE Trans. on Dependable and Secure Computing 2(2), 109–123 (2005); Full version on ePrint 2004/300
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proc. 10-th ACM Conf. on Computer and Communications Security (CCS), pp. 220–230. ACM Press, New York (2003); Full version on ePrint 2003/015
Bana, G.: Soundness and Completeness of Formal Logics of Symmetric Encryption. PhD thesis, University of Pennsylvania (2004) Available on ePrint 2005/101
Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652–663. Springer, Heidelberg (2005) (to appear)
Bellare, M., Desai, A., Pointcheval, D., Rogaway, P.: Relations among notions of security for public-key encryption schemes. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 26–45. Springer, Heidelberg (1998); Full version available at, http://www.cs.ucsd.edu/users/mihir/papers/relations.html
Black, J., Rogaway, P., Shrimpton, T.: Encryption-scheme security in the presence of key-dependent messages. In: Nyberg, K., Heys, H.M. (eds.) SAC 2002. LNCS, vol. 2595, pp. 62–75. Springer, Heidelberg (2003)
Beaver, D.: Secure multiparty protocols and zero knowledge proof systems tolerating a faulty minority. J. Cryptology 4(2), 75–122 (1991)
Camenisch, J., Lysyanskaya, A.: An efficient system for non-transferable anonymous credentials with optional anonymity revocation. In: Pfitzmann, B. (ed.) EUROCRYPT 2001. LNCS, vol. 2045, pp. 98–118. Springer, Heidelberg (2001)
Canetti, R.: Security and composition of multiparty cryptographic protocols. J. Cryptology 3(1), 143–202 (2000)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: 42-nd IEEE Symp. on Foundations of Comp. Sci (FOCS), pp. 136–145. IEEE Comp. Soc. Press, Los Alamitos (2001); Full version on ePrint 2000/067
Canetti, R., Herzog, J.: Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). ePrint 2004/334
Canetti, R., Goldreich, O., Halevi, S.: The random oracle methodology, revisited. In: Proc. 30-th Annual ACM Symp. on Theory of Computing (STOC), pp. 209–218. ACM Press, New York (1998)
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)
Cramer, R., Shoup, V.: A practical public key cryptosystem provably secure against adaptive chosen ciphertext attack. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 13–25. Springer, Heidelberg (1998)
Datta, A., Küsters, R., Mitchell, J.C., Ramanathan, A.: On the relationships between notions of simulation-based security. In: Kilian, J. (ed.) TCC 2005. LNCS, vol. 3378, pp. 476–494. Springer, Heidelberg (2005)
Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 16–29. Springer, Heidelberg (2005) (to appear)
Dolev, D., Yao, A.C.: On the security of public-key protocols. IEEE Trans. on Information Theory 29(2), 198–208 (1983); Prelim. version in FOCS 1981
Guttman, J.D., Thayer, F.J., Zuck, L.D.: The faithfulness of abstract protocol analysis: Message authentication. In: Proc. 8-th ACM Conf. on Computer and Communications Security (CCS), pp. 186–195. ACM Press, New York (2001)
Goldwasser, S., Levin, L.: Fair computation of general functions in presence of immoral majority. In: Menezes, A., Vanstone, S.A. (eds.) CRYPTO 1990. LNCS, vol. 537, pp. 77–93. Springer, Heidelberg (1991)
Herzog, J.: Computational Soundness of Formal Adversaries. Master thesis, MIT (2002)
Herzog, J.: Computational Soundness for Standard Assumptions of Formal Cryptography. PhD thesis, MIT (2004), Available at http://theory.lcs.mit.edu/jherzog/papers/herzog-phd.pdf
Herzog, J., Liskov, M., Micali, S.: Plaintext awareness via key registration. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 548–564. Springer, Heidelberg (2003)
Horvitz, O., Gligor, V.D.: Weak key authenticity and the computational completeness of formal encryption. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 530–547. Springer, Heidelberg (2003)
Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. In: Proc. 44-th IEEE Symp. on Foundations of Comp. Sci (FOCS), pp. 372–381. IEEE Comp. Soc. Press, Los Alamitos (2003)
Laud, P.: Encryption cycles and two views of cryptography. In: Proc. 7-th Nordic Workshop on Secure IT Systems (NORDSEC), Karlstad Univ. Studies No. 31, pp. 85–100 (2002)
Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 2004 IEEE Symp. on Security and Privacy, pp. 71–85. IEEE Comp. Soc. Press, Los Alamitos (2004)
Laud, P., Corin, R.: Sound computational interpretation of formal encryption with composed keys. In: Lim, J.-I., Lee, D.-H. (eds.) ICISC 2003. LNCS, vol. 2971, pp. 55–66. Springer, Heidelberg (2004)
Lincoln, P., Mitchell, J.C., Mitchell, M., Scedrov, A.: A probabilistic polynomial-time framework for protocol analysis. In: Proc. 5-th ACM Conf. on Computer and Communications Security (CCS), pp. 112–121. ACM Press, New York (1998)
Micali, S., Rogaway, P.: Secure computation. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 392–404. Springer, Heidelberg (1992)
Micali, S., Rackoff, C., Sloan, B.: The notion of security for probabilistic cryptosystems. SIAM J. Computing 17(2), 412–426 (1998)
Micciancio, D., Panjwani, S.: Adaptive security of symbolic encryption. In: Kilian, J. (ed.) TCC 2005. LNCS, vol. 3378, pp. 169–187. Springer, Heidelberg (2005)
Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. J. Computer Security 12(1), 99–130 (2004); Prelim. version in WITS 2002
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)
Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time calculus for the analysis of cryptographic protocols. Full, revised version available on http://theory.stanford.edu/people/jcm/publications.htm . Prelim. report in FOSSACS 2004, LNCS, vol. 2987. Springer, Heidelberg (2004)
Pfitzmann, B., Schunter, M., Waidner, M.: Cryptographic security of reactive systems. In: DERA/RHUL Workshop on Secure Architectures and Information Flow, 1999. ENTCS (2000), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/menu.htm
Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proc. 7-th ACM Conf. on Computer and Communications Security, pp. 245–254. ACM Press, New York (2000); Extended version (with M. Schunter) IBM Research Report RZ 3206, 2000, http://www.zurich.ibm.com/security/models
Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. 2001 IEEE Symp. on Security and Privacy, pp. 184–200. IEEE Comp. Soc. Press, Los Alamitos (2001)
Sahai, A.: Non-malleable non-interactive zero knowledge and adaptive chosen-ciphertext security. In: 40-th IEEE Symp. on Foundations of Comp. Sci (FOCS), pp. 543–553. IEEE Comp. Soc. Press, Los Alamitos (1999)
Warinschi, B.: A computational analysis of the Needham-Schröeder-(Lowe) protocol. In: Proc. 16-th IEEE Computer Security Foundations Workshop (CSFW), pp. 248–262. IEEE Comp. Soc. Press, Los Alamitos (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Adão, P., Bana, G., Herzog, J., Scedrov, A. (2005). Soundness of Formal Encryption in the Presence of Key-Cycles. In: di Vimercati, S.d.C., Syverson, P., Gollmann, D. (eds) Computer Security – ESORICS 2005. ESORICS 2005. Lecture Notes in Computer Science, vol 3679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11555827_22
Download citation
DOI: https://doi.org/10.1007/11555827_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28963-0
Online ISBN: 978-3-540-31981-8
eBook Packages: Computer ScienceComputer Science (R0)