Cryptology ePrint Archive: Report 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)

Category / Keywords: foundations / Cryptographic Modes of Operations, Symbolic Security

Date: received 25 Jun 2020

Contact author: catherine meadows at nrl navy mil

Available format(s): PDF | BibTeX Citation

Version: 20200627:185437 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]