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.
Note: Corrects some typos and clarifies some issues from the previous version.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Preprint. MAJOR revision.
- Keywords
- Cryptographic Modes of OperationsSymbolic Security
- Contact author(s)
- catherine meadows @ nrl navy mil
- History
- 2020-09-08: last of 3 revisions
- 2020-06-27: received
- See all versions
- Short URL
- https://ia.cr/2020/794
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2020/794,
author = {Catherine Meadows},
title = {Symbolic and Computational Reasoning About Cryptographic Modes of Operation},
howpublished = {Cryptology ePrint Archive, Paper 2020/794},
year = {2020},
note = {\url{https://eprint.iacr.org/2020/794}},
url = {https://eprint.iacr.org/2020/794}
}
