Paper 2014/774

Automated Analysis and Synthesis of Block-Cipher Modes of Operation

Alex J. Malozemoff, Jonathan Katz, and Matthew D. Green


Block ciphers such as AES are deterministic, keyed functions that operate on small, fixed-size blocks. Block-cipher \emph{modes of operation} define a mechanism for probabilistic encryption of arbitrary length messages using any underlying block cipher. A mode of operation can be proven secure (say, against chosen-plaintext attacks) based on the assumption that the underlying block cipher is a pseudorandom function. Such proofs are complex and error-prone, however, and must be done from scratch whenever a new mode of operation is developed. We propose an \emph{automated} approach for the security analysis of block-cipher modes of operation based on a ``local'' analysis of the steps carried out by the mode when handling a \emph{single} message block. We model these steps as a directed, acyclic graph, with nodes corresponding to instructions and edges corresponding to intermediate values. We then introduce a set of \emph{labels} and \emph{constraints} on the edges, and prove a meta-theorem showing that any mode for which there exists a labeling of the edges satisfying these constraints is secure (against chosen-plaintext attacks). This allows us to reduce security of a given mode to a constraint-satisfaction problem, which in turn can be handled using an SMT solver. We couple our security-analysis tool with a routine that automatically generates viable modes; together, these allow us to synthesize hundreds of secure modes.

Note: Full version of paper published at CSF 2014

Available format(s)
Secret-key cryptography
Publication info
Published elsewhere. Minor revision. 27th IEEE Computer Security Foundations Symposium, Vienna, Austria, July 19-22, 2014
modes of operationsynthesis
Contact author(s)
amaloz @ cs umd edu
2014-10-01: received
Short URL
Creative Commons Attribution


      author = {Alex J.  Malozemoff and Jonathan Katz and Matthew D.  Green},
      title = {Automated Analysis and Synthesis of Block-Cipher Modes of Operation},
      howpublished = {Cryptology ePrint Archive, Paper 2014/774},
      year = {2014},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.