Completeness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions

We show that the Abadi-Rogaway logic of indistinguishability for cryptographic expressions is not complete by giving a natural example of a secure encryption function and a pair of expressions, such that the distributions associated to the two expressions are computationally indistinguishable, but equality cannot be proved within the Abadi-Rogaway logic. Then, we show that if a stronger, yet natural, notion of security for encryption is used (namely, that of authenticated encryption), then the Abadi-Rogaway logic is both sound and complete. In addition, we consider a refinement of the Abadi-Rogaway logic that overcomes certain limitations of the original proposal, allowing for encryption functions that do not hide the length of the message being sent. Both the soundness theorem of Abadi and Rogaway, and our completeness result for authenticated encryption easily extend to this more realistic notion of secrecy.