Feedback

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

@@ -21,7 +21,7 @@ let pke_crypto_predicates_communication_layer #cusages = {
   pred = (fun tr sk_usage pk msg ->
     (exists sender receiver.
       sk_usage == long_term_key_type_to_usage (LongTermPkeKey comm_layer_pkenc_tag)  receiver /\
-      (get_label tr msg) `can_flow tr` (join (principal_label sender) (principal_label receiver)) /\
+      (get_label tr msg) `can_flow tr` (comm_label sender receiver) /\
       event_triggered tr sender (CommConfSendMsg sender receiver msg)
     )
     );
@@ -136,15 +136,15 @@ let event_predicate_communication_layer
   fun tr prin e ->
     (match e with
     | CommConfSendMsg sender receiver payload -> (
-      is_knowable_by (join (principal_label sender) (principal_label receiver)) tr payload /\
+      is_knowable_by (comm_label sender receiver) tr payload /\
       (match parse a payload with
       | None -> False
       | Some payload_p -> higher_layer_preds.send_conf tr sender receiver payload_p
-      )      
+      )
     )
     | CommConfReceiveMsg receiver payload -> (
       exists sender.
-        is_knowable_by (join (principal_label sender) (principal_label receiver)) tr payload /\
+        //is_knowable_by (comm_label sender receiver) tr payload /\
         (
           event_triggered tr sender (CommConfSendMsg sender receiver payload) \/
           is_publishable tr payload
@@ -164,15 +164,15 @@ let event_predicate_communication_layer
       )
     )
     | CommConfAuthSendMsg sender receiver payload -> (
-      is_knowable_by (join (principal_label sender) (principal_label receiver)) tr payload /\
+      is_knowable_by (comm_label sender receiver) tr payload /\
       (match parse a payload with
       | None -> False
       | Some payload_p -> higher_layer_preds.send_conf_auth tr sender receiver payload_p
       )
     )
     | CommConfAuthReceiveMsg sender receiver payload -> (
       // We can only show the following about the decrypted ciphertext (payload):
-      // is_knowable_by (join (principal_label sender) (principal_label receiver)) tr payload \/
+      // is_knowable_by (comm_label sender receiver) tr payload \/
       // is_corrupt tr (principal_label sender)
       // There are two cases how the ciphertext is created:
       // 1. The corrupted sender created the ciphertext. This means that the

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

@@ -133,16 +133,20 @@ val receive_confidential_proof:
     | (None, tr_out) -> trace_invariant tr_out
     | (Some payload, tr_out) -> ( 
       trace_invariant tr_out /\
-      (exists sender. is_well_formed a (is_knowable_by (comm_label sender receiver) tr) payload /\
-      // We explicitly do not use `event_triggered tr receiver
-      // (CommConfReceiveMsg receiver (serialize a payload))` as a
-      // post-condition here. The reason for the following form of the
-      // post-condition is that it allows us on the higher layer to assert a
-      // statement `b` contained in the `higher_layer_preds` that depends on
-      // some field `field1` of the payload in the following way: `b
-      // payload.field1 \/ is_publishable tr payload.field1`.
-      (event_triggered tr sender (CommConfSendMsg sender receiver (serialize a payload)) \/ 
-        is_well_formed a (is_publishable tr) payload)
+      (
+        (exists sender.
+          is_well_formed a (is_knowable_by (comm_label sender receiver) tr) payload /\
+          // We explicitly do not use `event_triggered tr receiver
+          // (CommConfReceiveMsg receiver (serialize a payload))` as a
+          // post-condition here. The reason for the following form of the
+          // post-condition is that it allows us on the higher layer to assert a
+          // statement `b` contained in the `higher_layer_preds` that depends on
+          // some field `field1` of the payload in the following way: `b
+          // payload.field1 \/ is_publishable tr payload.field1`.
+          event_triggered tr sender (CommConfSendMsg sender receiver (serialize a payload))
+        ) \/ (
+          is_well_formed a (is_publishable tr) payload
+        )
       )
     )
   ))

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

@@ -59,8 +59,8 @@ val sender_confauth_authentication:
     event_triggered_at tr i receiver (CommConfAuthReceiveMsg sender receiver payload)
   )
   (ensures
-    event_triggered tr sender (CommConfAuthSendMsg sender receiver payload) \/
-    is_corrupt tr (long_term_key_label sender)
+    event_triggered (prefix tr i) sender (CommConfAuthSendMsg sender receiver payload) \/
+    is_corrupt (prefix tr i) (long_term_key_label sender)
   )
 let sender_confauth_authentication #invs #a tr i higher_layer_preds sender receiver secret = ()