Merge branch 'fabian-hk/development' of github.com:REPROSEC/dolev-yao-star-extrinsic into fabian-hk/development

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.Data.fst

@@ -93,6 +93,8 @@ type response_envelope = {
 
 [@@with_bytes bytes]
 type authenticated_data = {
+  [@@@ with_parser #bytes (ps_option ps_principal)]
+  client:option principal;
   server:principal
 }
 

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

@@ -77,6 +77,13 @@ let comm_message_to_string #core_type #core_config #reqres_type #reqres_config m
     | None -> Some (other_messages_to_string b)
   )
 
+// TODO: This should be moved to the printing library
+val option_to_string: (#a:Type0) -> (a -> string) -> option a -> string
+let option_to_string #a to_string opt =
+  match opt with
+  | Some x -> Printf.sprintf "Some (%s)" (to_string x)
+  | None -> "None"
+
 val com_core_event_to_string:
   #a:Type0 -> {|comm_layer_core_config a|} ->
   (a -> string) ->
@@ -91,9 +98,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))
@@ -113,21 +120,21 @@ let com_reqres_event_to_string #a payload_to_string =
   ((event_communication_reqres_event #a).tag, (fun b -> (
     let? cre = parse (communication_reqres_event a) b in
     match cre with
-    | CommClientSendRequest client server request key -> (
-      Some (Printf.sprintf "CommClientSendRequest client = %s, server = %s, request = (%s)"
-        client server (payload_to_string request))
+    | CommClientSendRequest authenticated client server request key -> (
+      Some (Printf.sprintf "CommClientSendRequest authenticated = %b, client = %s, server = %s, request = (%s)"
+        authenticated client server (payload_to_string request))
     )
-    | CommServerReceiveRequest server request key -> (
-      Some (Printf.sprintf "CommServerReceiveRequest server = %s, request = (%s), key = %s"
-        server (payload_to_string request) (bytes_to_string key))
+    | CommServerReceiveRequest client server request key -> (
+      Some (Printf.sprintf "CommServerReceiveRequest client = %s, server = %s, request = (%s), key = %s"
+        (option_to_string (fun s -> s) client) server (payload_to_string request) (bytes_to_string key))
     )
-    | CommServerSendResponse server request response key -> (
-      Some (Printf.sprintf "CommServerSendResponse server = %s, request = %s, response = (%s), key = %s"
-        server (payload_to_string request) (payload_to_string response) (bytes_to_string key))
+    | CommServerSendResponse client server request response key -> (
+      Some (Printf.sprintf "CommServerSendResponse client = %s, server = %s, request = %s, response = (%s), key = %s"
+        (option_to_string (fun s -> s) client) server (payload_to_string request) (payload_to_string response) (bytes_to_string key))
     )
-    | CommClientReceiveResponse client server request response key -> (
-      Some (Printf.sprintf "CommClientReceiveResponse client = %s, server = %s, response = (%s), key = %s" 
-        client server (payload_to_string response) (bytes_to_string key))
+    | CommClientReceiveResponse authenticated client server request response key -> (
+      Some (Printf.sprintf "CommClientReceiveResponse authenticated = %b, client = %s, server = %s, response = (%s), key = %s" 
+        authenticated client server (payload_to_string response) (bytes_to_string key))
     )
   )))
 

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

@@ -29,18 +29,18 @@ let aead_crypto_predicate_communication_layer_reqres #cusages a #config = {
   pred = (fun tr key_usage key nonce msg ad ->
       (match parse authenticated_data ad with
       | None -> False
-      | Some {server} -> (exists request.
+      | Some {client; server} -> (exists request.
         match parse a msg with
         | None -> False
         | Some response ->
-          event_triggered tr server (CommServerSendResponse server request response key <: communication_reqres_event a)
+          event_triggered tr server (CommServerSendResponse client server request response key <: communication_reqres_event a)
       )
     )
   );
   pred_later = (fun tr1 tr2 key_usage key nonce msg ad -> (
     match parse authenticated_data ad with
     | None -> assert(False)
-    | Some {server} -> ()
+    | Some {client; server} -> ()
   ))
 }
 #pop-options
@@ -93,10 +93,10 @@ let state_predicate_communication_layer_reqres {|crypto_invariants|} (a:Type) {|
       is_secret (comm_label client server) tr key /\
       key `has_usage tr` (AeadKey (comm_layer_aead_tag a) empty)
     )
-    | ServerReceiveRequest {request; key} -> (
+    | ServerReceiveRequest {client; request; key} -> (
       let server = prin in
       is_knowable_by (principal_label server) tr key /\
-      is_well_formed a (is_knowable_by (principal_label server) tr) request /\
+      is_well_formed a (is_knowable_by (get_label tr key) tr) request /\
       key `has_usage tr` (AeadKey (comm_layer_aead_tag a) empty)
     )
     | ClientReceiveResponse {server; response; key} -> (
@@ -156,6 +156,20 @@ class comm_reqres_preds (a:Type) {| comm_layer_reqres_config a |} = {
       send_request_pred tr2 client server request key_label
     )
   ;
+  authenticated_request_pred: tr:trace -> client:principal -> server:principal -> request:a -> key_label:label -> prop;
+  authenticated_request_pred_later:
+    tr1:trace -> tr2:trace ->
+    client:principal -> server:principal -> request:a -> key_label:label ->
+    Lemma
+    (requires
+      authenticated_request_pred tr1 client server request key_label /\
+      is_well_formed a (bytes_well_formed tr1) request /\
+      tr1 <$ tr2
+    )
+    (ensures
+      authenticated_request_pred tr2 client server request key_label
+    )
+  ;
   // TODO rename to response_pred
   send_response_pred: tr:trace -> server:principal -> request:a -> response:a -> key_label:label -> prop;
   send_response_pred_later:
@@ -181,35 +195,40 @@ let event_predicate_communication_layer_reqres
   event_predicate (communication_reqres_event a) =
   fun tr prin e ->
     (match e with
-    | CommClientSendRequest client server request key -> (
+    | CommClientSendRequest authenticated client server request key -> (
       rand_just_generated tr key /\
       is_well_formed a (is_knowable_by (get_label tr key) tr) request /\
       is_secret (comm_label client server) tr key /\
       key `has_usage tr` (AeadKey (comm_layer_aead_tag a) empty) /\
       crpreds.send_request_pred tr client server request (get_label tr key)
     )
-    | CommServerReceiveRequest server request key -> (
+    | CommServerReceiveRequest client server request key -> (
       is_knowable_by (principal_label server) tr key /\
       is_well_formed a (is_knowable_by (get_label tr key) tr) request /\
       key `has_usage tr` (AeadKey (comm_layer_aead_tag a) empty) /\
-      (
-        (exists client. event_triggered tr client (CommClientSendRequest client server request key <: communication_reqres_event a)) \/
-        (is_publishable tr key /\ is_well_formed a (is_publishable tr) request)
+      (match client with
+      | None -> (
+        (exists client. event_triggered tr client (CommClientSendRequest Unauthenticated client server request key <: communication_reqres_event a)) \/
+          (is_publishable tr key /\ is_well_formed a (is_publishable tr) request)
       )
+      | Some client -> (
+        event_triggered tr client (CommClientSendRequest Authenticated client server request key <: communication_reqres_event a) \/
+          is_corrupt tr (long_term_key_label client)
+      ))
     )
-    | CommServerSendResponse server request response key -> (
-      event_triggered tr server (CommServerReceiveRequest server request key <: communication_reqres_event a) /\
+    | CommServerSendResponse client server request response key -> (
+      event_triggered tr server (CommServerReceiveRequest client server request key <: communication_reqres_event a) /\
       is_well_formed a (bytes_well_formed tr) request /\
       is_well_formed a (bytes_well_formed tr) response /\
       bytes_well_formed tr key /\
       crpreds.send_response_pred tr server request response (get_label tr key)
     )
-    | CommClientReceiveResponse client server request response key -> (
-      is_well_formed a (is_knowable_by (get_label tr key) tr) response /\
-      is_secret (comm_label client server) tr key /\
-      event_triggered tr client (CommClientSendRequest client server request key <: communication_reqres_event a) /\
-      (event_triggered tr server (CommServerSendResponse server request response key <: communication_reqres_event a) \/
-      (is_publishable tr key /\ is_well_formed a (is_publishable tr) response))
+    | CommClientReceiveResponse client response req_meta_data -> (
+      is_well_formed a (is_knowable_by (comm_label client req_meta_data.server) tr) response /\
+      is_secret (comm_label client req_meta_data.server) tr req_meta_data.key /\
+      event_triggered tr client (CommClientSendRequest (request_authenticated req_meta_data) client req_meta_data.server req_meta_data.request req_meta_data.key <: communication_reqres_event a) /\
+      (event_triggered tr req_meta_data.server (CommServerSendResponse req_meta_data.client req_meta_data.server req_meta_data.request response req_meta_data.key <: communication_reqres_event a) \/
+      is_corrupt tr (principal_label client) \/ is_corrupt tr (principal_label req_meta_data.server))
     )
     )
 #pop-options
@@ -225,12 +244,19 @@ let comm_core_higher_layer_event_preds_reqres #cinvs a #config = {
   send_conf = (fun tr client server (com_msg_t:comm_message_t) ->
     match com_msg_t with
     | RequestMessage {request; key} -> (
-      parse_and_pred (fun request_parsed -> event_triggered tr client (CommClientSendRequest client server request_parsed key <: communication_reqres_event a)) request
+      parse_and_pred (fun request_parsed -> event_triggered tr client (CommClientSendRequest Unauthenticated client server request_parsed key <: communication_reqres_event a)) request
+    )
+    | _ -> False
+  );
+  send_conf_later = (fun tr1 tr2 client server msg -> ());
+  send_conf_auth = (fun tr client server (com_msg_t:comm_message_t) ->
+    match com_msg_t with
+    | RequestMessage {request; key} -> (
+      parse_and_pred (fun request_parsed -> event_triggered tr client (CommClientSendRequest Authenticated client server request_parsed key <: communication_reqres_event a)) request
     )
     | _ -> False
   );
-  send_conf_later = (fun tr1 tr2 client server msg -> ()
-  )
+  send_conf_auth_later = (fun tr1 tr2 client server msg -> ());
 }
 #pop-options