Probabilistic relational Hoare logics for computer-aided security proofs

DOI10.1007/978-3-642-31113-0_1MaRDI QIDQ2908554zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin

Publication date 5 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00765864/file/main.pdf

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
• Computer-aided cryptographic proofs
• Computer-Aided Security Proofs for the Working Cryptographer
• Probabilistic annotations for protocol models. Dedicated to Joshua Guttman
• Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic

Cited in

(8)

• A relation-algebraic approach to the ``Hoare logic of functional dependencies
• Logics for reasoning about cryptographic constructions
• On counting propositional logic and Wagner's hierarchy
• Certified security proofs of cryptographic protocols in the computational model: an application to intrusion resilience
• Probabilistic relational verification for cryptographic implementations
• Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic
• EasyCrypt: a tutorial
• scientific article; zbMATH DE number 5714261 (Why is no real title available?)

Describes a project that uses

Uses Software

• EasyCrypt

This page was built for publication: Probabilistic relational Hoare logics for computer-aided security proofs

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