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