Paper 2011/564

Private-key Symbolic Encryption

N. Ahmed, C. D. Jensen, and E. Zenner

Abstract

Symbolic encryption, in the style of Dolev-Yao models, is ubiquitous in formal security analysis aiming at the automated verification of network protocols. The naive use of symbolic encryption, however, may unnecessarily require an expensive construction: an arbitrary-length encryption scheme that is private and non-malleable in an adaptive CCA-CPA setting. Most of the time, such assumptions remain hidden and rather symbolic encryption is instantiated with a seemingly ``good'' cryptographic encryption, such as AES in the CBC configuration. As an illustration of this problem, we first report new attacks on ECB and CBC based implementations of the well-known Needham-Schroeder and Denning-Sacco protocols. We then present a few symbolic encryption schemes along with their cryptographic semantics, and prove the hierarchical relations between the proposed schemes from both cryptographic and formal perspectives. These symbolic schemes can be seamlessly used in many existing formal security models.

Note: Revision: Removed a latex tag from the abstract.

Metadata
Available format(s)
PDF PS
Publication info
Published elsewhere. Unknown where it was published
Keywords
Symbolic EncryptionHidden AssumptionsFormal Security Model
Contact author(s)
naah @ imm dtu dk
History
2011-10-22: received
Short URL
https://ia.cr/2011/564
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2011/564,
      author = {N.  Ahmed and C. D.  Jensen and E.  Zenner},
      title = {Private-key Symbolic Encryption},
      howpublished = {Cryptology ePrint Archive, Paper 2011/564},
      year = {2011},
      note = {\url{https://eprint.iacr.org/2011/564}},
      url = {https://eprint.iacr.org/2011/564}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.