Computer-Aided Security Proofs for the Working Cryptographer
From MaRDI portal
Publication:5199185
DOI10.1007/978-3-642-22792-9_5zbMath1287.94048OpenAlexW2123991163MaRDI QIDQ5199185
Sylvain Heraud, Gilles Barthe, Santiago Zanella Béguelin, Benjamin Grégoire
Publication date: 12 August 2011
Published in: Advances in Cryptology – CRYPTO 2011 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22792-9_5
Applications of game theory (91A80) Cryptography (94A60) Data encryption (aspects in computer science) (68P25)
Related Items (22)
MoSS: modular security specifications framework ⋮ Automated proofs of block cipher modes of operation ⋮ Short variable length domain extenders with beyond birthday bound security ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ Monoidal computer. I: Basic computability by string diagrams ⋮ Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later ⋮ How to simulate it in Isabelle: towards formal proof for secure multi-party computation ⋮ Computer-Aided Verification for Mechanism Design ⋮ Authenticated confidential channel establishment and the security of TLS-DHE ⋮ Post-quantum verification of Fujisaki-Okamoto ⋮ State separation for code-based game-playing proofs ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory ⋮ Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC ⋮ Formalising \(\varSigma\)-protocols and commitment schemes using crypthol ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs ⋮ 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 ⋮ Formal security proofs with minimal fuss: implicit computational complexity at work
Uses Software
This page was built for publication: Computer-Aided Security Proofs for the Working Cryptographer
