Computational Soundness of Symbolic Analysis for Protocols Using Hash Functions

DOI10.1016/j.entcs.2007.01.066zbMath1277.94026OpenAlexW1995008399MaRDI QIDQ2866733

Romain Janvier, Laurent Mazaré, Yassine Lakhneche

Publication date: 13 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.01.066

zbMATH Keywords

securitycomputational modelcryptographic protocolskeyed hash functionDolev-Yao modelprobabilistic encryptionformal encryption

Mathematics Subject Classification ID

Cryptography (94A60)

Related Items

Sound and complete computational interpretation of symbolic hashes in the standard model, A survey of symbolic methods in computational analysis of cryptographic systems

Uses Software

• HERMES
• AVISPA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An attack on the Needham-Schroeder public-key authentication protocol
• Probabilistic encryption
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Keying Hash Functions for Message Authentication
• On the security of public key protocols
• Programming Languages and Systems
• Programming Languages and Systems
• Computationally Sound Symbolic Secrecy in the Presence of Hash Functions
• Fast Software Encryption
• Computer Aided Verification
• Limits of the BRSIM/UC Soundness of Dolev-Yao Models with Hashes
• Theory of Cryptography