Deduction Soundness: Prove One, Get Five for Free

Florian Boehl 1 Véronique Cortier 2 Bogdan Warinschi 3
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Most computational soundness theorems deal with a limited number of primitives, thereby limiting their applicability. The notion of deduction soundness of Cortier and Warinschi (CCS'11) aims to facilitate soundness theorems for richer frameworks via composition results: deduction soundness can be extended, generically, with asymmetric encryption and public data structures. Unfortunately, that paper also hints at rather serious limitations regarding further composition results: composability with digital signatures seems to be precluded. 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 five 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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-00881023
Contributor : Véronique Cortier <>
Submitted on : Thursday, November 7, 2013 - 12:12:14 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM

Identifiers

Citation

Florian Boehl, Véronique Cortier, Bogdan Warinschi. Deduction Soundness: Prove One, Get Five for Free. CCS '13 - Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security - 2013, Nov 2013, Berlin, Germany. pp.1261-1272, ⟨10.1145/2508859.2516711⟩. ⟨hal-00881023⟩

Share

Metrics

Record views

406