Secret independence for Kyber

[karthikbhargavan]

trafficstars

This issue tracks work on secret independence proofs for Kyber using the F* type system and HACL* secret integers library:

• [x] Libcrux.Kem.fst
• [x] Libcrux.Kem.Kyber.Constants.fst
• [x] Libcrux.Digest.fsti
• [x] Libcrux.Kem.Kyber.Hash_functions.fst
• [x] Libcrux.Kem.Kyber.Kyber768.fst
• [x] Libcrux.Kem.Kyber.Kyber1024.fst
• [x] Libcrux.Kem.Kyber.Kyber512.fst
• [x] Libcrux.Kem.Kyber.fst
• [x] Libcrux.Kem.Kyber.Types.fst
• [x] Libcrux.Kem.Kyber.Ind_cpa.fst
• [x] Libcrux.Kem.Kyber.Arithmetic.fst
• [x] Libcrux.Kem.Kyber.Compress.fst
• [x] Libcrux.Kem.Kyber.Constant_time_ops.fst
• [x] Libcrux.Kem.Kyber.Conversions.fst
• [x] Libcrux.Kem.Kyber.Matrix.fst
• [x] Libcrux.Kem.Kyber.Sampling.fst
• [x] Libcrux.Kem.Kyber.Serialize.fst
• [x] Libcrux.Kem.Kyber.Ntt.fst

[karthikbhargavan]

Addressed by https://github.com/cryspen/libcrux/pull/169

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.