Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic

DOI10.1016/J.SCICO.2008.09.006MaRDI QIDQ2517836zbMATH OpenOpenAlexFDO

Authors Jerry den Hartog

Publication date 9 January 2009

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2008.09.006

zbMATH Keywords

axiomatizationcryptographyHoare logicprobabilityprovable correctness

Mathematics Subject Classification ID

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

Recommendations

• A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
• Formal certification of code-based cryptographic proofs
• Probabilistic relational Hoare logics for computer-aided security proofs
• scientific article; zbMATH DE number 697830
• Computer-aided cryptographic proofs

Cited in

(6)

• Probabilistic functions and cryptographic oracles in higher order logic
• Probabilistic relational Hoare logics for computer-aided security proofs
• A Randomized Algorithm for BBCSPs in the Prover-Verifier Model
• A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
• Functional Correctness Proofs of Encryption Algorithms
• Probabilistic relational verification for cryptographic implementations

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic

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