Tool-supported proofs of security protocols typically rely on abstractions from real cryptography by term algebras, so-called Dolev-Yao models. However, there was traditionally no cryptographic justification, i.e., no theorem that said what a proof with a Dolev-Yao abstraction implied for the real implementation, even if provably secure cryptographic primitives are used.
We show how to justify a Dolev-Yao style model under active attacks and in arbitrary protocol environments. The justification is done by defining an ideal system handling Dolev-Yao style terms and a cryptographic realization with the same user interface, and by showing that the realization is as secure as the ideal system in the sense of reactive simulatability. This definition encompasses arbitrary active attacks and enjoys general composition and property-preservation properties. Security holds in the standard model of cryptography and under standard assumptions of adaptively secure primitives.
The proof is a novel combination of a probabilistic, imperfect bisimulation with cryptographic reductions, a hybrid argument, and a static information-flow analysis.
Following the recent trend of proving formal methods abstractions of cryptography sound by means of simulatability proofs, we investigate the cryptographic soundness of symbolic XOR and symbolic hashes. We show, somewhat surprisingly, that hashes in their usual generality in Dolev-Yao models cannot be proven sound with respect to their cryptographic counterparts. For XOR we even show that no Dolev-Yao model can be proven sound with respect to any at least moderately natural realization of the XOR function. On the positive side, we show that XOR can be proven sound under passive attacks and that hash functions can be proven sound if we restrict their usage in specific and easily checkable way.