Completeness theorems for the Abadi-Rogaway language 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 logic. We then introduce a new property for encryption schemes, which we call confusion freeness, and show that the Abadi-Rogaway logic is sound and complete, whenever the encryption scheme used satisfies this property. We relate confusion freeness with standard cryptographic security notions, showing that any authenticated encryption scheme is confusion free. We also consider two extensions of the basic logic. The first is 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 confusion free (or authenticated) encryption easily extend to this more realistic notion of secrecy. The second is an extension of the logic due to Abadi and Jürjens that allows to study more complex protocols in the presence of a passive adversary. Our completeness results holds for this extended logic as well.