Encapsulate all com messages in com_message_t type. This is needed fo…

…r a meaning full trace printing function; Com Layer trace printing functions

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

@@ -9,6 +9,7 @@ open DY.Lib.Event.Typed
 open DY.Lib.State.PrivateKeys
 open DY.Lib.State.Tagged
 
+open DY.Lib.Communication.Data
 open DY.Lib.Communication.Core
 
 #set-options "--fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'"

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

@@ -8,6 +8,7 @@ open DY.Lib.State.PKI
 open DY.Lib.State.PrivateKeys
 open DY.Lib.Event.Typed
 
+open DY.Lib.Communication.Data
 open DY.Lib.Communication.Core
 open DY.Lib.Communication.Core.Invariants
 
@@ -203,19 +204,19 @@ let sign_message_proof #cinvs #a tr sender receiver payload pk_receiver sk_sende
     let sig_input_bytes = serialize signature_input sig_input in
     serialize_wf_lemma signature_input (is_publishable tr) sig_input;
     let signature = sign sk_sender nonce sig_input_bytes in
-    let msg_signed = {msg=sig_input_bytes; signature} in
+    let msg_signed = SigMessage {msg=sig_input_bytes; signature} in
     assert(bytes_invariant tr signature);
-    serialize_wf_lemma signed_communication_message (is_publishable tr) msg_signed;
+    serialize_wf_lemma com_message_t (is_publishable tr) msg_signed;
     ()
   )
   | Some pk -> (
     let sig_input = Encrypted sender receiver payload_bytes pk in
     let sig_input_bytes = serialize signature_input sig_input in
     serialize_wf_lemma signature_input (is_publishable tr) sig_input;
     let signature = sign sk_sender nonce sig_input_bytes in
-    let msg_signed = {msg=sig_input_bytes; signature} in
+    let msg_signed = SigMessage {msg=sig_input_bytes; signature} in
     assert(bytes_invariant tr signature);
-    serialize_wf_lemma signed_communication_message (is_publishable tr) msg_signed;
+    serialize_wf_lemma com_message_t (is_publishable tr) msg_signed;
     ()
   )
 
@@ -275,7 +276,8 @@ val verify_message_proof:
   (ensures (
     match verify_message #a receiver msg_bytes sk_receiver_opt vk_sender with
     | Some cm -> (
-      let Some msg_signed = parse signed_communication_message #parseable_serializeable_bytes_signed_communication_message msg_bytes in
+      let Some msg_signed_t = parse com_message_t msg_bytes in
+      let SigMessage msg_signed = msg_signed_t in
       let Some sign_input = parse signature_input #parseable_serializeable_bytes_signature_input msg_signed.msg in
       let payload_bytes = serialize a cm.payload in
 
@@ -311,8 +313,9 @@ let verify_message_proof #cinvs #a #ps tr sender receiver msg_bytes sk_receiver_
   match verify_message #a receiver msg_bytes sk_receiver_opt vk_sender with
   | None -> ()
   | Some cm -> (
-    parse_wf_lemma signed_communication_message #parseable_serializeable_bytes_signed_communication_message (is_publishable tr) msg_bytes;
-    let Some msg_signed = parse signed_communication_message #parseable_serializeable_bytes_signed_communication_message msg_bytes in
+    parse_wf_lemma com_message_t (is_publishable tr) msg_bytes;
+    let Some msg_signed_t = parse com_message_t msg_bytes in
+    let SigMessage msg_signed = msg_signed_t in
     parse_wf_lemma signature_input #parseable_serializeable_bytes_signature_input (is_publishable tr) msg_signed.msg;
     let Some sign_input = parse signature_input #parseable_serializeable_bytes_signature_input msg_signed.msg in
 
@@ -481,7 +484,8 @@ let verify_and_decrypt_message_proof #cinvs #a tr sender receiver msg_encrypted_
     verify_message_proof #cinvs #com_send_byte tr sender receiver msg_encrypted_signed (Some sk_receiver) vk_sender;
     let Some cm' = verify_message #com_send_byte receiver msg_encrypted_signed (Some sk_receiver) vk_sender in
 
-    let Some msg_signed = parse signed_communication_message msg_encrypted_signed in
+    let Some msg_signed_t = parse com_message_t msg_encrypted_signed in
+    let SigMessage msg_signed = msg_signed_t in
     let Some sign_input = parse signature_input msg_signed.msg in
     let Encrypted _ _ _ pk_receiver = sign_input in
     assert(pk_receiver == pk sk_receiver);

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

@@ -6,57 +6,9 @@ open DY.Lib.State.PKI
 open DY.Lib.State.PrivateKeys
 open DY.Lib.Event.Typed
 
-#set-options "--fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'"
-
-(*** Messages ***)
-
-/// The following type is meant to be used to send a single byte with a function
-/// of the communication layer. Since the communication layer always takes a
-/// serializable data object we need to encapsulate the byte in a data object.
-[@@with_bytes bytes]
-type com_send_byte = {
-  b:bytes;
-}
-
-%splice [ps_com_send_byte] (gen_parser (`com_send_byte))
-%splice [ps_com_send_byte_is_well_formed] (gen_is_well_formed_lemma (`com_send_byte))
-
-instance parseable_serializeable_bytes_com_send_byte: parseable_serializeable bytes com_send_byte
-  = mk_parseable_serializeable ps_com_send_byte
-
-
-/// Data structure to return data from communication layer functions
-type communication_message (a:Type) = {
-  sender:principal;
-  receiver:principal;  
-  payload:a;
-}
-
-[@@with_bytes bytes]
-type signature_input = 
-  | Plain: sender:principal -> receiver:principal -> payload:bytes -> signature_input
-  | Encrypted: sender:principal -> receiver:principal -> payload:bytes -> pk:bytes -> signature_input
-
-#push-options "--ifuel 1 --fuel 0"
-%splice [ps_signature_input] (gen_parser (`signature_input))
-%splice [ps_signature_input_is_well_formed] (gen_is_well_formed_lemma (`signature_input))
-#pop-options
-
-instance parseable_serializeable_bytes_signature_input: parseable_serializeable bytes signature_input
-  = mk_parseable_serializeable ps_signature_input
-
-[@@with_bytes bytes]
-type signed_communication_message = {
-  msg:bytes;
-  signature:bytes;
-}
-
-%splice [ps_signed_communication_message] (gen_parser (`signed_communication_message))
-%splice [ps_signed_communication_message_is_well_formed] (gen_is_well_formed_lemma (`signed_communication_message))
-
-instance parseable_serializeable_bytes_signed_communication_message: parseable_serializeable bytes signed_communication_message
-  = mk_parseable_serializeable ps_signed_communication_message
+open DY.Lib.Communication.Data
 
+#set-options "--fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'"
 
 (*** Events ***)
 
@@ -157,8 +109,8 @@ let sign_message #a sender receiver payload pk_receiver sk nonce =
   ) in
   let sig_input_bytes = serialize signature_input sig_input in
   let signature = sign sk nonce sig_input_bytes in
-  let signed_msg = {msg=sig_input_bytes; signature} in
-  serialize signed_communication_message signed_msg
+  let signed_msg = SigMessage {msg=sig_input_bytes; signature} in
+  serialize com_message_t signed_msg
 #pop-options
 
 val send_authenticated:
@@ -180,7 +132,9 @@ val verify_message:
   #a:Type -> {| parseable_serializeable bytes a |} ->
   principal -> bytes -> option bytes -> bytes -> option (communication_message a)
 let verify_message #a receiver sign_msg_bytes sk_receiver_opt vk_sender =
-  let? msg_sign = parse signed_communication_message sign_msg_bytes in
+  let? msg_sign_t = parse com_message_t sign_msg_bytes in
+  guard (SigMessage? msg_sign_t);?
+  let SigMessage msg_sign = msg_sign_t in
   let? sign_input = parse signature_input msg_sign.msg in
   guard (verify vk_sender msg_sign.msg msg_sign.signature);?
   let? (pk_receiver_opt, cm) = match sign_input with
@@ -198,8 +152,10 @@ let verify_message #a receiver sign_msg_bytes sk_receiver_opt vk_sender =
   Some cm
 
 val get_sender: bytes -> option principal
-let get_sender msg_bytes =
-  let? msg_sign = parse signed_communication_message msg_bytes in
+let get_sender sign_msg_bytes =
+  let? msg_sign_t = parse com_message_t sign_msg_bytes in
+  guard (SigMessage? msg_sign_t);?
+  let SigMessage msg_sign = msg_sign_t in
   let? sign_input = parse signature_input msg_sign.msg in
   match sign_input with
   | Plain sender receiver payload_bytes -> Some sender
@@ -215,7 +171,7 @@ let receive_authenticated #a comm_keys_ids receiver msg_id =
   let*? msg_signed_bytes = recv_msg msg_id in
   let*? sender = return (get_sender msg_signed_bytes) in
   let*? vk_sender = get_public_key receiver comm_keys_ids.pki (LongTermSigKey comm_layer_sign_tag) sender in
-  let*? cm = return (verify_message receiver msg_signed_bytes None vk_sender) in
+  let*? cm:communication_message a = return (verify_message receiver msg_signed_bytes None vk_sender) in
   trigger_event receiver (CommAuthReceiveMsg sender receiver (serialize a cm.payload));*
   return (Some cm)
 
@@ -253,9 +209,9 @@ val verify_and_decrypt_message:
   #a:Type -> {| parseable_serializeable bytes a |} ->
   principal -> bytes -> bytes -> bytes -> option (communication_message a)
 let verify_and_decrypt_message #a #ps receiver sk_receiver vk_sender msg_encrypted_signed =
-  let? cm = verify_message #com_send_byte receiver msg_encrypted_signed (Some sk_receiver) vk_sender in
-  let? payload = decrypt_message #a sk_receiver cm.payload.b in
-  Some ({cm with payload})
+  let? cm:communication_message com_send_byte = verify_message #com_send_byte receiver msg_encrypted_signed (Some sk_receiver) vk_sender in
+  let? payload:a = decrypt_message #a sk_receiver cm.payload.b in
+  Some {sender=cm.sender; receiver=cm.receiver; payload}
 
 val receive_confidential_authenticated:
   #a:Type -> {| parseable_serializeable bytes a |} ->
@@ -267,7 +223,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) in
   let*? sender = return (get_sender msg_encrypted_signed) in
   let*? vk_sender = get_public_key receiver comm_keys_ids.pki (LongTermSigKey comm_layer_sign_tag) sender in 
-  let*? cm = return (verify_and_decrypt_message #a receiver sk_receiver vk_sender msg_encrypted_signed) in 
+  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 (serialize a cm.payload));*
   return (Some cm)
 

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

@@ -0,0 +1,103 @@
+module DY.Lib.Communication.Data
+
+open Comparse
+open DY.Core
+open DY.Lib.Comparse.Glue
+open DY.Lib.Comparse.Parsers
+
+#set-options "--fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'"
+
+(*** Messages ***)
+
+(**** Core ****)
+
+/// The following type is meant to be used to send a single byte with a function
+/// of the communication layer. Since the communication layer always takes a
+/// serializable data object we need to encapsulate the byte in a data object.
+[@@with_bytes bytes]
+type com_send_byte = {
+  b:bytes;
+}
+
+%splice [ps_com_send_byte] (gen_parser (`com_send_byte))
+%splice [ps_com_send_byte_is_well_formed] (gen_is_well_formed_lemma (`com_send_byte))
+
+instance parseable_serializeable_bytes_com_send_byte: parseable_serializeable bytes com_send_byte
+  = mk_parseable_serializeable ps_com_send_byte
+
+/// Data structure to return data from communication layer functions
+type communication_message (a:Type) = {
+  sender:principal;
+  receiver:principal;  
+  payload:a;
+}
+
+[@@with_bytes bytes]
+type signature_input = 
+  | Plain: sender:principal -> receiver:principal -> payload:bytes -> signature_input
+  | Encrypted: sender:principal -> receiver:principal -> payload:bytes -> pk:bytes -> signature_input
+
+#push-options "--ifuel 1 --fuel 0"
+%splice [ps_signature_input] (gen_parser (`signature_input))
+%splice [ps_signature_input_is_well_formed] (gen_is_well_formed_lemma (`signature_input))
+#pop-options
+
+instance parseable_serializeable_bytes_signature_input: parseable_serializeable bytes signature_input
+  = mk_parseable_serializeable ps_signature_input
+
+[@@with_bytes bytes]
+type signed_communication_message = {
+  msg:bytes;
+  signature:bytes;
+}
+
+%splice [ps_signed_communication_message] (gen_parser (`signed_communication_message))
+%splice [ps_signed_communication_message_is_well_formed] (gen_is_well_formed_lemma (`signed_communication_message))
+
+(**** Request/Response ****)
+
+[@@with_bytes bytes]
+type request_message = {
+  payload:bytes;
+  key:bytes
+}
+
+%splice [ps_request_message] (gen_parser (`request_message))
+%splice [ps_request_message_is_well_formed] (gen_is_well_formed_lemma (`request_message))
+
+[@@with_bytes bytes]
+type response_envelope = {
+  nonce:bytes;
+  ciphertext:bytes
+}
+
+%splice [ps_response_envelope] (gen_parser (`response_envelope))
+%splice [ps_response_envelope_is_well_formed] (gen_is_well_formed_lemma (`response_envelope))
+
+[@@with_bytes bytes]
+type authenticated_data = {
+  server:principal
+}
+
+%splice [ps_authenticated_data] (gen_parser (`authenticated_data))
+%splice [ps_authenticated_data_is_well_formed] (gen_is_well_formed_lemma (`authenticated_data))
+
+instance parseable_serializeable_bytes_authenticated_data: parseable_serializeable bytes authenticated_data
+  = mk_parseable_serializeable ps_authenticated_data
+
+
+(**** Message Type for all Messages on the Wire ****)
+
+[@@with_bytes bytes]
+type com_message_t =
+  | SigMessage: signed_communication_message -> com_message_t
+  | RequestMessage: request_message -> com_message_t
+  | ResponseMessage: response_envelope -> com_message_t
+
+#push-options "--ifuel 1"
+%splice [ps_com_message_t] (gen_parser (`com_message_t))
+%splice [ps_com_message_t_is_well_formed] (gen_is_well_formed_lemma (`com_message_t))
+#pop-options
+
+instance parseable_serializeable_bytes_com_message_t: parseable_serializeable bytes com_message_t
+  = mk_parseable_serializeable ps_com_message_t

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

@@ -4,54 +4,54 @@ open Comparse
 open DY.Core
 
 open DY.Lib.Printing
+open DY.Lib.Communication.Data
 open DY.Lib.Communication.Core
 open DY.Lib.Communication.RequestResponse
 
 #set-options "--fuel 0 --ifuel 1 --z3cliopt 'smt.qi.eager_threshold=100'"
 
 val com_message_to_string: (bytes -> option string) -> (bytes -> option string) -> bytes -> option string
 let com_message_to_string core_payload_to_string reqres_payload_to_string b =
-  match parse signed_communication_message b with
-  | Some scm -> (
-    match parse signature_input scm.msg with
-    | Some si -> (
-      let sender, receiver, payload = (
-        match si with
-        | Plain sender receiver payload -> sender, receiver, payload
-        | Encrypted sender receiver payload _ -> sender, receiver, (
-          match payload with
-          | PkeEnc pk nonce msg -> msg
-          | _ -> empty
-        )
-      ) in
-      Some (Printf.sprintf "msg = (%s, %s, (%s)), signature = sig(sk_{%s}, msg)" sender receiver (option_to_string core_payload_to_string payload) sender)
-    )
-    | None -> Some "Error: signed_communication_message does not contain a signature_input"
+  match b with
+  | PkeEnc pk nonce msg -> (
+    match parse com_message_t b with
+    | Some (SigMessage _) -> Some "Error: SigMessage cannot be inside a PkeEnc encryption"
+    | Some (RequestMessage {payload; key}) ->
+      Some (Printf.sprintf "Request payload = (%s), key = %s" 
+        (option_to_string reqres_payload_to_string payload) (bytes_to_string key))
+    | Some (ResponseMessage _) -> Some "Error: ResponseMessage cannot be inside a PkeEnc encryption"
+    | None -> Some (option_to_string core_payload_to_string b)
   )
-  | None -> (
-    match b with
-    | PkeEnc pk nonce msg -> (
-      match parse request_message b with
-      | Some {payload; key} ->
-        Some (Printf.sprintf "Request payload = (%s), key = %s" 
-          (option_to_string reqres_payload_to_string payload) (bytes_to_string key))
-      | None -> Some (option_to_string core_payload_to_string b)
-    )
-    | _ -> (
-      match parse response_envelope b with
-        | Some {nonce; ciphertext} -> (
-          match ciphertext with
-          | AeadEnc key nonce msg ad -> (
-            Some (Printf.sprintf "Response payload = (%s)"
-              (option_to_string reqres_payload_to_string msg))
+  | _ -> (
+    match parse com_message_t b with
+    | Some (SigMessage {msg; signature}) -> (
+      match parse signature_input msg with
+      | Some si -> (
+        let sender, receiver, payload = (
+          match si with
+          | Plain sender receiver payload -> sender, receiver, payload
+          | Encrypted sender receiver payload _ -> sender, receiver, (
+            match payload with
+            | PkeEnc pk nonce msg -> msg
+            | _ -> empty
           )
-          | _ -> Some "Error: response_envelope does not contain an AEAD ciphertext"
-        )
-        | None -> Some "Error not a communication layer message"
+        ) in
+        Some (Printf.sprintf "msg = (%s, %s, (%s)), signature = sig(sk_{%s}, msg)" sender receiver (option_to_string core_payload_to_string payload) sender)
+      )
+      | None -> Some "Error: signed_communication_message does not contain a signature_input"
     )
+    | Some (RequestMessage _) -> Some "Error: RequestMessage cannot be send in plaintext"
+    | Some (ResponseMessage {nonce; ciphertext}) -> (
+      match ciphertext with
+      | AeadEnc key nonce msg ad -> (
+        Some (Printf.sprintf "Response payload = (%s)"
+          (option_to_string reqres_payload_to_string msg))
+      )
+      | _ -> Some "Error: response_envelope does not contain an AEAD ciphertext"
+    )
+    | None -> Some "Error not a communication layer message"
   )
 
-
 val com_core_event_to_string: (bytes -> option string) -> (string & (bytes -> option string))
 let com_core_event_to_string payload_to_string =
   (event_communication_event.tag, (fun b -> (