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

Cryptography (94A60) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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