Computational Soundness of Symbolic Analysis for Protocols Using Hash Functions

In this paper, we consider a Dolev-Yao model with hash functions and establish its soundness with respect to the computational model. Soundness means that the absence of attacks in the Dolev-Yao model implies that the probability for an adversary to perform an attack in the computational model is negligible. Classical requirements for deterministic hash functions (e.g. one-wayness, collision freeness) are not sufficient for proving this result. Therefore we introduce new security requirements that are sufficient to prove the soundness result and that are verified by random oracles.