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