Abstract | ||
---|---|---|
Block ciphers such as AES are deterministic, keyed functions that operate on small, fixed-size blocks. Block-cipher 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 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 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 labels and 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. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1109/CSF.2014.18 | Computer Security Foundations Symposium |
Keywords | DocType | Volume |
symmetric-key encryption, modes of operation, program synthesis,pseudorandom function,constraint satisfaction problems,probabilistic encryption,proofs,aes,probability,labeling,constraint satisfaction problem,symmetric key encryption,block cipher modes of operation,cryptography,directed acyclic graph,encryption,law,smt solver,directed graphs | Journal | 2014 |
ISSN | Citations | PageRank |
1063-6900 | 42 | 1.37 |
References | Authors | |
29 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Alex J. Malozemoff | 1 | 158 | 8.98 |
Jonathan Katz | 2 | 7579 | 347.97 |
Matthew Green | 3 | 2007 | 114.98 |