### Abstract

This article formalizes the specification and the algorithm of the cryptographic scheme CRYSTALS-KYBER with multiplication using the Number Theoretic Transform and verifies its (1-δ)-correctness proof. CRYSTALS-KYBER is a key encapsulation mechanism in lattice-based post-quantum cryptography. This entry formalizes the key generation, encryption and decryption algorithms and shows that the algorithm decodes correctly under a highly probable assumption ((1-δ)-correctness). Moreover, the Number Theoretic Transform (NTT) in the case of Kyber and the convolution theorem thereon is formalized.

### License

BSD License

### Topics

- Computer science/Security

### Session CRYSTALS-Kyber

- Kyber_spec
- Mod_Plus_Minus
- Abs_Qr
- Compress
- Crypto_Scheme
- Kyber_Values
- Mod_Ring_Numeral
- NTT_Scheme
- Crypto_Scheme_NTT
- Powers3844
- Kyber_NTT_Values

### Depends on

- The Factorization Algorithm of Berlekamp and Zassenhaus
- Number Theoretic Transform

### Used by

- CRYSTALS-Kyber_Security

## Cite

×

CRYSTALS-Kyber-AFP

    @article{CRYSTALS-Kyber-AFP,
      author  = {Katharina Kreuzer},
      title   = {CRYSTALS-Kyber},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/CRYSTALS-Kyber.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Sep 8, 2022 : Isabelle2021-1