Computational soundness of symbolic analysis for protocols using hash functions

DOI10.1016/J.ENTCS.2007.01.066MaRDI QIDQ2866733zbMATH OpenOpenAlexFDO

Authors Romain Janvier, Laurent Mazaré, Yassine Lakhnech

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

computational modelcryptographic protocolsDolev-Yao modelformal encryptionkeyed hash functionprobabilistic encryptionsecurity

Mathematics Subject Classification ID

Cryptography (94A60)

Recommendations

• Computationally Sound Symbolic Secrecy in the Presence of Hash Functions
• Limits of the BRSIM/UC soundness of Dolev-Yao models with hashes
• Computational soundness of indistinguishability properties without computable parsing
• A survey of symbolic methods in computational analysis of cryptographic systems
• Sound and complete computational interpretation of symbolic hashes in the standard model

Cites work

• An attack on the Needham-Schroeder public-key authentication protocol
• Computationally Sound Symbolic Secrecy in the Presence of Hash Functions
• Computer Aided Verification
• Fast Software Encryption
• scientific article; zbMATH DE number 5009203 (Why is no real title available?)
• scientific article; zbMATH DE number 1088253 (Why is no real title available?)
• scientific article; zbMATH DE number 1759457 (Why is no real title available?)
• scientific article; zbMATH DE number 1832234 (Why is no real title available?)
• Keying hash functions for message authentication
• Limits of the BRSIM/UC soundness of Dolev-Yao models with hashes
• On the security of public key protocols
• Probabilistic encryption
• Programming Languages and Systems
• Programming Languages and Systems
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Theory of Cryptography

Cited in

(13)

• Moving the bar on computationally sound exclusive-or
• Symbolic analysis of identity-based protocols
• Sound and complete computational interpretation of symbolic hashes in the standard model
• Towards unconditional soundness: computationally complete symbolic attacker
• Computational soundness of indistinguishability properties without computable parsing
• Computational soundness of asymmetric bilinear pairing-based protocols
• Computational soundness for interactive primitives
• Computational soundness of symbolic zero-knowledge proofs: weaker assumptions and mechanized verification
• Computationally Sound Symbolic Secrecy in the Presence of Hash Functions
• A survey of symbolic methods in computational analysis of cryptographic systems
• On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography
• Computationally Sound Symbolic Analysis of Probabilistic Protocols with Ideal Setups
• Limits of the BRSIM/UC soundness of Dolev-Yao models with hashes

Describes a project that uses

Uses Software

• HERMES
• AVISPA

This page was built for publication: Computational soundness of symbolic analysis for protocols using hash functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2866733)