Paper Info
Title
On simulatability soundness and mapping soundness of symbolic cryptography
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. This paper relates the two approaches for the first time. Our main result is that simulatability soundness entails mapping soundness provided that both approaches use the same cryptographic implementation. Hence, future research may well concentrate on simulatability soundness whenever applicable, and resort to mapping soundness in those cases where simulatability soundness constitutes too strong a notion.
Year
DOI
Venue
2007
10.1007/978-3-540-77050-3_9
IACR Cryptology ePrint Archive
Keywords
DocType
Volume
mapping soundness,cryptographic operation,similar dolev-yao model,dolev-yao model,security definition,cryptographic implementation,actual cryptographic realization,symbolic cryptography,so-called mapping soundness,security protocol,simulatability soundness
Conference
2007
ISSN
ISBN
Citations 
0302-9743
3-540-77049-6
7
PageRank 
References 
Authors
0.52
32
3
Name
Order
Citations
PageRank
Michael Backes12801163.28
Markus Dürmuth242325.28
Ralf Küsters3101469.62