Automated Analysis and Synthesis of Block-Cipher Modes of Operation

ABSTRACT. Block cipher modes of operation provide a mechanism for encrypting arbitrary length messages based on block ciphers having some fixed (small) block size. Existing techniques for proving modes secure under standard security definitions require analyzing the global behavior of the mode. We propose a new approach which requires only \emph{local} analysis of a single block. As part of our approach, we model modes of operations as graphs, and specify a set of type-inference rules over the edges of the graph. This allows us to reduce the question of security (against chosen-plaintext attacks) for some mode to the question of whether the graph has a consistent type assignment, which in turn can be reduced to a question of boolean satisfiability. We couple this security-analysis tool with a synthesizer that automatically generates viable modes using an SMT solver.