Computational Soundness for Interactive Primitives
We present a generic computational soundness result for interactive cryptographic primitives. Our abstraction of interactive primitives leverages the Universal Composability (UC) framework, and thereby offers strong composability properties for our comput
- PDF / 856,625 Bytes
- 21 Pages / 439.37 x 666.142 pts Page_size
- 72 Downloads / 187 Views
bstract. We present a generic computational soundness result for interactive cryptographic primitives. Our abstraction of interactive primitives leverages the Universal Composability (UC) framework, and thereby offers strong composability properties for our computational soundness result: given a computationally sound Dolev-Yao model for non-interactive primitives, and given UC-secure interactive primitives, we obtain computational soundness for the combined model that encompasses both the non-interactive and the interactive primitives. Our generic result is formulated in the CoSP framework for computational soundness proofs and supports any equivalence property expressible in CoSP such as strong secrecy and anonymity. In a case study, we extend an existing computational soundness result by UC-secure blind signatures. We obtain computational soundness for blind signatures in uniform bi-processes in the applied π-calculus. This enables us to verify the untraceability of Chaum’s payment protocol in ProVerif in a computationally sound manner.
1
Introduction
Manual security analyses of cryptographic protocols are complex and errorprone. As a result, various automated verification techniques have been developed based on so-called Dolev-Yao models, which abstract cryptographic operations as symbolic terms obeying simple cancellation rules [12,26,35,36,38,40]. Numerous verification tools such as ProVerif [12] and APTE [26] are capable of reasoning about equivalence properties, e.g., strong secrecy and anonymity. A wide range of these Dolev-Yao models is computationally sound, i.e., the security of a symbolically abstracted protocol entails the security of a suitable cryptographic realization [3,7,14,20,27,29,31,50,52]. However, virtually all of these computational soundness results are inherently restricted to noninteractive primitives such as encryption and signatures. In contrast, interactive cryptographic primitives such as interactive zeroknowledge proofs [43], forward-secure key exchange [37], and blind signatures [25], have gained tremendous attention in the scientific community and widespread deployment in real systems. The security of interactive primitives is often defined and established in the Universal Composability (UC) framework [17] or similar frameworks [8,44,48], c Springer International Publishing Switzerland 2015 G. Pernul et al. (Eds.): ESORICS 2015, Part I, LNCS 9326, pp. 125–145, 2015. DOI: 10.1007/978-3-319-24174-6 7
126
M. Backes et al.
which allow to prove strong security guarantees in a composable manner [23,24,41]. In such frameworks, a primitive is secure if its execution is indistinguishable from a setting in which all parties have a private connection to an imaginary trusted machine, called ideal functionality, which performs the desired task locally and in a trustworthy manner. For interactive primitives, ideal functionalities are a suitable abstraction, but for non-interactive primitives, DY-style abstractions have two significant advantages compared to a corresponding abstraction as an id
Data Loading...
