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
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 (39)
- 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
- Automated proofs for asymmetric encryption
- 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
- 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
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- 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
- 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)
