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: This work was presented at the presentation-only workshop Foundations of Computer Security in August 2017. The algorithm described in Section 7 was presented at the UNIF workshop in September 2017 and is posted online at the workshop website. I am assuming neither of those count as previous publications.