feat: make labels erasable (#54)

* feat: make labels erasable

* add unknown label

* improve user interface of `enable_bytes_well_formed_smtpats`

examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst

@@ -19,7 +19,7 @@ let is_dh_shared_key tr alice bob k = exists si sj.
   // the label is either ``join (principal_state_label alice si) (principal_state_label bob sj)`` or
   // ``join (principal_state_label bob sj) (principal_state_label alice si)``.
   // This is because k is either build from ``dh x (dh_pk y)`` or ``dh y (dh_pk x)``.
-  get_label k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj) /\ 
+  get_label tr k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj) /\ 
   get_usage k == AeadKey "DH.aead_key" empty
 
 let dh_session_pred: local_state_predicate dh_session = {
@@ -277,7 +277,7 @@ let prepare_msg3_proof tr global_sess_id alice alice_si bob msg_id =
               assert(dh y res.gx == dh x res.gy);
               assert(k == k');
 
-              assert(exists si sj. get_label k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj));
+              assert(exists si sj. get_label tr k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj));
 
               assert(dh_key_and_event_respond1);
               ()
@@ -376,7 +376,7 @@ let verify_msg3_proof tr global_sess_id alice bob msg_id bob_si =
             );
 
             assert(is_corrupt tr (principal_label alice) \/
-              (exists si. get_label res.k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob bob_si)));
+              (exists si. get_label tr res.k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob bob_si)));
             assert(get_usage res.k == AeadKey "DH.aead_key" empty);
             assert(is_corrupt tr (principal_label alice) \/
               (is_dh_shared_key tr alice bob res.k /\ event_triggered tr alice (Initiate2 alice bob gx gy res.k)));

examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst

@@ -38,7 +38,7 @@ let dh_crypto_preds = {
   sign_pred = {
     pred = (fun tr vk sig_msg ->
       get_signkey_usage vk == SigKey "DH.SigningKey" empty /\
-      (exists prin. get_signkey_label vk = principal_label prin /\ (
+      (exists prin. get_signkey_label tr vk == principal_label prin /\ (
         match parse sig_message sig_msg with
         | Some (SigMsg2 sig_msg2) -> (
           exists y. sig_msg2.gy == (dh_pk y) /\ event_triggered tr prin (Respond1 sig_msg2.alice prin sig_msg2.gx sig_msg2.gy y)
@@ -87,7 +87,7 @@ let compute_message1_proof tr alice bob x =
   // It just shows what we need to show to prove the lemma.
   let msgb = compute_message1 alice x in 
   assert(bytes_invariant tr msgb);
-  assert(get_label msgb `can_flow tr` public);
+  assert(get_label tr msgb `can_flow tr` public);
   assert(is_publishable tr msgb);
   ()
 
@@ -115,7 +115,7 @@ let decode_message1_proof tr msg1_bytes =
       // The following code is not needed for the proof.
       // It just shows what we need to show to prove the lemma.
       assert(bytes_invariant tr msg1.gx);
-      assert(get_label msg1.gx `can_flow tr` public);
+      assert(get_label tr msg1.gx `can_flow tr` public);
       ()
     )
     | None -> ()
@@ -236,7 +236,7 @@ let compute_message3_proof tr alice bob gx gy x sk_a n_sig =
 
   // The following code is not needed for the proof.
   // It just shows what we need to show to prove the lemma. 
-  assert(get_label sg `can_flow tr` public);
+  assert(get_label tr sg `can_flow tr` public);
   assert(bytes_invariant tr sg);
   assert(is_publishable tr sg);
 

examples/iso_dh/DY.Example.DH.SecurityProperties.fst

@@ -77,7 +77,7 @@ let initiator_forward_secrecy tr alice alice_si bob gx gy k =
   // (this assert is not needed and only there for pedagogical purposes)
   assert(
     is_corrupt tr (principal_label bob) \/
-    (exists bob_si. get_label k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
+    (exists bob_si. get_label tr k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
   );
 
   // We deduce from the following this assertion,
@@ -124,7 +124,7 @@ let responder_forward_secrecy tr alice bob bob_si gx gy k =
   // (this assert is not needed and only there for pedagogical purposes)
   assert(
     is_corrupt tr (principal_label alice) \/
-    (exists alice_si. get_label k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
+    (exists alice_si. get_label tr k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
   );
 
   // We deduce from the following this assertion,

examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst

@@ -54,13 +54,13 @@ let event_predicate_nsl: event_predicate nsl_event =
     match e with
     | Initiate1 alice bob n_a -> (
       prin == alice /\
-      get_label n_a == join (principal_label alice) (principal_label bob) /\
+      is_secret (join (principal_label alice) (principal_label bob)) tr n_a /\
       0 < DY.Core.Trace.Type.length tr /\
       rand_generated_at tr (DY.Core.Trace.Type.length tr - 1) n_a
     )
     | Respond1 alice bob n_a n_b -> (
       prin == bob /\
-      get_label n_b == join (principal_label alice) (principal_label bob) /\
+      is_secret (join (principal_label alice) (principal_label bob)) tr n_b /\
       0 < DY.Core.Trace.Type.length tr /\
       rand_generated_at tr (DY.Core.Trace.Type.length tr - 1) n_b
     )
@@ -320,8 +320,8 @@ let prepare_msg4 tr global_sess_id bob sess_id msg_id =
           // because we know the label of n_b (which is (join (principal_label alice) (principal_label bob))).
           // It is useful in the "modulo corruption" part of the proof.
           introduce (~((join (principal_label alice) (principal_label bob)) `can_flow tr` public)) ==> event_triggered tr alice (Initiate2 alice bob n_a n_b) with _. (
-            assert(exists alice' n_a'. get_label n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b));
-            eliminate exists alice' n_a'. get_label n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b)
+            assert(exists alice' n_a'. get_label tr n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b));
+            eliminate exists alice' n_a'. get_label tr n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b)
             returns _
             with _. (
               event_respond1_injective tr alice alice' bob n_a n_a' n_b

examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst

@@ -24,28 +24,30 @@ let crypto_predicates_nsl = {
   pkenc_pred = {
     pred = (fun tr pk msg ->
       get_sk_usage pk == PkKey "NSL.PublicKey" empty /\
-      (exists prin. get_sk_label pk = principal_label prin /\ (
+      (exists prin. get_sk_label tr pk == principal_label prin /\ (
         match parse message msg with
         | Some (Msg1 msg1) -> (
           let (alice, bob) = (msg1.alice, prin) in
           event_triggered tr alice (Initiate1 alice bob msg1.n_a) /\
-          get_label msg1.n_a == join (principal_label alice) (principal_label bob)
+          get_label tr msg1.n_a == join (principal_label alice) (principal_label bob)
         )
         | Some (Msg2 msg2) -> (
           let (alice, bob) = (prin, msg2.bob) in
           event_triggered tr bob (Respond1 alice bob msg2.n_a msg2.n_b) /\
-          get_label msg2.n_b == join (principal_label alice) (principal_label bob)
+          get_label tr msg2.n_b == join (principal_label alice) (principal_label bob)
         )
         | Some (Msg3 msg3) -> (
           let bob = prin in
           exists alice n_a.
-            get_label msg3.n_b `can_flow tr` (principal_label alice) /\
+            get_label tr msg3.n_b `can_flow tr` (principal_label alice) /\
             event_triggered tr alice (Initiate2 alice bob n_a msg3.n_b)
         )
         | None -> False
       ))
     );
-    pred_later = (fun tr1 tr2 pk msg -> ());
+    pred_later = (fun tr1 tr2 pk msg ->
+      parse_wf_lemma message (bytes_well_formed tr1) msg
+    );
   };
 }
 #pop-options
@@ -213,7 +215,7 @@ val decode_message3_proof:
   Lemma
   (requires
     // From the NSL state invariant
-    get_label n_b = join (principal_label alice) (principal_label bob) /\
+    get_label tr n_b == join (principal_label alice) (principal_label bob) /\
     // From the PrivateKeys invariant
     is_decryption_key (PkKey "NSL.PublicKey" empty) (principal_label bob) tr sk_b /\
     // From the network
@@ -225,7 +227,7 @@ val decode_message3_proof:
     | Some msg3 -> (
       (is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob)) \/ (
         (exists alice n_a.
-          get_label msg3.n_b `can_flow tr` (principal_label alice) /\
+          get_label tr msg3.n_b `can_flow tr` (principal_label alice) /\
           event_triggered tr alice (Initiate2 alice bob n_a n_b))
       )
     )

src/core/DY.Core.Bytes.Type.fst

@@ -62,7 +62,7 @@ and bytes =
   // Public values (strings, numbers, ...)
   | Literal: FStar.Seq.seq FStar.UInt8.t -> bytes
   // Randomly generated numbers. `time` is used to ensure two random numbers are distinct.
-  | Rand: usage:usage -> label:label -> len:nat{len <> 0} -> time:nat -> bytes
+  | Rand: usage:usage -> len:nat{len <> 0} -> time:nat -> bytes
 
   // Concatenation
   | Concat: left:bytes -> right:bytes -> bytes
@@ -116,7 +116,7 @@ let rec encode_usage usg =
 and encode_bytes b =
   match b with
   | Literal l -> 0::(encode_list [encode l])
-  | Rand usg lab len time -> 1::(encode_list [encode_usage usg; encode lab; encode (len <: nat); encode time])
+  | Rand usg len time -> 1::(encode_list [encode_usage usg; encode (len <: nat); encode time])
   | Concat left right -> 2::(encode_list [encode_bytes left; encode_bytes right])
   | AeadEnc key nonce msg ad -> 3::(encode_list [encode_bytes key; encode_bytes nonce; encode_bytes msg; encode_bytes ad])
   | Pk sk -> 4::(encode_list [encode_bytes sk])
@@ -133,7 +133,7 @@ and encode_bytes b =
   | KemSecretShared ss -> 15::(encode_list [encode_bytes ss])
 
 // --warn_error is a workaround for FStar/FStarLang#3220
-#push-options "--z3rlimit 25 --fuel 4 --ifuel 4 --warn_error +290"
+#push-options "--z3rlimit 25 --fuel 3 --ifuel 3 --warn_error +290"
 val encode_usage_inj: usg1:usage -> usg2:usage -> Lemma (requires encode_usage usg1 == encode_usage usg2) (ensures usg1 == usg2)
 val encode_bytes_inj: b1:bytes -> b2:bytes -> Lemma (requires encode_bytes b1 == encode_bytes b2) (ensures b1 == b2)
 let rec encode_usage_inj usg1 usg2 =
@@ -160,10 +160,13 @@ and encode_bytes_inj b1 b2 =
   encode_inj_forall (list (list int)) ();
   match b1, b2 with
   | Literal x1, Literal x2 ->
+    encode_list_inj [encode x1] [encode x2];
     encode_inj x1 x2
-  | Rand x1 x2 _ _, Rand y1 y2 _ _ ->
+  | Rand x1 x2 x3, Rand y1 y2 y3 ->
+    encode_list_inj [encode_usage x1; encode (x2 <: nat); encode x3] [encode_usage y1; encode (y2 <: nat); encode y3];
     encode_usage_inj x1 y1;
-    encode_inj x2 y2
+    encode_inj x2 y2;
+    encode_inj x3 y3
   | Pk x1, Pk y1
   | Vk x1, Vk y1
   | Hash x1, Hash y1