On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography

Abstract. The abstraction of cryptographic operations by term algebras, called DolevYao 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. This paper relates the two approaches for the ...

• Type: Conference
• Year: 2007
• Where: FSTTCS
• Authors: Michael Backes, Markus Dürmuth, Ralf Küsters
• Keywords: Dolev-Yao Models, FSTTCS 2007, Mapping Soundness, Soundness