**Authors:** Daniele Micciancio and Bogdan Warinschi.

Journal of Computer Security, 12(1), 2004, pp. 99-129

**Abstract:** We show that the Abadi-Rogaway logic of
indistinguishability for cryptographic expressions is not complete, 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.

**Preliminary version**: Workshop on Issues in the Theory of
Security - WITS
2002. Jan. 12-13. Portland, Oregon.