From bc1ba13c0653352da78e5a12bca5909dabc719ba Mon Sep 17 00:00:00 2001 From: mamonet Date: Tue, 24 Sep 2024 13:17:00 +0000 Subject: [PATCH] Add proofs for encapsulate/decapsulate in Ind_cca --- .../extraction/Libcrux_ml_kem.Ind_cca.fst | 66 +++++++++++++++---- .../extraction/Libcrux_ml_kem.Ind_cca.fsti | 10 +-- .../proofs/fstar/spec/Spec.MLKEM.fst | 4 +- libcrux-ml-kem/src/ind_cca.rs | 41 ++++++++++-- 4 files changed, 96 insertions(+), 25 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst index 812549884..de9bf4482 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst @@ -192,8 +192,6 @@ let validate_public_key in public_key =. public_key_serialized -#push-options "--admit_smt_queries true" - #push-options "--z3rlimit 500" let decapsulate @@ -210,6 +208,10 @@ let decapsulate (private_key: Libcrux_ml_kem.Types.t_MlKemPrivateKey v_SECRET_KEY_SIZE) (ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE) = + let _:Prims.unit = + assert (v v_CIPHERTEXT_SIZE == + v v_IMPLICIT_REJECTION_HASH_INPUT_SIZE - v Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE) + in let ind_cpa_secret_key, secret_key:(t_Slice u8 & t_Slice u8) = Core.Slice.impl__split_at #u8 (private_key.Libcrux_ml_kem.Types.f_value <: t_Slice u8) @@ -221,6 +223,20 @@ let decapsulate let ind_cpa_public_key_hash, implicit_rejection_value:(t_Slice u8 & t_Slice u8) = Core.Slice.impl__split_at #u8 secret_key Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE in + let _:Prims.unit = + assert (ind_cpa_secret_key == slice private_key.f_value (sz 0) v_CPA_SECRET_KEY_SIZE); + assert (ind_cpa_public_key == + slice private_key.f_value v_CPA_SECRET_KEY_SIZE (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE) + ); + assert (ind_cpa_public_key_hash == + slice private_key.f_value + (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE) + (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE)); + assert (implicit_rejection_value == + slice private_key.f_value + (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE) + (length private_key.f_value)) + in let decrypted:t_Array u8 (sz 32) = Libcrux_ml_kem.Ind_cpa.decrypt v_K v_CIPHERTEXT_SIZE @@ -234,6 +250,7 @@ let decapsulate let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) = Libcrux_ml_kem.Utils.into_padded_array (sz 64) (decrypted <: t_Slice u8) in + let _:Prims.unit = eq_intro (Seq.slice to_hash 0 32) decrypted in let to_hash:t_Array u8 (sz 64) = Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE } @@ -249,6 +266,11 @@ let decapsulate <: t_Slice u8) in + let _:Prims.unit = + lemma_slice_append to_hash decrypted ind_cpa_public_key_hash; + assert (decrypted == Spec.MLKEM.ind_cpa_decrypt v_K ind_cpa_secret_key ciphertext.f_value); + assert (to_hash == concat decrypted ind_cpa_public_key_hash) + in let hashed:t_Array u8 (sz 64) = Libcrux_ml_kem.Hash_functions.f_G #v_Hasher #v_K @@ -260,11 +282,21 @@ let decapsulate (hashed <: t_Slice u8) Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE in + let _:Prims.unit = + assert ((shared_secret, pseudorandomness) == + split hashed Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE); + assert (length implicit_rejection_value = + v_SECRET_KEY_SIZE -! v_CPA_SECRET_KEY_SIZE -! v_PUBLIC_KEY_SIZE -! + Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE); + assert (length implicit_rejection_value = Spec.MLKEM.v_SHARED_SECRET_SIZE); + assert (Spec.MLKEM.v_SHARED_SECRET_SIZE <=. Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE v_K) + in let (to_hash: t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE):t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE = Libcrux_ml_kem.Utils.into_padded_array v_IMPLICIT_REJECTION_HASH_INPUT_SIZE implicit_rejection_value in + let _:Prims.unit = eq_intro (Seq.slice to_hash 0 32) implicit_rejection_value in let to_hash:t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE = Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE } @@ -285,8 +317,12 @@ let decapsulate <: t_Slice u8) in - let _:Prims.unit = assert (v (sz 32) < pow2 32) in - let _:Prims.unit = assert (i4.f_PRF_pre (sz 32) to_hash) in + let _:Prims.unit = + assert_norm (pow2 32 == 0x100000000); + assert (v (sz 32) < pow2 32); + assert (i4.f_PRF_pre (sz 32) to_hash); + lemma_slice_append to_hash implicit_rejection_value ciphertext.f_value + in let (implicit_rejection_shared_secret: t_Array u8 (sz 32)):t_Array u8 (sz 32) = Libcrux_ml_kem.Hash_functions.f_PRF #v_Hasher #v_K @@ -294,6 +330,10 @@ let decapsulate (sz 32) (to_hash <: t_Slice u8) in + let _:Prims.unit = + assert (implicit_rejection_shared_secret == Spec.Utils.v_PRF (sz 32) to_hash); + assert (Seq.length ind_cpa_public_key == v v_PUBLIC_KEY_SIZE) + in let expected_ciphertext:t_Array u8 v_CIPHERTEXT_SIZE = Libcrux_ml_kem.Ind_cpa.encrypt v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_SIZE v_C2_SIZE v_VECTOR_U_COMPRESSION_FACTOR v_VECTOR_V_COMPRESSION_FACTOR v_C1_BLOCK_SIZE v_ETA1 @@ -331,8 +371,6 @@ let decapsulate #pop-options -#pop-options - #push-options "--z3rlimit 150" let encapsulate @@ -359,6 +397,7 @@ let encapsulate let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) = Libcrux_ml_kem.Utils.into_padded_array (sz 64) (randomness <: t_Slice u8) in + let _:Prims.unit = eq_intro (Seq.slice to_hash 0 32) randomness in let to_hash:t_Array u8 (sz 64) = Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE } @@ -379,6 +418,11 @@ let encapsulate <: t_Slice u8) in + let _:Prims.unit = + assert (Seq.slice to_hash 0 (v Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE) == randomness); + lemma_slice_append to_hash randomness (Spec.Utils.v_H public_key.f_value); + assert (to_hash == concat randomness (Spec.Utils.v_H public_key.f_value)) + in let hashed:t_Array u8 (sz 64) = Libcrux_ml_kem.Hash_functions.f_G #v_Hasher #v_K @@ -412,13 +456,9 @@ let encapsulate shared_secret ciphertext in - let result:(Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32)) = - ciphertext, shared_secret_array - <: - (Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32)) - in - let _:Prims.unit = admit () (* Panic freedom *) in - result + ciphertext, shared_secret_array + <: + (Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32)) #pop-options diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fsti index 69d9a3cbd..1f5d45da9 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fsti @@ -100,9 +100,9 @@ class t_Variant (v_Self: Type0) = { v_K: usize -> #v_Hasher: Type0 -> {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> - t_Slice u8 -> - t_Array u8 (sz 32) - -> Type0; + randomness: t_Slice u8 -> + result: t_Array u8 (sz 32) + -> pred: Type0{pred ==> result == randomness}; f_entropy_preprocess: v_K: usize -> #v_Hasher: Type0 -> @@ -183,9 +183,9 @@ let impl: t_Variant t_MlKem = i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) (randomness: t_Slice u8) - (out: t_Array u8 (sz 32)) + (result: t_Array u8 (sz 32)) -> - true); + result == randomness); f_entropy_preprocess = fun diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst index 44ae4d7af..07c9216ae 100644 --- a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst +++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst @@ -240,7 +240,8 @@ val ind_cpa_encrypt (r:rank) (public_key: t_MLKEMPublicKey r) (message: t_Array u8 v_SHARED_SECRET_SIZE) (randomness:t_Array u8 v_SHARED_SECRET_SIZE) : (t_MLKEMCiphertext r & bool) - + +[@ "opaque_to_smt"] let ind_cpa_encrypt r public_key message randomness = let (t_as_ntt_bytes, seed_for_A) = split public_key (v_T_AS_NTT_ENCODED_SIZE r) in let t_as_ntt = vector_decode_12 #r t_as_ntt_bytes in @@ -262,6 +263,7 @@ val ind_cpa_decrypt (r:rank) (secret_key: t_MLKEMCPAPrivateKey r) (ciphertext: t_MLKEMCiphertext r): t_MLKEMSharedSecret +[@ "opaque_to_smt"] let ind_cpa_decrypt r secret_key ciphertext = let (c1,c2) = split ciphertext (v_C1_SIZE r) in let u = decode_then_decompress_u #r c1 in diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs index 2199a9412..ae4b87ebe 100644 --- a/libcrux-ml-kem/src/ind_cca.rs +++ b/libcrux-ml-kem/src/ind_cca.rs @@ -163,10 +163,7 @@ fn generate_keypair< MlKemKeyPair::from(private_key, MlKemPublicKey::from(public_key)) } -// For some reason F* manages to assert the post-condition but fails to verify it -// as a part of function signature #[hax_lib::fstar::options("--z3rlimit 150")] -#[hax_lib::fstar::verification_status(panic_free)] #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\ $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\ $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ @@ -205,7 +202,11 @@ fn encapsulate< ) -> (MlKemCiphertext, MlKemSharedSecret) { let randomness = Scheme::entropy_preprocess::(&randomness); let mut to_hash: [u8; 2 * H_DIGEST_SIZE] = into_padded_array(&randomness); + hax_lib::fstar!("eq_intro (Seq.slice $to_hash 0 32) $randomness"); to_hash[H_DIGEST_SIZE..].copy_from_slice(&Hasher::H(public_key.as_slice())); + hax_lib::fstar!("assert (Seq.slice to_hash 0 (v $H_DIGEST_SIZE) == $randomness); + lemma_slice_append $to_hash $randomness (Spec.Utils.v_H ${public_key}.f_value); + assert ($to_hash == concat $randomness (Spec.Utils.v_H ${public_key}.f_value))"); let hashed = Hasher::G(&to_hash); let (shared_secret, pseudorandomness) = hashed.split_at(SHARED_SECRET_SIZE); @@ -233,7 +234,6 @@ fn encapsulate< /// This code verifies on some machines, runs out of memory on others #[hax_lib::fstar::options("--z3rlimit 500")] -#[hax_lib::fstar::verification_status(lax)] #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\ $SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\ $CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\ @@ -276,10 +276,17 @@ pub(crate) fn decapsulate< private_key: &MlKemPrivateKey, ciphertext: &MlKemCiphertext, ) -> MlKemSharedSecret { + hax_lib::fstar!("assert (v $CIPHERTEXT_SIZE == v $IMPLICIT_REJECTION_HASH_INPUT_SIZE - v $SHARED_SECRET_SIZE)"); let (ind_cpa_secret_key, secret_key) = private_key.value.split_at(CPA_SECRET_KEY_SIZE); let (ind_cpa_public_key, secret_key) = secret_key.split_at(PUBLIC_KEY_SIZE); let (ind_cpa_public_key_hash, implicit_rejection_value) = secret_key.split_at(H_DIGEST_SIZE); + hax_lib::fstar!("assert ($ind_cpa_secret_key == slice ${private_key}.f_value (sz 0) $CPA_SECRET_KEY_SIZE); + assert ($ind_cpa_public_key == slice ${private_key}.f_value $CPA_SECRET_KEY_SIZE ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE)); + assert ($ind_cpa_public_key_hash == slice ${private_key}.f_value ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE) + ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE)); + assert ($implicit_rejection_value == slice ${private_key}.f_value ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE) + (length ${private_key}.f_value))"); let decrypted = crate::ind_cpa::decrypt::< K, CIPHERTEXT_SIZE, @@ -290,18 +297,31 @@ pub(crate) fn decapsulate< >(ind_cpa_secret_key, &ciphertext.value); let mut to_hash: [u8; SHARED_SECRET_SIZE + H_DIGEST_SIZE] = into_padded_array(&decrypted); + hax_lib::fstar!("eq_intro (Seq.slice $to_hash 0 32) $decrypted"); to_hash[SHARED_SECRET_SIZE..].copy_from_slice(ind_cpa_public_key_hash); + hax_lib::fstar!("lemma_slice_append to_hash $decrypted $ind_cpa_public_key_hash; + assert ($decrypted == Spec.MLKEM.ind_cpa_decrypt $K $ind_cpa_secret_key ${ciphertext}.f_value); + assert ($to_hash == concat $decrypted $ind_cpa_public_key_hash)"); let hashed = Hasher::G(&to_hash); let (shared_secret, pseudorandomness) = hashed.split_at(SHARED_SECRET_SIZE); + hax_lib::fstar!("assert (($shared_secret , $pseudorandomness) == split $hashed $SHARED_SECRET_SIZE); + assert (length $implicit_rejection_value = $SECRET_KEY_SIZE -! $CPA_SECRET_KEY_SIZE -! $PUBLIC_KEY_SIZE -! $H_DIGEST_SIZE); + assert (length $implicit_rejection_value = Spec.MLKEM.v_SHARED_SECRET_SIZE); + assert (Spec.MLKEM.v_SHARED_SECRET_SIZE <=. Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE $K)"); let mut to_hash: [u8; IMPLICIT_REJECTION_HASH_INPUT_SIZE] = into_padded_array(implicit_rejection_value); + hax_lib::fstar!("eq_intro (Seq.slice $to_hash 0 32) $implicit_rejection_value"); to_hash[SHARED_SECRET_SIZE..].copy_from_slice(ciphertext.as_ref()); - hax_lib::fstar!("assert (v (sz 32) < pow2 32)"); - hax_lib::fstar!("assert (i4.f_PRF_pre (sz 32) to_hash)"); + hax_lib::fstar!("assert_norm (pow2 32 == 0x100000000); + assert (v (sz 32) < pow2 32); + assert (i4.f_PRF_pre (sz 32) $to_hash); + lemma_slice_append $to_hash $implicit_rejection_value ${ciphertext}.f_value"); let implicit_rejection_shared_secret: [u8; SHARED_SECRET_SIZE] = Hasher::PRF(&to_hash); + hax_lib::fstar!("assert ($implicit_rejection_shared_secret == Spec.Utils.v_PRF (sz 32) $to_hash); + assert (Seq.length $ind_cpa_public_key == v $PUBLIC_KEY_SIZE)"); let expected_ciphertext = crate::ind_cpa::encrypt::< K, CIPHERTEXT_SIZE, @@ -551,6 +571,9 @@ pub(crate) trait Variant { ciphertext: &MlKemCiphertext, ) -> [u8; 32]; #[requires(randomness.len() == 32)] + #[ensures(|result| + fstar!("$result == $randomness")) + ] fn entropy_preprocess>(randomness: &[u8]) -> [u8; 32]; } @@ -578,6 +601,9 @@ impl Variant for Kyber { #[inline(always)] #[requires(randomness.len() == 32)] + #[ensures(|result| + fstar!("$result == Spec.Utils.v_H $randomness")) + ] fn entropy_preprocess>(randomness: &[u8]) -> [u8; 32] { Hasher::H(&randomness) } @@ -605,6 +631,9 @@ impl Variant for MlKem { #[inline(always)] #[requires(randomness.len() == 32)] + #[ensures(|result| + fstar!("$result == $randomness")) + ] fn entropy_preprocess>(randomness: &[u8]) -> [u8; 32] { randomness.try_into().unwrap() }