Computer-Aided Security Proofs for the Working Cryptographer
From MaRDI portal
Recommendations
- Computer-aided cryptographic proofs
- Programming Languages and Systems
- scientific article; zbMATH DE number 1982609
- scientific article; zbMATH DE number 17388
- scientific article; zbMATH DE number 2048525
- scientific article; zbMATH DE number 1962854
- Fundamental problems in provable security and cryptography
Cited in
(40)- Short variable length domain extenders with beyond birthday bound security
- Finding a middle ground for computer-aided cryptography
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- Authenticated confidential channel establishment and the security of TLS-DHE
- State separation for code-based game-playing proofs
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
- MoSS: modular security specifications framework
- CryptHOL: game-based proofs in higher-order logic
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
- Formal security proofs with minimal fuss: implicit computational complexity at work
- Proof producing synthesis of arithmetic and cryptographic hardware
- Post-quantum verification of Fujisaki-Okamoto
- Proof techniques for cryptographic processes
- Probabilistic functions and cryptographic oracles in higher order logic
- Automated proofs of block cipher modes of operation
- Probabilistic relational Hoare logics for computer-aided security proofs
- Computer-aided cryptographic proofs
- Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later
- Computer-aided verification for mechanism design
- Probabilistic termination by monadic affine sized typing
- Another look at automated theorem-proving. II
- Formal Certification of ElGamal Encryption
- Monoidal computer. I: Basic computability by string diagrams
- Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC
- Formalization in PVS of balancing properties necessary for proving security of the Dolev-Yao cascade protocol model
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- EasyCrypt: a tutorial
- Programming Languages and Systems
- A “proof-reading” of Some Issues in Cryptography
- Another look at automated theorem-proving
- Programming language techniques for cryptographic proofs
- VPHL: a verified partial-correctness logic for probabilistic programs
- Formalizing Coppersmith's method in Isabelle/HOL
- Formally verifying Kyber. Episode V: machine-checked IND-CCA security and correctness of ML-KEM in Easycrypt
- How hard can it be to formalize a proof? Lessons from formalizing \texttt{CryptoBox} three times in EasyCrypt
- A tight security proof for SPHINCS\textsuperscript{+}, formally verified
- Quantum relational Hoare logic with expectations
- Propositional logics of overwhelming truth
- Verified cryptographic code for everybody
This page was built for publication: Computer-Aided Security Proofs for the Working Cryptographer
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5199185)
