Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience

DOI10.1007/978-3-642-25379-9_27zbMath1350.68229OpenAlexW2162571320MaRDI QIDQ3100218

Mathilde Duclos, Pierre Corbineau, Yassine Lakhneche

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_27

zbMATH Keywords

formal verificationcomputational modelprovable cryptographysecurity protocolintrusion resilience

Mathematics Subject Classification ID

Uses Software

• Coq

Cites Work

• Unnamed Item
• A survey of symbolic methods in computational analysis of cryptographic systems
• Proofs of randomized algorithms in Coq
• Conditionally-perfect secrecy and a provably-secure randomized cipher
• Optimal randomizer efficiency in the bounded-storage model
• Logics for reasoning about cryptographic constructions
• Leakage Resilient ElGamal Encryption
• Interacting with Modal Logics in the Coq Proof Assistant
• Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems
• Survey: Leakage Resilience and the Bounded Retrieval Model
• Formal certification of code-based cryptographic proofs
• Theory of Cryptography
• Theory of Cryptography

This page was built for publication: Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience