Cryptology ePrint Archive: Report 2007/233
On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography
Michael Backes and Markus Duermuth and Ralf Kuesters
Abstract: The abstraction of cryptographic operations by term algebras, called
Dolev-Yao models or symbolic cryptography, is essential in almost
all tool-supported methods for proving security protocols. Recently
significant progress was made -- using two conceptually different
approaches -- in proving that Dolev-Yao models can be sound with
respect to actual cryptographic realizations and security
definitions. One such approach is grounded on the notion of
simulatability, which constitutes a salient technique of Modern
Cryptography with a longstanding history for a variety of different
tasks. The other approach strives for the so-called mapping
soundness -- a more recent technique that is tailored to the
soundness of specific security properties in Dolev-Yao models, and
that can be established using more compact proofs. Typically, both
notions of soundness for similar Dolev-Yao models are established
separately in independent papers.
In this paper, the two approaches are related for the first time.
Our main result is that simulatability soundness entails mapping
soundness provided that both approaches use the same cryptographic
implementation. Interestingly, this result does not dependent on
details of the simulator, which translates between cryptographic
implementations and their Dolev-Yao abstractions in simulatability
soundness. Hence, future research may well concentrate on
simulatability soundness whenever applicable, and resort to mapping
soundness in those cases where simulatability soundness is too
strong a notion.
Category / Keywords: foundations / symbolic cryptography, simulatability, mapping soundness, Dolev-Yao
Date: received 14 Jun 2007
Contact author: duermuth at cs uni-sb de
Available format(s): PDF | BibTeX Citation
Version: 20070619:195302 (All versions of this report)
Short URL: ia.cr/2007/233
[ Cryptology ePrint archive ]