Formal certification of code-based cryptographic proofs

DOI10.1145/1480881.1480894zbMath1315.68081OpenAlexW2011086847MaRDI QIDQ5261508

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

zbMATH Keywords

program transformationsobservational equivalenceCoq proof assistantcryptographic proofsrelational Hoare logic

Mathematics Subject Classification ID

Related Items (37)

A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Product programs and relational program logics ⋮ ANF preserves dependent types up to extensional equality ⋮ The expectation monad in quantum foundations ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Formalizing Probabilistic Noninterference ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ Dijkstra and Hoare monads in monadic computation ⋮ How to simulate it in Isabelle: towards formal proof for secure multi-party computation ⋮ RHLE: modular deductive verification of relational \(\forall \exists\) properties ⋮ Post-quantum verification of Fujisaki-Okamoto ⋮ Certifying assembly with formal security proofs: the case of BBS ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ Automated proofs for asymmetric encryption ⋮ Strassen's theorem for quantum couplings ⋮ A Calculus for Game-Based Security Proofs ⋮ Fifty years of Hoare's logic ⋮ Formalising \(\varSigma\)-protocols and commitment schemes using crypthol ⋮ Verified analysis of random binary tree structures ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ Measure Transformer Semantics for Bayesian Machine Learning ⋮ Beyond Provable Security Verifiable IND-CCA Security of OAEP ⋮ Logical Formalisation and Analysis of the Mifare Classic Card in PVS ⋮ A Formalization of Polytime Functions ⋮ The Computational SLR: A Logic for Reasoning about Computational Indistinguishability ⋮ CertiCrypt ⋮ Verifiable Security of Boneh-Franklin Identity-Based Encryption ⋮ A Machine-Checked Framework for Relational Separation Logic ⋮ Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience ⋮ Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs ⋮ Unnamed Item ⋮ Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model ⋮ EasyCrypt: A Tutorial ⋮ Formal security proofs with minimal fuss: implicit computational complexity at work ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory

Uses Software

• Coq

This page was built for publication: Formal certification of code-based cryptographic proofs