Paper 2005/101 Original: eprint.iacr.org/2005/101 ↗

Soundness and Completeness of Formal Logics of Symmetric Encryption

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.