A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs

DOI10.1007/11787006_22MaRDI QIDQ3591439zbMATH OpenOpenAlexFDO

Authors Ricardo Corin, Jerry den Hartog

Publication date 11 September 2007

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11787006_22

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Recommendations

• Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic
• CryptHOL: game-based proofs in higher-order logic
• A Calculus for Game-Based Security Proofs
• Formal certification of code-based cryptographic proofs
• A Formal Language for Cryptographic Pseudocode

Cited in

(14)

• CryptHOL: game-based proofs in higher-order logic
• Formalisation of probabilistic concealment
• Formal security proofs with minimal fuss: implicit computational complexity at work
• Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic
• Probabilistic functions and cryptographic oracles in higher order logic
• Probabilistic relational Hoare logics for computer-aided security proofs
• The computational SLR: a logic for reasoning about computational indistinguishability
• Formal Proof of Provable Security by Game-Playing in a Proof Assistant
• The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
• A Calculus for Game-Based Security Proofs
• Automated proofs for asymmetric encryption
• Automated proofs for asymmetric encryption
• A Formal Language for Cryptographic Pseudocode
• Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties

This page was built for publication: A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs

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