International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: Soundness and Completeness of Formal Logics of Symmetric Encryption

Gergei Bana
Search ePrint
Search Google
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.
  title={Soundness and Completeness of Formal Logics of Symmetric Encryption},
  booktitle={IACR Eprint archive},
  keywords={foundations / soundness, completeness, formal logics},
  note={PhD Dissertation, University of Pennsylvania, 2004 12877 received 3 Apr 2005},
  author={Gergei Bana},