Sound and complete computational interpretation of symbolic hashes in the standard model

This paper provides one more step towards bridging the gap between the formal and computational approaches to the verification of cryptographic protocols. We extend the well-known Abadi–Rogaway logic with probabilistic hashes and give a precise semantic interpretation to it using Canetti’s oracle hashes. These are probabilistic polynomial-time hashes that hide all partial information. We show that, under appropriate conditions on the encryption scheme, this interpretation is computationally sound and complete. This can be used to port security results from the formal world to the computational world when considering passive adversaries. We also give an explicit example showing that oracle hashing is not strong enough to obtain such a result for active adversaries.