Paper 2005/101
Soundness and Completeness of Formal Logics of Symmetric Encryption
Gergei Bana
Abstract
We consider expansions of the Abadi-Rogaway logic of indistinguishability of formal cryptographic expressions. The formal language of this logic uses a box as notation for indecipherable strings, through which formal equivalence is defined. We expand the logic by considering different kinds of boxes corresponding to equivalence classes of formal ciphers. We consider not only computational, but also purely probabilistic, information-theoretic interpretations. We present a general, systematic treatment of the expansions of the logic for symmetric encryption. We establish general soundness and completeness theorems for the interpretations. We also present applications to specific settings not covered in earlier works: a purely probabilistic one that interprets formal expressions in One-Time Pad, and computational settings of the so-called type 2 (which-key revealing) cryptosystems based on computational complexity.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Published elsewhere. PhD Dissertation, University of Pennsylvania, 2004
- Keywords
- soundnesscompletenessformal logics
- Contact author(s)
- bana @ math upenn edu
- History
- 2005-04-05: received
- Short URL
- https://ia.cr/2005/101
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2005/101,
author = {Gergei Bana},
title = {Soundness and Completeness of Formal Logics of Symmetric Encryption},
howpublished = {Cryptology ePrint Archive, Paper 2005/101},
year = {2005},
note = {\url{https://eprint.iacr.org/2005/101}},
url = {https://eprint.iacr.org/2005/101}
}
