feat:Communication Layer

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

@@ -8,6 +8,7 @@ open DY.Lib.Crypto.AEAD.Split
 open DY.Lib.Event.Typed
 open DY.Lib.State.PrivateKeys
 open DY.Lib.State.Tagged
+open DY.Lib.Comparse.DYUtils
 
 open DY.Lib.Communication.Data
 open DY.Lib.Communication.Core
@@ -128,34 +129,29 @@ let default_comm_higher_layer_event_preds (a:Type) {| parseable_serializeable by
 }
 
 #push-options "--ifuel 1 --fuel 0"
-let event_predicate_communication_layer 
+let event_predicate_communication_layer
   {|cinvs:crypto_invariants|}
   (#a:Type) {| parseable_serializeable bytes a |}
-  (higher_layer_preds:comm_higher_layer_event_preds a) : 
+  (higher_layer_preds:comm_higher_layer_event_preds a) :
   event_predicate communication_event =
   fun tr prin e ->
     (match e with
     | CommConfSendMsg sender receiver 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
-      )
+      parse_and_pred (higher_layer_preds.send_conf tr sender receiver) payload
     )
     | CommConfReceiveMsg receiver payload -> (
-      exists sender.
-        (
-          event_triggered tr sender (CommConfSendMsg sender receiver payload) \/
-          is_publishable tr payload
-        )
+      Some? (parse a payload) /\
+      (
+        (exists sender. event_triggered tr sender (CommConfSendMsg sender receiver payload)) \/
+        is_publishable tr payload
+      )
     )
     | CommAuthSendMsg sender payload -> (
-      (match parse a payload with
-      | None -> False
-      | Some payload_p -> higher_layer_preds.send_auth tr sender payload_p
-      )
+      parse_and_pred (higher_layer_preds.send_auth tr sender) payload
     )
     | CommAuthReceiveMsg sender receiver payload -> (
+      Some? (parse a payload) /\
       is_publishable tr payload /\
       (
         event_triggered tr sender (CommAuthSendMsg sender payload) \/
@@ -164,10 +160,7 @@ let event_predicate_communication_layer
     )
     | CommConfAuthSendMsg sender receiver 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
-      )
+      parse_and_pred (higher_layer_preds.send_conf_auth tr sender receiver) payload
     )
     | CommConfAuthReceiveMsg sender receiver payload -> (
       // We can only show the following about the decrypted ciphertext (payload):
@@ -180,13 +173,16 @@ let event_predicate_communication_layer
       // 2. The corrupted sender takes a ciphertext from an honest principal.
       //    Since the crypto predicates apply to this ciphertext, the
       //    decrypted payload flows to the receiver and some unknown sender'.
-      event_triggered tr sender (CommConfAuthSendMsg sender receiver payload) \/
-      is_corrupt tr (long_term_key_label sender)
+      Some? (parse a payload) /\
+      (
+        event_triggered tr sender (CommConfAuthSendMsg sender receiver payload) \/
+        is_corrupt tr (long_term_key_label sender)
+      )
     )
     )
 #pop-options
 
-val event_predicate_communication_layer_and_tag: 
+val event_predicate_communication_layer_and_tag:
   {|cinvs:crypto_invariants|} ->
   #a:Type -> {| parseable_serializeable bytes a |} ->
   comm_higher_layer_event_preds a ->

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

@@ -123,32 +123,18 @@ val receive_confidential_proof:
   receiver:principal -> msg_id:timestamp ->
   Lemma
   (requires
-    trace_invariant tr /\ 
+    trace_invariant tr /\
     has_private_keys_invariant /\
     has_communication_layer_crypto_predicates /\
     has_communication_layer_event_predicates higher_layer_preds
   )
   (ensures (
     match receive_confidential #a comm_keys_ids receiver msg_id tr with
     | (None, tr_out) -> trace_invariant tr_out
-    | (Some payload, 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
-        )
-      )
-    )
+      event_triggered tr_out receiver (CommConfReceiveMsg receiver (serialize a payload)) /\
+      is_well_formed a (is_knowable_by (principal_label receiver) tr) payload
   ))
 let receive_confidential_proof #invs #a tr higher_layer_preds comm_keys_ids receiver msg_id =
   match receive_confidential #a comm_keys_ids receiver msg_id tr with

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

@@ -8,6 +8,7 @@ open DY.Lib.Event.Typed
 open DY.Lib.State.PKI
 open DY.Lib.State.PrivateKeys
 open DY.Lib.State.Typed
+open DY.Lib.Comparse.DYUtils
 
 open DY.Lib.Communication.Core
 open DY.Lib.Communication.Core.Invariants
@@ -18,6 +19,52 @@ open DY.Lib.Communication.Core.Lemmas
 /// This module contains security properties that can be proven from the
 /// communication layer guarantees.
 
+(*** Confidential Messages Properties ***)
+
+val conf_message_secrecy:
+  {|protocol_invariants|} ->
+  #a:Type -> {| parseable_serializeable bytes a |} ->
+  tr:trace -> i:timestamp ->
+  higher_layer_preds:comm_higher_layer_event_preds a ->
+  receiver:principal ->
+  payload:bytes ->
+  Lemma
+  (requires
+    trace_invariant tr /\
+    has_communication_layer_event_predicates higher_layer_preds /\
+    event_triggered_at tr i receiver (CommConfReceiveMsg receiver payload)
+  )
+  (ensures
+    is_knowable_by (principal_label receiver) (prefix tr i) payload /\
+
+    parse_and_pred (fun payload_parsed ->
+      (exists sender. higher_layer_preds.send_conf (prefix tr i) sender receiver payload_parsed) \/
+      is_well_formed a (is_publishable (prefix tr i)) payload_parsed
+    ) payload
+  )
+let conf_message_secrecy #invs #a tr i higher_layer_preds receiver payload =
+  let send_event sender = CommConfSendMsg sender receiver payload in
+  let tr_i = prefix tr i in
+  eliminate (exists sender. event_triggered tr_i sender (send_event sender)) \/
+            is_publishable tr_i payload
+  returns
+    is_knowable_by (principal_label receiver) tr_i payload /\
+    parse_and_pred (fun payload_parsed ->
+      (exists sender. higher_layer_preds.send_conf (prefix tr i) sender receiver payload_parsed) \/
+      is_well_formed a (is_publishable (prefix tr i)) payload_parsed
+    ) 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);
+
+      serialize_parse_inv_lemma a payload;
+      higher_layer_preds.send_conf_later (prefix tr j) tr_i sender receiver (Some?.v (parse a payload))
+    )
+  and _. parse_wf_lemma a (is_publishable (prefix tr i)) payload
+
+
 (*** Authenticated Messages Properties ***)
 
 val sender_authentication:

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

@@ -9,6 +9,7 @@ open DY.Lib.Event.Typed
 open DY.Lib.State.PrivateKeys
 open DY.Lib.State.Tagged
 open DY.Lib.State.Typed
+open DY.Lib.Comparse.DYUtils
 
 open DY.Lib.Communication.Data
 open DY.Lib.Communication.Core
@@ -70,10 +71,7 @@ let state_predicates_communication_layer {|crypto_invariants|}: local_state_pred
       let server = prin in
       is_knowable_by (principal_label server) tr key /\
       is_knowable_by (get_label tr key) tr request /\
-      (
-        key `has_usage tr` (AeadKey comm_layer_aead_tag empty) \/
-        is_publishable tr key
-      )
+      key `has_usage tr` (AeadKey comm_layer_aead_tag empty)
     )
     | ClientReceiveResponse {server; response; key} -> (
       let client = prin in
@@ -152,23 +150,21 @@ let event_predicate_communication_layer_reqres
       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 empty) /\
-      (match parse a request with
-      | None -> False
-      | Some request -> higher_layer_resreq_preds.send_request tr client server request (get_label tr key))
+      parse_and_pred (fun request -> higher_layer_resreq_preds.send_request tr client server request (get_label tr key)) request
     )
     | CommServerReceiveRequest server request key -> (
-      is_knowable_by (principal_label server) tr request /\
-      (exists client. event_triggered tr client (CommClientSendRequest client server request key) \/
-        is_publishable tr request)
+      is_knowable_by (principal_label server) tr key /\
+      is_knowable_by (get_label tr key) tr request /\
+      key `has_usage tr` (AeadKey comm_layer_aead_tag empty) /\
+      (
+        (exists client. event_triggered tr client (CommClientSendRequest client server request key)) \/
+        is_publishable tr key
+      )
     )
     | CommServerSendResponse server request response -> (
-      (match parse a response with
-      | None -> False
-      | Some response -> (
-        match parse a request with
-        | None -> False
-        | Some request -> higher_layer_resreq_preds.send_response tr server request response)
-      )
+      match parse a request, parse a response with
+      | Some request, Some response -> higher_layer_resreq_preds.send_response tr server request response
+      | _ -> False
     )
     | CommClientReceiveResponse client server response key -> (
       (exists request. event_triggered tr server (CommServerSendResponse server request response)) \/

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

@@ -13,6 +13,7 @@ open DY.Lib.Communication.Data
 open DY.Lib.Communication.Core
 open DY.Lib.Communication.Core.Invariants
 open DY.Lib.Communication.Core.Lemmas
+open DY.Lib.Communication.Core.Properties
 open DY.Lib.Communication.RequestResponse
 open DY.Lib.Communication.RequestResponse.Invariants
 
@@ -117,15 +118,12 @@ val receive_request_proof:
     | (Some (payload, req_meta_data), tr_out) -> (
       let payload_bytes = serialize a payload in
       trace_invariant tr_out /\
-      // See comment on `receive_confidential_proof` for the reason of this form
-      // of the post-condition.
-      (exists client. event_triggered tr_out client (CommClientSendRequest client server payload_bytes req_meta_data.key) \/
-        is_well_formed a (is_publishable tr_out) payload) /\
+      event_triggered tr_out server (CommServerReceiveRequest server payload_bytes req_meta_data.key) /\
       is_well_formed a (is_knowable_by (principal_label server) tr_out) payload /\
-      is_well_formed a (is_knowable_by (get_response_label tr req_meta_data) tr) payload
+      is_well_formed a (is_knowable_by (get_response_label tr_out req_meta_data) tr_out) payload
     )
   ))
-  [SMTPat (trace_invariant tr); 
+  [SMTPat (trace_invariant tr);
   SMTPat (apply_com_layer_lemmas higher_layer_preds);
   SMTPat (receive_request #a comm_keys_ids server msg_id tr)]
 let receive_request_proof #invs #a tr comm_keys_ids higher_layer_preds server msg_id =
@@ -136,13 +134,36 @@ let receive_request_proof #invs #a tr comm_keys_ids higher_layer_preds server ms
     let (Some req_msg_t, tr') = receive_confidential #com_message_t comm_keys_ids server msg_id tr in
     let RequestMessage req_msg = req_msg_t in
 
+    let req_msg_bytes = serialize com_message_t req_msg_t in
+    let req_send_event client = CommClientSendRequest client server req_msg.request req_msg.key in
+
+    let i = find_event_triggered_at_timestamp tr' server (CommConfReceiveMsg server req_msg_bytes) in
+    conf_message_secrecy tr' i request_response_event_preconditions server req_msg_bytes;
+
+    // Properties that can be proved uniformly in both the honest and corrupt case
+    eliminate (exists client. event_triggered tr' client (req_send_event client)) \/
+              (is_publishable tr' req_msg.request /\ is_publishable tr' req_msg.key)
+    returns (
+      is_knowable_by (get_response_label tr' req_meta_data) tr' req_msg.request /\
+      req_msg.key `has_usage tr'` (AeadKey comm_layer_aead_tag empty)
+    )
+    with _. eliminate exists client. event_triggered tr' client (req_send_event client)
+      returns _
+      with _. (
+        let i = find_event_triggered_at_timestamp tr' client (req_send_event client) in
+        // Triggers event_triggered_at_implies_pred
+        assert(event_triggered_at tr' i client (req_send_event client))
+      )
+    and _. has_usage_publishable tr' req_msg.key (AeadKey comm_layer_aead_tag empty);
+
+    // Relating knowledge of the request to knowledge of its fields
     serialize_parse_inv_lemma #bytes a req_msg.request;
-    assert(is_comm_response_payload tr_out server req_meta_data payload);
+    assert(is_comm_response_payload tr' server req_meta_data payload);
 
     let ((), tr') = trigger_event server (CommServerReceiveRequest server req_msg.request req_msg.key) tr' in
     let (sid', tr') = new_session_id server tr' in
     let ((), tr') = set_state server sid' (ServerReceiveRequest {request=req_msg.request; key=req_msg.key} <: communication_states) tr' in
-    assert(tr' == tr_out);    
+    assert(tr' == tr_out);
     assert(trace_invariant tr_out);
     ()
   )
@@ -182,9 +203,7 @@ val compute_response_message_proof:
     is_knowable_by (principal_label server) tr key /\
     is_well_formed a (is_knowable_by (get_label tr key) tr) response /\    
     is_publishable tr nonce /\
-    (key `has_usage tr` (AeadKey comm_layer_aead_tag empty) \/
-      is_publishable tr key    
-    ) /\
+    key `has_usage tr` (AeadKey comm_layer_aead_tag empty) /\
     event_triggered tr server (CommServerSendResponse server request (serialize a response))
   )
   (ensures

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

@@ -120,13 +120,13 @@ val receive_request:
   principal -> timestamp ->
   traceful (option (a & comm_meta_data))
 let receive_request #a comm_keys_ids server msg_id =
-  let*? req_msg_t:com_message_t = receive_confidential #com_message_t comm_keys_ids server msg_id in  
+  let*? req_msg_t:com_message_t = receive_confidential #com_message_t comm_keys_ids server msg_id in
   guard_tr (RequestMessage? req_msg_t);*?
   let RequestMessage req_msg = req_msg_t in
+  let*? request = return (parse a req_msg.request) in
   trigger_event server (CommServerReceiveRequest server req_msg.request req_msg.key);*
   let* sid = new_session_id server in
   set_state server sid (ServerReceiveRequest {request=req_msg.request; key=req_msg.key} <: communication_states);*
-  let*? request = return (parse a req_msg.request) in
   let req_meta_data = {key=req_msg.key; server; sid; request=req_msg.request} in
   return (Some (request, req_meta_data))
 

src/lib/communication/README.md

@@ -39,4 +39,4 @@ The request-response pairs are implemented with the same structure in the
 `DY.Lib.Communication.RequstResponse.*` namespace.
 
 Examples for how to use the communication layer functions
-in a higher layer protocol can be found in this [repository](https://github.com/fabian-hk/dolev-yao-star-communication-layer-examples).
+in a higher layer protocol can be found in this [repository](https://github.com/REPROSEC/dolev-yao-star-communication-layer-examples).

src/lib/comparse/DY.Lib.Comparse.DYUtils.fst

@@ -0,0 +1,23 @@
+module DY.Lib.Comparse.DYUtils
+
+open Comparse
+open DY.Core
+
+open DY.Lib.Comparse.Glue
+open DY.Lib.Comparse.Parsers
+
+/// This module provides some utility functions for working more simply
+/// with parseable bytes (e.g., lifting predicates from abstract types to
+/// their serialized bytes counterparts).
+
+#set-options "--fuel 0 --ifuel 0"
+
+unfold
+val parse_and_pred:
+  #a:Type -> {| parseable_serializeable bytes a |} ->
+  (p:a -> Type0) -> (bytes -> Type0)
+let parse_and_pred #a p = (fun b ->
+  match parse a b with
+  | None -> False
+  | Some x -> p x
+  )