Completeness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions

Daniele Micciancio, Bogdan Warinschi

Research output: Contribution to journalArticle (Academic Journal)peer-review


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 contributionCompleteness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions
Original languageEnglish
Pages (from-to)99-129
JournalJournal of Computer Security
Publication statusPublished - 2004

Bibliographical note

Other identifier: 2000660


Dive into the research topics of 'Completeness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions'. Together they form a unique fingerprint.

Cite this