In this paper we provide techniques for bypassing the perceived limitations of deduction soundness and demonstrate that it enjoys vastly improved composition properties. More precisely, we show that a deduction sound implementation can be modularly extended with all of the basic cryptographic primitives (symmetric/asymmetric encryption, message authentication codes, digital signatures, and hash functions). We thus obtain the first soundness framework that allows for the joint use of multiple instances of all of the basic primitives.
In addition, we show how to overcome an important restriction of the bare deduction soundness framework which forbids sending encrypted secret keys. In turn, this prevents its use for the analysis of a large class of interesting protocols (e.g. key exchange protocols). We allow for more liberal uses of keys as long as they are hidden in a sense that we also define. All primitives typically used to send secret data (symmetric/asymmetric encryption) satisfy our requirement which we also show to be preserved under composition.
Category / Keywords: foundations / computational soundness, composability Original Publication (with major differences): Proc. ACM CCS 2013, to appear. Date: received 23 Jul 2013 Contact author: florian boehl at kit edu Available format(s): PDF | BibTeX Citation Version: 20130727:011225 (All versions of this report) Short URL: ia.cr/2013/457 Discussion forum: Show discussion | Start new discussion