B.: A composable computational soundness notion

Computational soundness results show that under certain conditions it is possible to conclude computational secu-rity whenever symbolic security holds. Unfortunately, each soundness result is usually established for some set of cryp-tographic primitives and extending the result to encompass new primitives typically requires redoing most of the work. In this paper we suggest a way of getting around this prob-lem. We propose a notion of computational soundness that we term deduction soundness. As for other soundness notions, our definition captures the idea that a computational adver-sary does not have any more power than a symbolic adver-sary. However, a key aspect of deduction soundness is that it considers, intrinsically, the use of the primitives in the presence of functions specified by the adversary. As a conse-quence, the resulting notion is amenable to modular exten-sions. We prove that a deduction sound implementation of some arbitrary primitives can be extended to include asym-metric encryption and public data-structures (e.g. pairings or list), without repeating the original proof effort. Furthermore, our notion of soundness concerns crypto-graphic primitives in a way that is independent of any pro-tocol specification language. Nonetheless, we show that de-duction soundness leads to computational soundness for lan-guages (or protocols) that satisfy a so called commutation property