Formal certification of code-based cryptographic proofs
DOI10.1145/1480881.1480894zbMATH Open1315.68081OpenAlexW2011086847MaRDI QIDQ5261508FDOQ5261508
Authors: Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin 
Publication date: 3 July 2015
Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1480881.1480894
Recommendations
observational equivalenceprogram transformationsCoq proof assistantcryptographic proofsrelational Hoare logic
Cryptography (94A60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cited In (51)
- Verified cryptographic code for everybody
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
- Probabilistic termination by monadic affine sized typing
- Product programs and relational program logics
- Strassen's theorem for quantum couplings
- Fifty years of Hoare's logic
- Certifying assembly with formal security proofs: the case of BBS
- A Formal Language for Cryptographic Pseudocode
- Automated proofs for asymmetric encryption
- Automated Security Proofs with Sequences of Games
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
- RHLE: modular deductive verification of relational \(\forall \exists\) properties
- CryptHOL: game-based proofs in higher-order logic
- The expectation monad in quantum foundations
- A formalization of polytime functions
- Dijkstra and Hoare monads in monadic computation
- Computer-aided cryptographic proofs
- Formalization in PVS of balancing properties necessary for proving security of the Dolev-Yao cascade protocol model
- CoSMed: a confidentiality-verified social media platform
- Formal Certification of ElGamal Encryption
- Title not available (Why is that?)
- A Calculus for Game-Based Security Proofs
- CertiCrypt
- Formal security proofs with minimal fuss: implicit computational complexity at work
- Verified analysis of random binary tree structures
- On the equality of probabilistic terms
- Beyond provable security verifiable IND-CCA security of OAEP
- Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
- Machine-checked security proofs of cryptographic signature schemes
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- Does a Program Yield the Right Distribution?
- VPHL: a verified partial-correctness logic for probabilistic programs
- Verifiable security of Boneh-Franklin identity-based encryption
- ANF preserves dependent types up to extensional equality
- Certified security proofs of cryptographic protocols in the computational model: an application to intrusion resilience
- A denotational semantics for low-level probabilistic programs with nondeterminism
- Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
- Formalizing probabilistic noninterference
- Probabilistic functions and cryptographic oracles in higher order logic
- The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
- Post-quantum verification of Fujisaki-Okamoto
- A machine-checked framework for relational separation logic
- Programming language techniques for cryptographic proofs
- \textsc{CoqCryptoLine}: a verified model checker with certified results
- Logical formalisation and analysis of the Mifare Classic card in PVS
- EasyCrypt: a tutorial
- A formalized hierarchy of probabilistic system types. Proof pearl
- Formal Proof of Provable Security by Game-Playing in a Proof Assistant
- Measure transformer semantics for Bayesian machine learning
Uses Software
This page was built for publication: Formal certification of code-based cryptographic proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261508)
