Sound Computational Interpretation of Symbolic Hashes in the Standard Model

Flavio D.  Garcia; Peter van Rossum

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

BibTeX

@misc{cryptoeprint:2006/014,
      author = {Flavio D.  Garcia and Peter van Rossum},
      title = {Sound Computational Interpretation of Symbolic Hashes in the Standard Model},
      howpublished = {Cryptology {ePrint} Archive, Paper 2006/014},
      year = {2006},
      url = {https://eprint.iacr.org/2006/014}
}