Formal certification of code-based cryptographic proofs
DOI10.1145/1480881.1480894zbMATH Open1315.68081OpenAlexW2011086847MaRDI QIDQ5261508FDOQ5261508
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 (45)
- Verifiable Security of Boneh-Franklin Identity-Based Encryption
- Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience
- Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
- Formalizing Probabilistic Noninterference
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
- Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
- A Machine-Checked Framework for Relational Separation Logic
- A Formalized Hierarchy of Probabilistic System Types
- Product programs and relational program logics
- Logical Formalisation and Analysis of the Mifare Classic Card in PVS
- 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
- Probabilistic Termination by Monadic Affine Sized Typing
- RHLE: modular deductive verification of relational \(\forall \exists\) properties
- CryptHOL: game-based proofs in higher-order logic
- The expectation monad in quantum foundations
- Dijkstra and Hoare monads in monadic computation
- 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
- EasyCrypt: A Tutorial
- Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
- 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
- ANF preserves dependent types up to extensional equality
- 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
- A Formalization of Polytime Functions
- The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
- Post-quantum verification of Fujisaki-Okamoto
- Beyond Provable Security Verifiable IND-CCA Security of OAEP
- 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)
