CryptoDB
Soundness and Completeness of Formal Logics of Symmetric Encryption
Authors: | |
---|---|
Download: | |
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. |
BibTeX
@misc{eprint-2005-12437, title={Soundness and Completeness of Formal Logics of Symmetric Encryption}, booktitle={IACR Eprint archive}, keywords={foundations / soundness, completeness, formal logics}, url={http://eprint.iacr.org/2005/101}, note={PhD Dissertation, University of Pennsylvania, 2004 bana@math.upenn.edu 12877 received 3 Apr 2005}, author={Gergei Bana}, year=2005 }