Cryptology ePrint Archive: Report 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.

Category / Keywords: foundations / hash functions, formal methods, formal hashes, Dolev-Yao, soundness

Publication Info: in submission

Date: received 13 Jan 2006, last revised 21 Nov 2011

Contact author: flaviog at cs ru nl

Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation

Version: 20111121:181527 (All versions of this report)

Short URL: ia.cr/2006/014

Discussion forum: Show discussion | Start new discussion