Paper 2017/1152

Symbolic Security Criteria for Blockwise Adaptive Secure Modes of Encryption

Catherine Meadows

Abstract

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.