Pages that link to "Item:Q5261508"
From MaRDI portal
The following pages link to Formal certification of code-based cryptographic proofs (Q5261508):
Displaying 37 items.
- CertiCrypt (Q21426) (← links)
- The expectation monad in quantum foundations (Q320204) (← links)
- Certifying assembly with formal security proofs: the case of BBS (Q436406) (← links)
- Automated proofs for asymmetric encryption (Q540682) (← links)
- Dijkstra and Hoare monads in monadic computation (Q890377) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation (Q1687724) (← links)
- Strassen's theorem for quantum couplings (Q2007728) (← links)
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol (Q2031427) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
- A denotational semantics for low-level probabilistic programs with nondeterminism (Q2133180) (← links)
- CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (Q2331068) (← links)
- Formal security proofs with minimal fuss: implicit computational complexity at work (Q2343128) (← links)
- Product programs and relational program logics (Q2374302) (← links)
- Post-quantum verification of Fujisaki-Okamoto (Q2692346) (← links)
- Probabilistic Functions and Cryptographic Oracles in Higher Order Logic (Q2802495) (← links)
- Formalizing Probabilistic Noninterference (Q2938053) (← links)
- A Formalized Hierarchy of Probabilistic System Types (Q2945633) (← links)
- Probabilistic Termination by Monadic Affine Sized Typing (Q2988649) (← links)
- Beyond Provable Security Verifiable IND-CCA Security of OAEP (Q3073706) (← links)
- Logical Formalisation and Analysis of the Mifare Classic Card in PVS (Q3087992) (← links)
- A Formalization of Polytime Functions (Q3088001) (← links)
- Verifiable Security of Boneh-Franklin Identity-Based Encryption (Q3092349) (← links)
- A Machine-Checked Framework for Relational Separation Logic (Q3095237) (← links)
- Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience (Q3100218) (← links)
- The Computational SLR: A Logic for Reasoning about Computational Indistinguishability (Q3637209) (← links)
- A Calculus for Game-Based Security Proofs (Q4933210) (← links)
- ANF preserves dependent types up to extensional equality (Q5051989) (← links)
- (Q5155670) (← links)
- Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model (Q5195250) (← links)
- EasyCrypt: A Tutorial (Q5253588) (← links)
- Measure Transformer Semantics for Bayesian Machine Learning (Q5892490) (← links)
- Verified analysis of random binary tree structures (Q5919010) (← links)
- VPHL: a verified partial-correctness logic for probabilistic programs (Q5971408) (← links)
- Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving (Q6639734) (← links)