Probabilistic relational verification for cryptographic implementations

DOI10.1145/2535838.2535847MaRDI QIDQ5408416zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Cédric Fournet

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2535838.2535847

zbMATH Keywords

probabilistic programmingprogram logics

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 697830
• Probabilistic relational Hoare logics for computer-aided security proofs
• Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic
• Probabilistically checkable proofs and codes
• Logic for verifying public-key cryptographic protocols
• scientific article; zbMATH DE number 1962854
• scientific article; zbMATH DE number 7297874
• Verifying Cryptographic Protocols with Subterms Constraints
• The coinductive approach to verifying cryptographic protocols.
• scientific article; zbMATH DE number 1024091

Cited in

(18)

• Program synthesis for interactive-security systems
• Translation certification for smart contracts
• Modular verification of protocol equivalence in the presence of randomness
• CryptHOL: game-based proofs in higher-order logic
• Coupled relational symbolic execution for differential privacy
• Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
• Product programs and relational program logics
• Probabilistic functions and cryptographic oracles in higher order logic
• A formalized hierarchy of probabilistic system types. Proof pearl
• scientific article; zbMATH DE number 3877090 (Why is no real title available?)
• Relational Hash: Probabilistic Hash for Verifying Relations, Secure Against Forgery and More
• Automated type-based analysis of injective agreement in the presence of compromised principals
• scientific article; zbMATH DE number 7378548 (Why is no real title available?)
• Relational cost analysis in a functional-imperative setting
• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
• A higher-order language for Markov kernels and linear operators
• Toward automatic verification of quantum programs
• On iteration in discrete probabilistic programming

Describes a project that uses

Uses Software

• EasyCrypt
• Coq
• z3
• Ynot

This page was built for publication: Probabilistic relational verification for cryptographic implementations

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