Formal certification of code-based cryptographic proofs
From MaRDI portal
Recommendations
Cited in
(56)- CoSMed: a confidentiality-verified social media platform
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- Strassen's theorem for quantum couplings
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- A denotational semantics for low-level probabilistic programs with nondeterminism
- CertiCrypt
- CryptHOL: game-based proofs in higher-order logic
- Fifty years of Hoare's logic
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
- Formal security proofs with minimal fuss: implicit computational complexity at work
- Product programs and relational program logics
- Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic
- Post-quantum verification of Fujisaki-Okamoto
- Probabilistic functions and cryptographic oracles in higher order logic
- Computer-aided cryptographic proofs
- Formalizing probabilistic noninterference
- A formalized hierarchy of probabilistic system types. Proof pearl
- Probabilistic termination by monadic affine sized typing
- On the equality of probabilistic terms
- 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
- 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
- The expectation monad in quantum foundations
- Formal Proof of Provable Security by Game-Playing in a Proof Assistant
- A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
- Formal Certification of ElGamal Encryption
- The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
- Certifying assembly with formal security proofs: the case of BBS
- A Calculus for Game-Based Security Proofs
- ANF preserves dependent types up to extensional equality
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- Formalization in PVS of balancing properties necessary for proving security of the Dolev-Yao cascade protocol model
- EasyCrypt: a tutorial
- Automated proofs for asymmetric encryption
- A Formal Language for Cryptographic Pseudocode
- Programming language techniques for cryptographic proofs
- Automated Security Proofs with Sequences of Games
- Machine-checked security proofs of cryptographic signature schemes
- Measure transformer semantics for Bayesian machine learning
- Verified analysis of random binary tree structures
- VPHL: a verified partial-correctness logic for probabilistic programs
- RHLE: modular deductive verification of relational \(\forall \exists\) properties
- Does a Program Yield the Right Distribution?
- \textsc{CoqCryptoLine}: a verified model checker with certified results
- Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
- Exposure and hiding: approaching the objective probability and hiding the secret in zero-knowledge proof
- BiGKAT: an algebraic framework for relational verification of probabilistic programs
- Predicate abstraction for hyperliveness verification
- Quantum relational Hoare logic with expectations
- Formalizing the hidden number problem in Isabelle/HOL
- Verified cryptographic code for everybody
- Dijkstra and Hoare monads in monadic computation
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)
