Separating Trace Mapping and Reactive Simulatability Soundness: The Case of Adaptive Corruption

摘要

Computational soundness is the research direction that aims to translate security guarantees with respect to Dolev-Yao models into guarantees with resepect to the stronger computational models of modern cryptography. There are essentially two different approaches that aim to achieve computational soundness. One approach is based on the so-called trace mapping theorems, and one based on reactive simulatability. In a recent paper, Backes, Duerthmuth, and Kiisters have shown that the stronger requirements needed for reactive simulatability-based soundness imply that a trace mapping theorem also holds. It was left as an open problem whether there exists interesting settings where the simulatability framework breaks down but mapping theorems still exist.rnIn this paper we describe one such setting, and thus give a separation between the two frameworks. Specifically, we show that adaptive corruption of symmetric encryption keys (a problematic setting for simulation-based frameworks) can be smoothly treated in a mapping theorem-based soundness framework.rnA crucial ingredient of our proof, and a result of independent interest, is a new (indistinguishability based) security notion for encryption. The central feature of our definition is that in addition to standard chosen-ciphertext attacks in multi-user settings, it also directly accounts for adaptive corruption of decryption keys. We show that our notion satisfies the intuitively appealing property that it is equivalent to standard security requirements on encryption.