Cleanup conf_auth send and receive functions: Remove higher_layer_preds.send_conf from precondition; Add property confauth_message_properties'

fabian-hk · fabian-hk · commit 03176f55f002 · 2026-01-30T10:44:55.000+01:00
diff --git a/src/lib/communication/DY.Lib.Communication.Core.Invariants.fst b/src/lib/communication/DY.Lib.Communication.Core.Invariants.fst
@@ -17,16 +17,17 @@ open DY.Lib.Communication.Core
 
 (*** PkEnc Predicates ***)
 
-#push-options "--ifuel 1"
+#push-options "--ifuel 2"
 val pke_crypto_predicates_communication_layer_core: {|cusages:crypto_usages|} -> a:Type0 -> {|comm_layer_core_config a|} -> pke_crypto_predicate
 let pke_crypto_predicates_communication_layer_core #cusages a #config  = {
   pred = (fun tr sk_usage pk msg ->
     (exists sender receiver.
-      sk_usage == long_term_key_type_to_usage (LongTermPkeKey (comm_layer_pkenc_tag a))  receiver /\
+      sk_usage == long_term_key_type_to_usage (LongTermPkeKey (comm_layer_pkenc_tag a)) receiver /\
       (get_label tr msg) `can_flow tr` (comm_label sender receiver) /\
-      parse_and_pred 
-        (fun msg_parsed -> event_triggered tr sender (CommConfSendMsg sender receiver msg_parsed <: communication_core_event a)) 
-        msg      
+      (match parse (encryption_input a) msg with
+      | Some (Unsigned payload) -> event_triggered tr sender (CommConfSendMsg sender receiver payload <: communication_core_event a) 
+      | Some (Signed payload) -> event_triggered tr sender (CommConfAuthSendMsg sender receiver payload <: communication_core_event a)
+      | None -> False)
     )
     );
   pred_later = (fun tr1 tr2 sk_usage pk msg -> ());
@@ -57,9 +58,9 @@ let sign_crypto_predicate_communication_layer_core #cusages a #config = {
       sk_usage == long_term_key_type_to_usage (LongTermSigKey (comm_layer_sign_tag a)) sender /\
       (exists plain_payload nonce.
         payload == pke_enc pk_receiver nonce plain_payload /\
-        (match parse a plain_payload with
-        | None -> False
-        | Some plain_payload_parsed -> event_triggered tr sender (CommConfAuthSendMsg sender receiver plain_payload_parsed <: communication_core_event a))
+        (match parse (encryption_input a) plain_payload with
+        | Some (Signed plain_payload_parsed) -> event_triggered tr sender (CommConfAuthSendMsg sender receiver plain_payload_parsed <: communication_core_event a)
+        | _ -> False)
       )
     )
     | None -> False)
@@ -186,6 +187,10 @@ let event_predicate_communication_layer_core
       (
         event_triggered tr sender (CommConfAuthSendMsg sender receiver payload <: communication_core_event a) \/
         is_corrupt tr (long_term_key_label sender)
+      ) /\
+      (
+        exists sender. event_triggered tr sender (CommConfAuthSendMsg sender receiver payload <: communication_core_event a) \/
+        is_well_formed a (is_publishable tr) payload
       )
     )
     )
diff --git a/src/lib/communication/DY.Lib.Communication.Core.Lemmas.fst b/src/lib/communication/DY.Lib.Communication.Core.Lemmas.fst
@@ -92,8 +92,10 @@ val encrypt_message_proof:
   (ensures
     is_publishable tr (encrypt_message pk_receiver nonce payload) 
   )
-let encrypt_message_proof #cinvs #a tr sender receiver pk_receiver nonce pkenc_in =
-  reveal_opaque (`%encrypt_message) (encrypt_message #a)
+let encrypt_message_proof #cinvs #a #config tr sender receiver pk_receiver nonce pkenc_in =
+  reveal_opaque (`%encrypt_message) (encrypt_message #a);
+  assert(is_well_formed (encryption_input a) #(parseable_serializeable_bytes_encryption_input #a) (is_knowable_by (comm_label sender receiver) tr) (Unsigned pkenc_in));
+  ()
 
 val send_confidential_proof:
   {|invs:protocol_invariants|} ->
@@ -154,7 +156,6 @@ val decrypt_message_proof:
       match decrypt_message #a sk_receiver msg_encrypted with
       | None -> True
       | Some payload -> (exists sender.
-        is_well_formed a (is_knowable_by (comm_label sender receiver) tr) payload /\
         is_well_formed a (is_knowable_by (comm_label sender receiver) tr) payload /\
         (
           comm_conf_send_event_triggered tr sender receiver payload \/
@@ -169,8 +170,22 @@ let decrypt_message_proof #cinvs #a tr receiver sk_receiver msg_encrypted =
   | None -> ()
   | Some payload -> (
     let Some plaintext = pke_dec sk_receiver msg_encrypted in
-    serialize_parse_inv_lemma #bytes a plaintext;
-    ()
+    let Some payload = parse (encryption_input a) plaintext in
+    let Unsigned payload = payload in
+    assert(exists sender. is_knowable_by (comm_label sender receiver) tr plaintext);
+    eliminate exists sender. is_knowable_by (comm_label sender receiver) tr plaintext /\ 
+      (event_triggered tr sender (CommConfSendMsg sender receiver payload <: communication_core_event a) \/
+          is_publishable tr plaintext)
+    returns exists sender. is_well_formed a (is_knowable_by (comm_label sender receiver) tr) payload /\
+            (
+              comm_conf_send_event_triggered tr sender receiver payload \/
+              is_well_formed a (is_publishable tr) payload
+            )
+    with _. (
+      parse_wf_lemma (encryption_input a) (is_knowable_by (comm_label sender receiver) tr) plaintext;
+      FStar.Classical.move_requires (parse_wf_lemma (encryption_input a) (is_publishable tr)) plaintext;
+      ()
+    )
   )
 
 val receive_confidential_proof:
@@ -253,9 +268,9 @@ val sign_message_proof:
         is_publishable tr pk /\
         (exists plain_payload nonce.
           payload == pke_enc pk nonce plain_payload /\
-          (match parse a #(parseable_serializeable_bytes_a_core #a) plain_payload with
-          | None -> False
-          | Some plain_payload_parsed -> comm_conf_auth_send_event_triggered tr sender receiver plain_payload_parsed)
+          (match parse (encryption_input a) #(parseable_serializeable_bytes_encryption_input #a) plain_payload with
+          | Some (Signed plain_payload_parsed) -> comm_conf_auth_send_event_triggered tr sender receiver plain_payload_parsed
+          | _ -> False)
         )
       )
     )
@@ -368,9 +383,9 @@ val verify_message_proof:
             (
               exists plain_payload nonce.
                 (Inr?.v payload) == pke_enc pk_receiver nonce plain_payload /\
-                (match parse a plain_payload with
-                | None -> False
-                | Some plain_payload_parsed -> comm_conf_auth_send_event_triggered tr sender receiver plain_payload_parsed)
+                (match parse (encryption_input a) plain_payload with
+                | Some (Signed plain_payload_parsed) -> comm_conf_auth_send_event_triggered tr sender receiver plain_payload_parsed
+                | _ -> False)
             ) \/ (
               is_corrupt tr (long_term_key_label sender)
             )
@@ -465,17 +480,15 @@ val encrypt_and_sign_message_proof:
     is_public_key_for tr pk_receiver (LongTermPkeKey (comm_layer_pkenc_tag a)) receiver /\
     is_private_key_for tr sk_sender (LongTermSigKey (comm_layer_sign_tag a)) sender /\
     is_well_formed a (is_knowable_by (comm_label sender receiver) tr) payload /\
-    comm_conf_send_event_triggered tr sender receiver payload /\
     comm_conf_auth_send_event_triggered tr sender receiver payload
   )
   (ensures
     is_publishable tr (encrypt_and_sign_message sender receiver payload pk_receiver sk_sender enc_nonce sign_nonce)
   )
 let encrypt_and_sign_message_proof #cinvs #a tr sender receiver payload pk_receiver sk_sender enc_nonce sign_nonce =
   reveal_opaque (`%encrypt_and_sign_message) (encrypt_and_sign_message #a);
-  reveal_opaque (`%encrypt_message) (encrypt_message #a); // TODO: This should be removeable.
-  encrypt_message_proof tr sender receiver pk_receiver enc_nonce payload;
-  let enc_payload = encrypt_message pk_receiver enc_nonce payload in
+  assert(is_well_formed (encryption_input a) #(parseable_serializeable_bytes_encryption_input #a) (is_knowable_by (comm_label sender receiver) tr) (Signed payload));
+  let enc_payload = pke_enc pk_receiver enc_nonce (serialize (encryption_input a) (Signed payload)) in
   sign_message_proof #cinvs #a tr sender receiver (Inr (enc_payload, pk_receiver)) sk_sender sign_nonce;
   ()
 
@@ -493,7 +506,6 @@ val send_confidential_authenticated_proof:
     has_private_keys_invariant /\
     has_pki_invariant /\
     has_communication_layer_core_predicates higher_layer_preds /\
-    higher_layer_preds.send_conf tr sender receiver payload /\
     higher_layer_preds.send_conf_auth tr sender receiver payload /\
     is_well_formed a (is_knowable_by (join (principal_label sender) (principal_label receiver)) tr) payload
   )
@@ -514,11 +526,6 @@ let send_confidential_authenticated_proof #invs #a tr higher_layer_preds comm_ke
     let (enc_nonce, tr') = mk_rand PkeNonce (long_term_key_label sender) 32 tr' in
     let (sign_nonce, tr') = mk_rand SigNonce (long_term_key_label sender) 32 tr' in
 
-    let payload_bytes = serialize #bytes a payload in
-    higher_layer_preds.send_conf_later tr tr' sender receiver payload;
-    let ((), tr') = trigger_event sender (CommConfSendMsg sender receiver payload <: communication_core_event a) tr' in
-    assert(comm_conf_send_event_triggered tr' sender receiver payload);
-
     higher_layer_preds.send_conf_auth_later tr tr' sender receiver payload;
     let ((), tr') = trigger_event sender (CommConfAuthSendMsg sender receiver payload <: communication_core_event a) tr' in
     assert(comm_conf_auth_send_event_triggered tr' sender receiver payload);
@@ -552,7 +559,7 @@ val verify_and_decrypt_message_proof:
     | None -> True
     | Some cm -> (
       (
-        (exists sender. event_triggered tr sender (CommConfSendMsg sender receiver cm.payload <: communication_core_event a)) \/
+        (exists sender. comm_conf_auth_send_event_triggered tr sender receiver cm.payload) \/
         is_well_formed a (is_publishable tr) cm.payload
       ) /\ (
         comm_conf_auth_send_event_triggered tr sender receiver cm.payload \/
@@ -575,16 +582,21 @@ let verify_and_decrypt_message_proof #cinvs #a tr sender receiver msg_encrypted_
     assert(pk_receiver == pk sk_receiver);
 
     let Some plaintext = pke_dec sk_receiver payload_enc in
-    serialize_parse_inv_lemma #bytes a plaintext;
+    let Some payload = parse (encryption_input a) plaintext in
+    let Signed payload = payload in
+
+    FStar.Classical.move_requires (parse_wf_lemma (encryption_input a) (is_publishable tr)) plaintext;
+    assert(exists sender. event_triggered tr sender (CommConfAuthSendMsg sender receiver payload <: communication_core_event a) \/ is_well_formed a (is_publishable tr) payload);
 
     introduce (~(is_corrupt tr (long_term_key_label sender))) ==>  (
         comm_conf_auth_send_event_triggered tr sender receiver cm.payload
       )
     with _. (
       eliminate exists plain_payload nonce.
           payload_enc == pke_enc pk_receiver nonce plain_payload /\
-          Some? (parse a plain_payload) /\
-          comm_conf_auth_send_event_triggered tr sender receiver (Some?.v (parse a plain_payload))
+          Some? (parse (encryption_input a) plain_payload) /\
+          Signed? (Some?.v (parse (encryption_input a) plain_payload)) /\
+          comm_conf_auth_send_event_triggered tr sender receiver (Signed?.payload (Some?.v (parse (encryption_input a) plain_payload)))
       returns comm_conf_auth_send_event_triggered tr sender receiver cm.payload
       with _. (
         pke_dec_enc sk_receiver nonce plain_payload;
@@ -609,17 +621,14 @@ val receive_confidential_authenticated_proof:
     has_pki_invariant /\
     has_communication_layer_core_predicates higher_layer_preds
   )
-  (ensures
-    (
-      match receive_confidential_authenticated #a comm_keys_ids receiver msg_id tr with
-      | (None, tr_out) -> trace_invariant tr_out
-      | (Some cm, tr_out) -> (
-        trace_invariant tr_out /\
-        event_triggered tr_out receiver (CommConfReceiveMsg receiver cm.payload <: communication_core_event a) /\
-        event_triggered tr_out receiver (CommConfAuthReceiveMsg cm.sender receiver cm.payload <: communication_core_event a)
-      )
+  (ensures(
+    match receive_confidential_authenticated #a comm_keys_ids receiver msg_id tr with
+    | (None, tr_out) -> trace_invariant tr_out
+    | (Some cm, tr_out) -> (
+      trace_invariant tr_out /\
+      event_triggered tr_out receiver (CommConfAuthReceiveMsg cm.sender receiver cm.payload <: communication_core_event a)
     )
-  )
+  ))
   [SMTPat (trace_invariant #invs tr);
    SMTPat (receive_confidential_authenticated #a comm_keys_ids receiver msg_id tr);
    SMTPat (core_comm_layer_lemmas_enabled higher_layer_preds)]
@@ -636,7 +645,6 @@ let receive_confidential_authenticated_proof #invs #a tr higher_layer_preds comm
     let (Some vk_sender, tr) = get_public_key receiver comm_keys_ids.pki (LongTermSigKey (comm_layer_sign_tag a)) sender tr in
     verify_and_decrypt_message_proof #invs.crypto_invs #a tr sender receiver msg_encrypted_signed sk_receiver vk_sender;
     let Some cm = verify_and_decrypt_message #a receiver sk_receiver vk_sender msg_encrypted_signed in
-    let ((), tr) = trigger_event receiver (CommConfReceiveMsg receiver cm.payload <: communication_core_event a) tr in
     let ((), tr) = trigger_event receiver (CommConfAuthReceiveMsg sender receiver cm.payload <: communication_core_event a) tr in
     assert(trace_invariant tr);
     assert(tr == tr_out);
diff --git a/src/lib/communication/DY.Lib.Communication.Core.Properties.fst b/src/lib/communication/DY.Lib.Communication.Core.Properties.fst
@@ -139,4 +139,43 @@ let confauth_message_properties #invs #a tr higher_layer_preds sender receiver p
     higher_layer_preds.send_conf_auth_later (prefix tr j) tr sender receiver payload;
     ()
   )
-  and _. ()
+  and _. ()
+
+val confauth_message_properties':
+  {|protocol_invariants|} ->
+  #a:Type -> {|comm_layer_core_config a|} ->
+  tr:trace ->
+  higher_layer_preds:comm_core_higher_layer_event_preds a ->
+  sender:principal -> receiver:principal -> payload:a ->
+  Lemma
+  (requires
+    trace_invariant tr /\
+    has_communication_layer_core_predicates higher_layer_preds /\
+    event_triggered tr receiver (CommConfAuthReceiveMsg sender receiver payload <: communication_core_event a)
+  )
+  (ensures
+    is_well_formed a (is_knowable_by (principal_label receiver) tr) payload /\
+    (exists sender'. higher_layer_preds.send_conf_auth tr sender' receiver payload \/
+    is_well_formed a (is_publishable tr) payload)
+  )
+let confauth_message_properties' #invs #a tr higher_layer_preds sender receiver payload =
+  let send_event sender':communication_core_event a = CommConfAuthSendMsg sender' receiver payload in
+  let i = find_event_triggered_at_timestamp tr receiver (CommConfAuthReceiveMsg sender receiver payload <: communication_core_event a) in
+  let tr_i = prefix tr i in
+  eliminate (exists sender'. event_triggered tr_i sender' (send_event sender')) \/ is_well_formed a (is_publishable tr_i) payload
+  returns
+    is_well_formed a (is_knowable_by (principal_label receiver) tr) payload /\
+    (exists sender'. higher_layer_preds.send_conf_auth tr sender' receiver payload \/
+    is_well_formed a (is_publishable tr) payload)
+  with _. (
+    eliminate exists sender'. event_triggered tr_i sender' (send_event sender')
+    returns _
+    with _. (
+      let j = find_event_triggered_at_timestamp tr sender' (send_event sender') in
+      find_event_triggered_at_timestamp_later tr_i tr sender' (send_event sender');
+      higher_layer_preds.send_conf_auth_later (prefix tr j) tr sender' receiver payload;
+      ()
+    )
+  )
+  and _. ()
+  
diff --git a/src/lib/communication/DY.Lib.Communication.Core.fst b/src/lib/communication/DY.Lib.Communication.Core.fst
@@ -57,10 +57,10 @@ instance event_communication_core_event (a:Type) {|config:comm_layer_core_config
 
 [@@ "opaque_to_smt"]
 val encrypt_message:
-  #a:Type -> {|comm_layer_core_config a|} ->
+  #a:Type0 -> {|comm_layer_core_config a|} ->
   bytes -> bytes -> a -> bytes
 let encrypt_message #a pk_receiver nonce payload =
-  pke_enc pk_receiver nonce (serialize a payload)
+  pke_enc pk_receiver nonce (serialize (encryption_input a) (Unsigned payload))
 
 [@@ "opaque_to_smt"]
 val send_confidential:
@@ -82,7 +82,10 @@ val decrypt_message:
   bytes -> bytes -> option a
 let decrypt_message #a sk_receiver msg_encrypted =
   let? plaintext = pke_dec sk_receiver msg_encrypted in
-  parse #bytes a plaintext
+  let? payload = parse (encryption_input a) plaintext in
+  guard (Unsigned? payload);?
+  let Unsigned payload = payload in
+  Some payload
 
 [@@ "opaque_to_smt"]
 val receive_confidential:
@@ -193,7 +196,7 @@ val encrypt_and_sign_message:
   #a:Type0 -> {|comm_layer_core_config a|} ->
   principal -> principal -> a -> bytes -> bytes -> bytes -> bytes -> bytes
 let encrypt_and_sign_message #a sender receiver payload pk_receiver sk_sender enc_nonce sign_nonce =
-  let enc_payload = encrypt_message #a pk_receiver enc_nonce payload in
+  let enc_payload = pke_enc pk_receiver enc_nonce (serialize (encryption_input a) (Signed payload)) in
   sign_message #a sender receiver (Inr (enc_payload, pk_receiver)) sk_sender sign_nonce
 
 // We do not encrypt the sender and receiver because, in real-world settings,
@@ -211,7 +214,6 @@ let send_confidential_authenticated #a comm_keys_ids sender receiver payload =
   let*? sk_sender = get_private_key sender comm_keys_ids.private_keys (LongTermSigKey (comm_layer_sign_tag a)) in
   let* enc_nonce = mk_rand PkeNonce (long_term_key_label sender) 32 in
   let* sign_nonce = mk_rand SigNonce (long_term_key_label sender) 32 in
-  trigger_event sender (CommConfSendMsg sender receiver payload <: communication_core_event a);*
   trigger_event sender (CommConfAuthSendMsg sender receiver payload <: communication_core_event a);*
   let msg_encrypted_signed_bytes = encrypt_and_sign_message sender receiver payload pk_receiver sk_sender enc_nonce sign_nonce in
   let* msg_id = send_msg msg_encrypted_signed_bytes in
@@ -223,7 +225,10 @@ val verify_and_decrypt_message:
   principal -> bytes -> bytes -> bytes -> option (communication_message a)
 let verify_and_decrypt_message #a receiver sk_receiver vk_sender msg_encrypted_signed =
   let? Inr payload_enc = verify_message #a receiver msg_encrypted_signed (Some sk_receiver) vk_sender in
-  let? payload:a = decrypt_message #a sk_receiver payload_enc in
+  let? plaintext = pke_dec sk_receiver payload_enc in
+  let? payload = parse #bytes (encryption_input a) plaintext in
+  guard (Signed? payload);?
+  let Signed payload = payload in
   let? sender = get_sender #a msg_encrypted_signed in
   Some {sender; receiver; payload}
 
@@ -238,8 +243,7 @@ let receive_confidential_authenticated #a comm_keys_ids receiver msg_id =
   let*? sk_receiver = get_private_key receiver comm_keys_ids.private_keys (LongTermPkeKey (comm_layer_pkenc_tag a)) in
   let*? sender = return (get_sender #a msg_encrypted_signed) in
   let*? vk_sender = get_public_key receiver comm_keys_ids.pki (LongTermSigKey (comm_layer_sign_tag a)) sender in 
-  let*? cm:communication_message a = return (verify_and_decrypt_message #a receiver sk_receiver vk_sender msg_encrypted_signed) in 
-  trigger_event receiver (CommConfReceiveMsg receiver cm.payload <: communication_core_event a);*
+  let*? cm:communication_message a = return (verify_and_decrypt_message #a receiver sk_receiver vk_sender msg_encrypted_signed) in
   trigger_event receiver (CommConfAuthReceiveMsg sender receiver cm.payload <: communication_core_event a);*
   return (Some cm)
 
diff --git a/src/lib/communication/DY.Lib.Communication.Data.fst b/src/lib/communication/DY.Lib.Communication.Data.fst
@@ -27,6 +27,19 @@ type communication_message (a:Type) = {
   payload:a;
 }
 
+[@@with_bytes bytes]
+type encryption_input (a:Type) {|config:comm_layer_core_config a|} =
+  | Unsigned: [@@@ with_parser #bytes config.core_ps_a] payload:a -> encryption_input a
+  | Signed: [@@@ with_parser #bytes config.core_ps_a] payload:a -> encryption_input a
+
+#push-options "--ifuel 1 --fuel 0"
+%splice [ps_encryption_input] (gen_parser (`encryption_input))
+%splice [ps_encryption_input_is_well_formed] (gen_is_well_formed_lemma (`encryption_input))
+#pop-options
+
+instance parseable_serializeable_bytes_encryption_input (#a:Type) {|config:comm_layer_core_config a|}: parseable_serializeable bytes (encryption_input a)
+  = mk_parseable_serializeable (ps_encryption_input a)
+
 [@@with_bytes bytes]
 type signature_input (a:Type) {|config:comm_layer_core_config a|} = 
   | Plain: sender:principal -> receiver:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> signature_input a
