Paper 2007/233

On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography

Michael Backes, 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.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
symbolic cryptographysimulatabilitymapping soundnessDolev-Yao
Contact author(s)
duermuth @ cs uni-sb de
History
2007-06-19: received
Short URL
https://ia.cr/2007/233
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2007/233,
      author = {Michael Backes and Markus Duermuth and Ralf Kuesters},
      title = {On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography},
      howpublished = {Cryptology ePrint Archive, Paper 2007/233},
      year = {2007},
      note = {\url{https://eprint.iacr.org/2007/233}},
      url = {https://eprint.iacr.org/2007/233}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.