Verified cryptographic code for everybody

DOI10.1007/978-3-030-81685-8_31MaRDI QIDQ832216zbMATH OpenOpenAlexFDO

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

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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)