Soundness and Completeness of Formal Encryption: the Cases of Key-Cycles and Partial Information Leakage (joint work with Gergei Bana, Jonathan Herzog and Andre Scedrov)
Journal of Computer Security, 17(5):737--797, 2009. © IOS Press.

Abstract: In their seminal work, Abadi and Rogaway (see Abadi and Rogaway, Journal of Cryptology, 15(2)) show that the formal (Dolev-Yao) notion of indistinguishability is \emph{sound} with respect to the computational model: pairs of messages that are indistinguishable in the formal model become indistinguishable messages in the computational model. However, this result has two weaknesses. First, it cannot tolerate key-cycles. Second, it makes the too-strong assumption that the underlying cryptography can hide all aspects of the plaintext, including its length. Both of these weaknesses stem from a 'gap' between the formal and computational models, and we consider and close both weaknesses in this paper. We show that the recently-introduced notion of KDM-security can provide soundness even in the presence of key-cycles, which is the first time a gap has been closed by strengthening the computational model. We then consider encryption that reveals the length of plaintexts, and use this to motivate a general examination information-leaking encryption. In particular, we consider the conditions under which an encryption scheme, which may leak some partial information, will provide soundness and completeness to some (possibly weakened) version of the formal model.

Date: 05 November 2005, last revised 19 January 2009.

Get a preprint: PDF | PS | BibTeX Citation.
Get it from the publisher's website.