Verified cryptographic code for everybody

DOI10.1007/978-3-030-81685-8_31MaRDI QIDQ832216zbMATHOpenAlexFDO

Authors Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, A. Stefanescu

Publication date 25 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-81685-8_31

zbMATH Keywords

verificationcryptographyautomated reasoning

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Practical Formal Methods for Real World Cryptography (Invited Talk)
• scientific article; zbMATH DE number 7378548
• Computer-aided cryptographic proofs
• Formal certification of code-based cryptographic proofs
• Computer-Aided Security Proofs for the Working Cryptographer

Cites work

• Continuous reasoning: scaling the impact of formal methods
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(5)

• Certifying assembly with formal security proofs: the case of BBS
• Formalizing Coppersmith's method in Isabelle/HOL
• \textsc{CoqCryptoLine}: a verified model checker with certified results
• Certified verification for algebraic abstraction
• Verifying classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation

Describes a project that uses

Uses Software

• Boogie
• Toolchain
• CBMC
• ABC
• GitHub
• HACL*

This page was built for publication: Verified cryptographic code for everybody

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