Skip to content

Commit

Permalink
Don't inadvertently perform explicit rejection in Kyber. (#95)
Browse files Browse the repository at this point in the history 
* Don't inadvertently perform explicit rejection in Kyber.
* Update f-star extraction.
  • Loading branch information
@xvzcf
xvzcf authored Sep 28, 2023
1 parent 21a26b7 commit fdc4a1a
Show file tree
Hide file tree
Showing 6 changed files with 525 additions and 657 deletions.
789 changes: 341 additions & 448 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber768.Ind_cpa.fst
View file

Large diffs are not rendered by default.

10 changes: 5 additions & 5 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber768.Sampling.fst
View file
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
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

0 comments on commit fdc4a1a

Please sign in to comment.