Computational soundness is an important research direction that aims to translate security guarantees obtained using the Dolev-Yao models t o guarantees in the stronger computational models of modern cryptography. Two different approaches have been developed to achieve computational soundness, one based on the so-called trace mapping theorems, and one based on reactive simulatability. Recently, Backes, D\"urthmuth, and K\"usters have shown that the stronger requirements needed for reactive simulatability-based soundness i mply that a trace mapping theorem also holds. It was left as an open problem whether there exists interesting settings where the simulatab ility framework breaks down but mapping theorems still exist.
In this paper we describe one such setting, and thus give a separation between the two frameworks. Specifically, we show that adaptive cor ruption of symmetric encryption keys (a problematic setting for simulation-based frameworks) can be smoothly treated in a mapping theorem-b ased soundness framework.
A 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.