Paper 2017/1152

Symbolic Security Criteria for Blockwise Adaptive Secure Modes of Encryption

Catherine Meadows


Symbolic methods for reasoning about the security of cryptographic systems have for some time concentrated mainly on protocols. More recently, however, we see a rising interest in the use of symbolic methods to reason about the security of algorithms as well, especially algorithms that are built by combining well-defined primitives. For this kind of application two things are generally required: the ability to reason about term algebras obeying equational theories at the symbolic level, and the ability to prove computational soundness and completeness of the symbolic model. It is often challenging to provide both these capabilities, especially for an adaptive adversary that can perform chosen plaintext or ciphertext attacks. In this paper we derive sound and complete symbolic criteria for computational security against adaptive chosen plaintext attacks of a class of modes of encryption. These apply to any scheduling policy used to send the cipher text, ranging from the messagewise schedule, in which ciphertext blocks are sent to the adversary only after all the plaintext blocks have been received, to the blockwise schedule, in which ciphertext blocks are sent as soon as they are computed. We also discuss how this approach could extended to larger classes of modes, and how could it be applied to the automatic synthesis of cryptosystems.

Note: It has come to my attention that there is a mistake in the proof of the main result in this paper, Theorem 7. The statement of Bellare's result on negligible functions is wrong, and the proof does not go through for the correct result. I am working on a correct version of this proof and will post a new version of the paper when it is ready.

Available format(s)
Publication info
Preprint. MINOR revision.
Modes of encryptionsymbolic analysis
Contact author(s)
catherine meadows @ nrl navy mil
2018-03-06: revised
2017-11-27: received
See all versions
Short URL
Creative Commons Attribution


      author = {Catherine Meadows},
      title = {Symbolic Security  Criteria for Blockwise Adaptive Secure Modes of Encryption},
      howpublished = {Cryptology ePrint Archive, Paper 2017/1152},
      year = {2017},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.