Affiliations: [a] SQIG – Instituto de Telecomunicações and IST, TU Lisbon, Portugal. E-mail: pedro.adao@ist.utl.pt | [b] Department of Computer Science, UC Davis, USA. E-mail: gebana@cs.ucdavis.edu | [c] The Naval Postgraduate School, Monterey, CA, USA. E-mail: jcherzog@nps.edu | [d] Department of Mathematics, University of Pennsylvania, Philadelphia, PA, USA. E-mail: scedrov@math.upenn.edu
Correspondence:
[*]
Corresponding author.
Note: [1] Partially supported by FCT grant SFRH/BD/8148/2002. Additional support from FEDER/FCT projects QuantLog POCI/MAT/55796/2004, QSec PTDC/EIA/67661/2006 and KLog PTDC/MAT/68723/2006.
Note: [3] Partially supported by OSD/ONR CIP/SW URI “Software Quality and Infrastructure Protection for Diffuse Computing” through ONR Grant N00014-01-1-0795. Additional support from NSF Grant CNS-0429689. Additional support from the Packard Fellowship. Part of this work was done while the author was affiliated with University of Pennsylvania, Department of Mathematics.
Note: [3] Partially supported by OSD/ONR CIP/SW URI “Software Quality and Infrastructure Protection for Diffuse Computing” through ONR Grant N00014-01-1-0795 and OSD/ONR CIP/SW URI “Trustworthy Infrastructure, Mechanisms, and Experimentation for Diffuse Computing” through ONR Grant N00014-04-1-0725. Additional support from NSF Grants CCR-0098096 and CNS-0429689.
Abstract: In their seminal work, Abadi and Rogaway show that the formal (Dolev–Yao) notion of indistinguishability is sound with respect to the computational model: messages that are indistinguishable in the formal model become indistinguishable messages in the computational model. However, this result leaves two problems unsolved. First, it cannot tolerate key cycles. Second, it makes the too-strong assumption that the underlying cryptography hides all aspects of the plaintext, including its length. In this paper we extend their work in order to address these problems. We show that the recently-introduced notion of KDM-security can provide soundness even in the presence of key cycles. For this, we have to consider encryption that reveals the length of plaintexts, which we use to motivate a general examination information-leaking encryption. In particular, we consider the conditions under which an encryption scheme that may leak some partial information will provide soundness and completeness to some (possibly weakened) version of the formal model.
