Cryptology ePrint Archive: Report 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.

Category / Keywords: foundations / soundness, completeness, formal logics

Publication Info: PhD Dissertation, University of Pennsylvania, 2004

Date: received 3 Apr 2005

Contact author: bana at math upenn edu

Available format(s): PDF | BibTeX Citation

Version: 20050405:072645 (All versions of this report)

Short URL: ia.cr/2005/101

Discussion forum: Show discussion | Start new discussion