Paper 2023/087
Verification of Correctness and Security Properties for CRYSTALS-KYBER
Abstract
Since the post-quantum crypto system CRYSTALS-KYBER has been chosen for standardization by the National Institute for Standards and Technology (US), a formal verification of its correctness and security properties becomes even more relevant.
Using the automated theorem prover Isabelle, we are able to formalize the algorithm specifications and parameter sets of Kyber's public key encryption scheme and verify the
Metadata
- Available format(s)
-
PDF
- Category
- Public-key cryptography
- Publication info
- Preprint.
- Keywords
- post-quantum cryptographyKybersecurityverificationIsabelle
- Contact author(s)
- k kreuzer @ tum de
- History
- 2024-02-05: last of 2 revisions
- 2023-01-24: received
- See all versions
- Short URL
- https://ia.cr/2023/087
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2023/087, author = {Katharina Kreuzer}, title = {Verification of Correctness and Security Properties for {CRYSTALS}-{KYBER}}, howpublished = {Cryptology {ePrint} Archive, Paper 2023/087}, year = {2023}, url = {https://eprint.iacr.org/2023/087} }