Sound Computational Interpretation of Symbolic Hashes in the Standard Model

You are looking at a specific version 20111121:181527 of this paper. See the latest version.

Paper 2006/014

Sound Computational Interpretation of Symbolic Hashes in the Standard Model

Flavio D. Garcia and Peter van Rossum

Abstract

This paper provides one more step towards bridging the gap between the formal and computational approaches to cryptographic protocols. We extend the well-known Abadi-Rogaway logic with probabilistic hashes and we give precise semantic to it using Canetti's oracle hashing. Finally, we show that this interpretation is computationally sound.

Metadata

Available format(s): PDF PS
Category: Foundations
Publication info: Published elsewhere. in submission
Keywords: hash functions formal methods formal hashes Dolev-Yao soundness
Contact author(s): flaviog @ cs ru nl
History: 2011-11-21: revised; 2006-01-17: received; See all versions
Short URL: https://ia.cr/2006/014
License: CC BY