Sciweavers

FSTTCS
2007
Springer

On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography

13 years 9 months ago
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 ...
Michael Backes, Markus Dürmuth, Ralf Küs
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FSTTCS
Authors Michael Backes, Markus Dürmuth, Ralf Küsters
Comments (0)