Programming language techniques for cryptographic proofs

DOI10.1007/978-3-642-14052-5_10MaRDI QIDQ5747645zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_10

Mathematics Subject Classification ID

Cryptography (94A60)

Recommendations

• Formal certification of code-based cryptographic proofs
• Formal Certification of ElGamal Encryption
• Computer-aided cryptographic proofs
• Computer-Aided Security Proofs for the Working Cryptographer
• Automated Security Proofs with Sequences of Games

Cited in

(6)

• Certifying assembly with formal security proofs: the case of BBS
• Formal Certification of ElGamal Encryption
• Beyond provable security verifiable IND-CCA security of OAEP
• Formal certification of code-based cryptographic proofs
• Verifiable security of Boneh-Franklin identity-based encryption
• Probabilistic functions and cryptographic oracles in higher order logic

Describes a project that uses

Uses Software

• CertiCrypt
• Coq

This page was built for publication: Programming language techniques for cryptographic proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747645)