Computational and information-theoretic soundness and completeness of formal encryption

We consider expansions of the Abadi-Rogaway logic of indistinguishability of formal cryptographic expressions. We expand the logic in order to cover cases when par-tial information of the encrypted plaintext is revealed. 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 gen-eral soundness and completeness theorems for the inter-pretations. We also present applications to specific set-tings not covered in earlier works: a purely probabilistic one based on One-Time Pad, and computational settings of the so-called type-2 (which-key revealing) and type-3 (which-key and length revealing) encryption schemes based on computational complexity