Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't inadvertently perform explicit rejection in Kyber. #95

Merged
merged 4 commits into from
Sep 28, 2023
+525 −657
Merged

Don't inadvertently perform explicit rejection in Kyber. #95

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
09a2604
Don't inadvertently perform explicit rejection in Kyber.
xvzcf Sep 26, 2023
7182830
Update f-star extraction.
xvzcf Sep 26, 2023
fdba901
Review comments.
xvzcf Sep 27, 2023
6631529
Update f-star extraction.
xvzcf Sep 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
789 changes: 341 additions & 448 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber768.Ind_cpa.fst
View file
Open in desktop

Large diffs are not rendered by default.

10 changes: 5 additions & 5 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber768.Sampling.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ module Libcrux.Kem.Kyber768.Sampling
open Core

let sample_from_uniform_distribution (randomness: array u8 840sz)
: Core.Result.t_Result Libcrux.Kem.Kyber768.Arithmetic.t_KyberPolynomialRingElement
Libcrux.Kem.Kyber768.t_BadRejectionSamplingRandomnessError =
: (Libcrux.Kem.Kyber768.Arithmetic.t_KyberPolynomialRingElement &
Core.Option.t_Option Libcrux.Kem.Kyber768.t_BadRejectionSamplingRandomnessError) =
let (sampled_coefficients: usize):usize = 0sz in
let (out: Libcrux.Kem.Kyber768.Arithmetic.t_KyberPolynomialRingElement):Libcrux.Kem.Kyber768.Arithmetic.t_KyberPolynomialRingElement
=
Expand Down Expand Up @@ -55,13 +55,13 @@ let sample_from_uniform_distribution (randomness: array u8 840sz)
in
if sampled_coefficients =. Libcrux.Kem.Kyber768.Parameters.v_COEFFICIENTS_IN_RING_ELEMENT
then
let* hoist11:Rust_primitives.Hax.t_Never =
Core.Ops.Control_flow.ControlFlow.v_Break (Core.Result.Result_Ok out)
let* hoist1:Rust_primitives.Hax.t_Never =
Core.Ops.Control_flow.ControlFlow.v_Break (out, Core.Option.Option_None)
in
Core.Ops.Control_flow.ControlFlow_Continue (out, sampled_coefficients)
else Core.Ops.Control_flow.ControlFlow_Continue (out, sampled_coefficients))
in
Core.Result.Result_Err Libcrux.Kem.Kyber768.BadRejectionSamplingRandomnessError
out, Core.Option.Option_Some Libcrux.Kem.Kyber768.BadRejectionSamplingRandomnessError

let sample_from_binomial_distribution_2_ (randomness: array u8 128sz)
: Libcrux.Kem.Kyber768.Arithmetic.t_KyberPolynomialRingElement =
Expand Down
279 changes: 115 additions & 164 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber768.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,154 +34,121 @@ type t_BadRejectionSamplingRandomnessError =

let generate_keypair (randomness: array u8 64sz)
: Core.Result.t_Result (array u8 1184sz & array u8 2400sz) t_BadRejectionSamplingRandomnessError =
Rust_primitives.Hax.Control_flow_monad.Mexception.run (let ind_cpa_keypair_randomness:slice u8 =
randomness.[ {
Core.Ops.Range.Range.f_start = 0sz;
Core.Ops.Range.Range.f_end
=
Libcrux.Kem.Kyber768.Parameters.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
} ]
in
let implicit_rejection_value:slice u8 =
randomness.[ {
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
} ]
in
let* ind_cpa_key_pair:Libcrux.Kem.Kyber768.Ind_cpa.t_KeyPair =
match
Core.Ops.Try_trait.Try.branch (Libcrux.Kem.Kyber768.Ind_cpa.generate_keypair ind_cpa_keypair_randomness

<:
Core.Result.t_Result Libcrux.Kem.Kyber768.Ind_cpa.t_KeyPair
t_BadRejectionSamplingRandomnessError)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist12:Rust_primitives.Hax.t_Never =
Core.Ops.Control_flow.ControlFlow.v_Break (Core.Ops.Try_trait.FromResidual.from_residual
residual
<:
Core.Result.t_Result (array u8 1184sz & array u8 2400sz)
t_BadRejectionSamplingRandomnessError)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist12)
| Core.Ops.Control_flow.ControlFlow_Continue v_val ->
Core.Ops.Control_flow.ControlFlow_Continue v_val
in
Core.Ops.Control_flow.ControlFlow_Continue
(let secret_key_serialized:array u8 2400sz =
Libcrux.Kem.Kyber768.Ind_cpa.serialize_secret_key_under_impl ind_cpa_key_pair
implicit_rejection_value
in
Core.Result.Result_Ok
(Libcrux.Kem.Kyber768.Ind_cpa.pk_under_impl ind_cpa_key_pair, secret_key_serialized)))
let ind_cpa_keypair_randomness:slice u8 =
randomness.[ {
Core.Ops.Range.Range.f_start = 0sz;
Core.Ops.Range.Range.f_end
=
Libcrux.Kem.Kyber768.Parameters.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
} ]
in
let implicit_rejection_value:slice u8 =
randomness.[ {
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
} ]
in
let ind_cpa_key_pair, sampling_a_error:(Libcrux.Kem.Kyber768.Ind_cpa.t_KeyPair &
Core.Option.t_Option t_BadRejectionSamplingRandomnessError) =
Libcrux.Kem.Kyber768.Ind_cpa.generate_keypair ind_cpa_keypair_randomness
in
let secret_key_serialized:array u8 2400sz =
Libcrux.Kem.Kyber768.Ind_cpa.serialize_secret_key_under_impl ind_cpa_key_pair
implicit_rejection_value
in
match sampling_a_error with
| Core.Option.Option_Some error -> Core.Result.Result_Err error
| _ ->
Core.Result.Result_Ok
(Libcrux.Kem.Kyber768.Ind_cpa.pk_under_impl ind_cpa_key_pair, secret_key_serialized)

let encapsulate (public_key: array u8 1184sz) (randomness: array u8 32sz)
: Core.Result.t_Result (array u8 1088sz & array u8 32sz) t_BadRejectionSamplingRandomnessError =
Rust_primitives.Hax.Control_flow_monad.Mexception.run (let randomness_hashed:array u8 32sz =
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H (Rust_primitives.unsize randomness
<:
slice u8)
in
let (to_hash: array u8 64sz):array u8 64sz =
Libcrux.Kem.Kyber768.Conversions.into_padded_array (Rust_primitives.unsize randomness_hashed
let randomness_hashed:array u8 32sz =
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H (Rust_primitives.unsize randomness
<:
slice u8)
in
let (to_hash: array u8 64sz):array u8 64sz =
Libcrux.Kem.Kyber768.Conversions.into_padded_array (Rust_primitives.unsize randomness_hashed
<:
slice u8)
in
let to_hash:array u8 64sz =
Rust_primitives.Hax.update_at to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
(Core.Slice.copy_from_slice_under_impl (Core.Ops.Index.IndexMut.index_mut to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
<:
slice u8)
in
let to_hash:array u8 64sz =
Rust_primitives.Hax.update_at to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
(Core.Slice.copy_from_slice_under_impl (Core.Ops.Index.IndexMut.index_mut to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
<:
slice u8)
(Rust_primitives.unsize (Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H (Rust_primitives.unsize
public_key
<:
slice u8)
(Rust_primitives.unsize (Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H (Rust_primitives.unsize
public_key
<:
array u8 32sz)
slice u8)
<:
slice u8)
array u8 32sz)
<:
slice u8)
in
let hashed:array u8 64sz =
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_G (Rust_primitives.unsize to_hash
<:
slice u8)
in
let hashed:array u8 64sz =
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_G (Rust_primitives.unsize to_hash <: slice u8)
in
let k_not, pseudorandomness:(slice u8 & slice u8) =
Core.Slice.split_at_under_impl (Rust_primitives.unsize hashed <: slice u8) 32sz
in
let ciphertext, sampling_a_error:(array u8 1088sz &
Core.Option.t_Option t_BadRejectionSamplingRandomnessError) =
Libcrux.Kem.Kyber768.Ind_cpa.encrypt (Rust_primitives.unsize public_key <: slice u8)
randomness_hashed
pseudorandomness
in
let (to_hash: array u8 64sz):array u8 64sz =
Libcrux.Kem.Kyber768.Conversions.into_padded_array k_not
in
let to_hash:array u8 64sz =
Rust_primitives.Hax.update_at to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
(Core.Slice.copy_from_slice_under_impl (Core.Ops.Index.IndexMut.index_mut to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
<:
slice u8)
in
let k_not, pseudorandomness:(slice u8 & slice u8) =
Core.Slice.split_at_under_impl (Rust_primitives.unsize hashed <: slice u8) 32sz
in
let* ciphertext:array u8 1088sz =
match
Core.Ops.Try_trait.Try.branch (Libcrux.Kem.Kyber768.Ind_cpa.encrypt (Rust_primitives.unsize
public_key
<:
slice u8)
randomness_hashed
pseudorandomness
<:
Core.Result.t_Result (array u8 1088sz) t_BadRejectionSamplingRandomnessError)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist13:Rust_primitives.Hax.t_Never =
Core.Ops.Control_flow.ControlFlow.v_Break (Core.Ops.Try_trait.FromResidual.from_residual
residual
(Rust_primitives.unsize (Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H (Rust_primitives.unsize
ciphertext
<:
slice u8)
<:
Core.Result.t_Result (array u8 1088sz & array u8 32sz)
t_BadRejectionSamplingRandomnessError)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist13)
| Core.Ops.Control_flow.ControlFlow_Continue v_val ->
Core.Ops.Control_flow.ControlFlow_Continue v_val
in
Core.Ops.Control_flow.ControlFlow_Continue
(let (to_hash: array u8 64sz):array u8 64sz =
Libcrux.Kem.Kyber768.Conversions.into_padded_array k_not
in
let to_hash:array u8 64sz =
Rust_primitives.Hax.update_at to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
(Core.Slice.copy_from_slice_under_impl (Core.Ops.Index.IndexMut.index_mut to_hash
({
Core.Ops.Range.RangeFrom.f_start
=
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H_DIGEST_SIZE
})
<:
slice u8)
(Rust_primitives.unsize (Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_H (Rust_primitives.unsize
ciphertext
<:
slice u8)
<:
array u8 32sz)
<:
slice u8)
<:
slice u8)
in
let (shared_secret: array u8 32sz):array u8 32sz =
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_KDF (Rust_primitives.unsize to_hash
<:
slice u8)
in
Core.Result.Result_Ok (ciphertext, shared_secret)))
array u8 32sz)
<:
slice u8)
<:
slice u8)
in
let (shared_secret: array u8 32sz):array u8 32sz =
Libcrux.Kem.Kyber768.Parameters.Hash_functions.v_KDF (Rust_primitives.unsize to_hash <: slice u8
)
in
if Core.Option.is_some_under_impl sampling_a_error
then Core.Result.Result_Err (Core.Option.unwrap_under_impl sampling_a_error)
else Core.Result.Result_Ok (ciphertext, shared_secret)

let decapsulate (secret_key: array u8 2400sz) (ciphertext: array u8 1088sz) : array u8 32sz =
let ind_cpa_secret_key, secret_key:(slice u8 & slice u8) =
Expand Down Expand Up @@ -225,37 +192,21 @@ let decapsulate (secret_key: array u8 2400sz) (ciphertext: array u8 1088sz) : ar
let k_not, pseudorandomness:(slice u8 & slice u8) =
Core.Slice.split_at_under_impl (Rust_primitives.unsize hashed <: slice u8) 32sz
in
let expected_ciphertext_result:Core.Result.t_Result (array u8 1088sz)
t_BadRejectionSamplingRandomnessError =
let expected_ciphertext, _:(array u8 1088sz &
Core.Option.t_Option t_BadRejectionSamplingRandomnessError) =
Libcrux.Kem.Kyber768.Ind_cpa.encrypt ind_cpa_public_key decrypted pseudorandomness
in
let selector:u8 =
Libcrux.Kem.Kyber768.Constant_time_ops.compare_ciphertexts_in_constant_time (Rust_primitives.unsize
ciphertext
<:
slice u8)
(Rust_primitives.unsize expected_ciphertext <: slice u8)
in
let to_hash:array u8 32sz =
match expected_ciphertext_result with
| Core.Result.Result_Ok expected_ciphertext ->
let selector:u8 =
Libcrux.Kem.Kyber768.Constant_time_ops.compare_ciphertexts_in_constant_time (Rust_primitives.unsize
ciphertext
<:
slice u8)
(Rust_primitives.unsize expected_ciphertext <: slice u8)
in
Libcrux.Kem.Kyber768.Constant_time_ops.select_shared_secret_in_constant_time k_not
implicit_rejection_value
selector
| _ ->
let out:array u8 32sz = Rust_primitives.Hax.repeat 0uy 32sz in
let out:array u8 32sz =
Rust_primitives.Hax.update_at out
Core.Ops.Range.RangeFull
(Core.Slice.copy_from_slice_under_impl (Core.Ops.Index.IndexMut.index_mut out
Core.Ops.Range.RangeFull
<:
slice u8)
implicit_rejection_value
<:
slice u8)
in
out
Libcrux.Kem.Kyber768.Constant_time_ops.select_shared_secret_in_constant_time k_not
implicit_rejection_value
selector
in
let (to_hash: array u8 64sz):array u8 64sz =
Libcrux.Kem.Kyber768.Conversions.into_padded_array (Rust_primitives.unsize to_hash <: slice u8)
Expand Down
Loading