Abstract
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.
| Translated title of the contribution | Completeness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions |
|---|---|
| Original language | English |
| Pages (from-to) | 99-129 |
| Journal | Journal of Computer Security |
| Volume | 12(1) |
| Publication status | Published - 2004 |