Skip to main content

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

Laurent Mazare, Bogdan Warinschi, Separating Trace Mapping and Reactive Simulatability Soundness: The Case of Adaptive Corruption. Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security - WITS-ARSPA. May 2009. No electronic version available.


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.

Bibtex entry.

Contact details

Publication Admin