Weak Key Authenticity and the Computational Completeness of Formal Encryption

  • Omer Horvitz
  • Virgil Gligor
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2729)


A significant effort has recently been made to rigorously relate the formal treatment of cryptography with the computational one. A first substantial step in this direction was taken by Abadi and Rogaway [AR02]. Considering a formal language that treats symmetric encryption, [AR02] show that an associated formal semantics is sound with respect to an associated computational semantics, under a particular, sufficient, condition on the computational encryption scheme. In this paper, we give a necessary and sufficient condition for completeness, tightly characterizing this aspect of the exposition. Our condition involves the ability to distinguish a ciphertext and the key it was encrypted with, from a ciphertext and a random key. It is shown to be strictly weaker than a previously suggested condition for completeness (confusion-freedom of Micciancio and Warinschi [MW02]), and should be of independent interest.


Cryptography Encryption Authentication Formal Reasoning Completeness Weak Key Authenticity 


  1. [AJ01]
    Abadi, M., Jurgens, J.: Formal Eavesdropping and its Computational Interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, p. 82. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. [AR02]
    Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography (the computational soundness of formal encryption). Journal of Cryptology 15(2), 103–128 (2000); also Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, p. 3–22. Springer, Heidelberg (2000)Google Scholar
  3. [BB01]
    Bellare, M., Boldyreva, A., Desai, A., Pointcheval, D.: Key-Privacy in Public- Key Encryption. In: Boyd, C. (ed.) ASIACRYPT 2001. LNCS, vol. 2248, pp. 566–582. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. [BD97]
    Bellare, M., Desai, A., Jokipii, E., Rogaway, P.: A Concrete Security Treatment of Symmetric Encryption: Analysis of the DES Modes of Operation. In: Proceedings of the 38th Annual Symposium on Foundations of Computer Science, FOCS 1997 (1997)Google Scholar
  5. [BN00]
    Bellare, M., Namprempre, C.: Authenticated Encryption: Relations Among Notions and Analysis of the Generic Composition Paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol. 1976, pp. 541–545. Springer, Heidelberg (2000)Google Scholar
  6. [GG86]
    Goldreich, O., Goldwasser, S., Micali, S.: How to Construct Random Functions. Journal of the ACM 33(4), 792–807 (1986)CrossRefMathSciNetGoogle Scholar
  7. [GM84]
    Goldwasser, S., Micali, S.: Probabilistic Encryption. Journal of Computer and System Sciences 28, 270–299 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  8. [HG03]
    O. Horvitz, V. Gligor. Weak Key Authenticity and the Computational Completeness of Formal Encryption. Full version available at,
  9. [KY00]
    Katz, J., Yung, M.: Unforgeable Encryption and Chosen Ciphertext Secure Modes of Operation. In: Schneier, B. (ed.) FSE 2000. LNCS, vol. 1978, pp. 284–299. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. [Ll87]
    Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987); Section 1.5zbMATHGoogle Scholar
  11. [LN84]
    Lassez, J.L., Nguyen, V.L., Sonenberg, E.A.: Fixpoint Theorems and Semantics: a Folk Tale. Information Processing Letters 14(3), 112–116 (1982)zbMATHCrossRefMathSciNetGoogle Scholar
  12. [MW02]
    Micciancio, D., Warinschi, B.: Completeness Theorems for the Abadi-Rogaway Language of Encrypted Expressions. In: Journal of Computer Security (to appear); Also in Proceedings of the Workshop on Issues in the Theory of Security (2002)Google Scholar
  13. [Ta55]
    Tarski, A.: A Lattice-theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics 5, 285–309 (1955)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Omer Horvitz
    • 1
  • Virgil Gligor
    • 2
  1. 1.Department of Computer ScienceUniversity of MarylandCollege ParkUSA
  2. 2.Department of Electrical and Computer EngineeringUniversity of MarylandCollege ParkUSA

Personalised recommendations