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.
Category / Keywords: secret-key cryptography / modes of operation, synthesis Original Publication (with minor differences): 27th IEEE Computer Security Foundations Symposium, Vienna, Austria, July 19-22, 2014 Date: received 30 Sep 2014 Contact author: amaloz at cs umd edu Available format(s): PDF | BibTeX Citation Note: Full version of paper published at CSF 2014 Version: 20141001:060719 (All versions of this report) Short URL: ia.cr/2014/774 Discussion forum: Show discussion | Start new discussion