Weak Key Authenticity and the Computational Completeness of Formal Encryption

Abstract. 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. Keywords. Cryptography, Encryption, Authentication, Formal Reasonin...

• Type: Conference
• Year: 2003
• Where: CRYPTO
• Authors: Omer Horvitz, Virgil D. Gligor
• Keywords: Associated Computational Semantics, Associated Formal Semantics, CRYPTO 2003, first Substantial Step