Paper 2020/794

Symbolic and Computational Reasoning About Cryptographic Modes of Operation

Catherine Meadows

Abstract

In this paper we develop symbolic and computational representations for a class of cryptographic modes of operation, where the symbolic representations are modeled as elements of a term algebra, and we apply them to the analysis of the computational security of the modes. We derive two different conditions on the symbolic representations, a simple one that is sufficient for security, and a more complex one that is both necessary and sufficient, and prove that these properties hold. The problem of deciding computational security then is reduced to the problem of solving certain disunification problems. We also discuss how these results can be extended. This paper subsumes and replaces the paper ``Symbolic Security Criteria for Blockwise Adaptive Secure Modes of Encryption." (IACR eprint 2017/1152)