Add receiver to comm core pred send_auth

Author: fabian-hk

src/lib/communication/DY.Lib.Communication.Core.Invariants.fst

@@ -51,7 +51,7 @@ let sign_crypto_predicate_communication_layer_core #cusages a #config = {
     | Some (Plain sender receiver payload) -> (
       sk_usage == long_term_key_type_to_usage (LongTermSigKey (comm_layer_sign_tag a)) sender /\
       get_label tr (serialize a payload) `can_flow tr` public /\
-      event_triggered tr sender (CommAuthSendMsg sender payload <: communication_core_event a)
+      event_triggered tr sender (CommAuthSendMsg sender receiver payload <: communication_core_event a)
     )
     | Some (Encrypted payload pk_receiver) -> (
       get_label tr payload `can_flow tr` public /\
@@ -111,17 +111,17 @@ type comm_core_higher_layer_event_preds (a:Type) {|comm_layer_core_config a|} =
     )
     (ensures send_conf tr2 sender receiver payload)
   ;
-  send_auth: tr:trace -> sender:principal -> payload:a -> prop;
+  send_auth: tr:trace -> sender:principal -> receiver:principal -> payload:a -> prop;
   send_auth_later:
     tr1:trace -> tr2:trace ->
-    sender:principal -> payload:a ->
+    sender:principal -> receiver:principal -> payload:a ->
     Lemma
     (requires
-      send_auth tr1 sender payload /\
+      send_auth tr1 sender receiver payload /\
       is_well_formed a (bytes_well_formed tr1) payload /\
       tr1 <$ tr2
     )
-    (ensures send_auth tr2 sender payload)
+    (ensures send_auth tr2 sender receiver payload)
   ;
   send_conf_auth: tr:trace -> sender:principal -> receiver:principal -> payload:a -> prop;
   send_conf_auth_later:
@@ -139,8 +139,8 @@ type comm_core_higher_layer_event_preds (a:Type) {|comm_layer_core_config a|} =
 let default_comm_core_higher_layer_event_preds (a:Type) {|comm_layer_core_config a|} : comm_core_higher_layer_event_preds a = {
   send_conf = (fun tr sender receiver payload -> False);
   send_conf_later = (fun tr1 tr2 sender receiver payload -> ());
-  send_auth = (fun tr sender payload -> False);
-  send_auth_later = (fun tr1 tr2 sender payload -> ());
+  send_auth = (fun tr sender receiver payload -> False);
+  send_auth_later = (fun tr1 tr2 sender receiver payload -> ());
   send_conf_auth = (fun tr sender receiver payload -> False);
   send_conf_auth_later = (fun tr1 tr2 sender receiver payload -> ())
 }
@@ -161,13 +161,13 @@ let event_predicate_communication_layer_core
       (exists sender. event_triggered tr sender (CommConfSendMsg sender receiver payload <: communication_core_event a)) \/
       is_well_formed a (is_publishable tr) payload
     )
-    | CommAuthSendMsg sender payload -> (
-      higher_layer_preds.send_auth tr sender payload
+    | CommAuthSendMsg sender receiver payload -> (
+      higher_layer_preds.send_auth tr sender receiver payload
     )
     | CommAuthReceiveMsg sender receiver payload -> (
       is_well_formed a (is_publishable tr) payload /\
       (
-        event_triggered tr sender (CommAuthSendMsg sender payload <: communication_core_event a) \/
+        event_triggered tr sender (CommAuthSendMsg sender receiver payload <: communication_core_event a) \/
         is_corrupt tr (long_term_key_label sender)
       )
     )

src/lib/communication/DY.Lib.Communication.Core.Lemmas.fst

@@ -232,10 +232,10 @@ let receive_confidential_proof #invs #a tr higher_layer_preds comm_keys_ids rece
 
 val comm_auth_send_event_triggered:
   #a:Type0 -> {|comm_layer_core_config a|} ->
-  trace -> principal -> a ->
+  trace -> principal -> principal -> a ->
   prop
-let comm_auth_send_event_triggered #a tr sender payload =
-  event_triggered tr sender (CommAuthSendMsg sender payload <: communication_core_event a)
+let comm_auth_send_event_triggered #a tr sender receiver payload =
+  event_triggered tr sender (CommAuthSendMsg sender receiver payload <: communication_core_event a)
 
 val comm_conf_auth_send_event_triggered:
   #a:Type0 -> {|comm_layer_core_config a|} ->
@@ -261,7 +261,7 @@ val sign_message_proof:
       match input with
       | Inl payload -> (
         is_well_formed a (is_publishable tr) payload /\
-        comm_auth_send_event_triggered #a tr sender payload
+        comm_auth_send_event_triggered #a tr sender receiver payload
       )
       | Inr (payload, pk) -> (
         is_publishable tr payload /\
@@ -319,7 +319,7 @@ val send_authenticated_proof:
     trace_invariant tr /\
     has_private_keys_invariant /\
     has_communication_layer_core_predicates higher_layer_preds /\
-    higher_layer_preds.send_auth tr sender payload /\
+    higher_layer_preds.send_auth tr sender receiver payload /\
     is_well_formed a (is_publishable tr) payload
   )
   (ensures (
@@ -336,9 +336,9 @@ let send_authenticated_proof #invs #a tr higher_layer_preds comm_keys_ids sender
   | (Some _, tr_out) -> (
     let (Some sk_sender, tr') = get_private_key sender comm_keys_ids.private_keys (LongTermSigKey (comm_layer_sign_tag a)) tr in
     let (nonce,  tr') = mk_rand SigNonce (long_term_key_label sender) 32 tr' in
-    higher_layer_preds.send_auth_later tr tr' sender payload;
-    let ((), tr') = trigger_event sender (CommAuthSendMsg sender payload <: communication_core_event a) tr' in
-    assert(comm_auth_send_event_triggered tr' sender payload);
+    higher_layer_preds.send_auth_later tr tr' sender receiver payload;
+    let ((), tr') = trigger_event sender (CommAuthSendMsg sender receiver payload <: communication_core_event a) tr' in
+    assert(comm_auth_send_event_triggered tr' sender receiver payload);
     sign_message_proof #invs.crypto_invs #a tr' sender receiver (Inl payload) sk_sender nonce;
     let msg_signed = sign_message #a sender receiver (Inl payload) sk_sender nonce in
     let (msg_id, tr') = send_msg msg_signed tr' in
@@ -375,7 +375,7 @@ val verify_message_proof:
           (
             sender == sender' /\
             receiver == receiver' /\
-            comm_auth_send_event_triggered tr sender (Inl?.v payload) \/ 
+            comm_auth_send_event_triggered tr sender receiver (Inl?.v payload) \/ 
             is_corrupt tr (long_term_key_label sender)
           )
         )

src/lib/communication/DY.Lib.Communication.Core.Properties.fst

@@ -78,7 +78,7 @@ val sender_authentication:
     event_triggered_at tr i receiver (CommAuthReceiveMsg sender receiver payload <: communication_core_event a)
   )
   (ensures
-    event_triggered (prefix tr i) sender (CommAuthSendMsg sender payload <: communication_core_event a) \/
+    event_triggered (prefix tr i) sender (CommAuthSendMsg sender receiver payload <: communication_core_event a) \/
     is_corrupt (prefix tr i) (long_term_key_label sender)
   )
 let sender_authentication #tag #invs #a tr i higher_layer_preds sender receiver secret = ()

src/lib/communication/DY.Lib.Communication.Core.fst

@@ -34,7 +34,7 @@ let comm_label sender receiver = join (principal_label sender) (principal_label
 type communication_core_event (a:Type) {|config:comm_layer_core_config a|} =
   | CommConfSendMsg: sender:principal -> receiver:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> communication_core_event a
   | CommConfReceiveMsg: receiver:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> communication_core_event a
-  | CommAuthSendMsg: sender:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> communication_core_event a
+  | CommAuthSendMsg: sender:principal -> receiver:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> communication_core_event a
   | CommAuthReceiveMsg: sender:principal -> receiver:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> communication_core_event a
   | CommConfAuthSendMsg: sender:principal -> receiver:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> communication_core_event a
   | CommConfAuthReceiveMsg: sender:principal -> receiver:principal -> [@@@ with_parser #bytes config.core_ps_a] payload:a -> communication_core_event a
@@ -129,7 +129,7 @@ val send_authenticated:
 let send_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* nonce = mk_rand SigNonce (long_term_key_label sender) 32 in
-  trigger_event sender (CommAuthSendMsg sender payload <: communication_core_event a);*
+  trigger_event sender (CommAuthSendMsg sender receiver payload <: communication_core_event a);*
   let msg_signed = sign_message sender receiver (Inl payload) sk_sender nonce in
   let* msg_id = send_msg msg_signed in
   return (Some msg_id)

src/lib/communication/DY.Lib.Communication.Printing.fst

@@ -91,9 +91,9 @@ let com_core_event_to_string #a payload_to_string =
     | CommConfReceiveMsg receiver payload ->
       Some (Printf.sprintf "CommConfReceiveMsg receiver = %s, payload = (%s)"
         receiver (payload_to_string payload))
-    | CommAuthSendMsg sender payload ->
-      Some (Printf.sprintf "CommAuthSendMsg sender = %s, payload = (%s)"
-        sender (payload_to_string payload))
+    | CommAuthSendMsg sender receiver payload ->
+      Some (Printf.sprintf "CommAuthSendMsg sender = %s, receiver = %s, payload = (%s)"
+        sender receiver (payload_to_string payload))
     | CommAuthReceiveMsg sender receiver payload -> 
       Some (Printf.sprintf "CommAuthReceiveMsg sender = %s, receiver = %s, payload = (%s)"
         sender receiver (payload_to_string payload))