Paper 2024/1880
Cryptography Experiments In Lean 4: SHA-3 Implementation
Abstract
In this paper we explain how we implemented the Secure Hash Algorithm-3 (SHA-3) family of functions in Lean 4, a functional programming language and theorem prover. We describe how we used several Lean facilities including type classes, dependent types, macros, and formal verification, and then refined the design to provide a simple one-shot and streaming API for hashing, and Extendable-output functions (XOFs), to reduce potential for misuse by users, and formally prove properties about the implementation.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- Lean 4SHA-3Keccak
- Contact author(s)
- gerald doussot @ nccgroup com
- History
- 2024-11-22: approved
- 2024-11-19: received
- See all versions
- Short URL
- https://ia.cr/2024/1880
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2024/1880,
author = {Gérald Doussot},
title = {Cryptography Experiments In Lean 4: {SHA}-3 Implementation},
howpublished = {Cryptology {ePrint} Archive, Paper 2024/1880},
year = {2024},
url = {https://eprint.iacr.org/2024/1880}
}
