Cryptology ePrint Archive: Report 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.
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 formats: PDF | BibTeX Citation
Version: 20050405:072645 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]