From aa869ef6b8978adc2781e9d534a333cf2c7a8e92 Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Wed, 19 Feb 2025 10:43:53 +0100
Subject: [PATCH 1/9] online authn with 3 events - init

---
 Makefile                                      |   2 +-
 .../Online_with_authn/DY.OnlineA.Data.fst     | 202 ++++++++++
 .../DY.OnlineA.Invariants.Proofs.fst          | 359 ++++++++++++++++++
 .../DY.OnlineA.Invariants.fst                 | 261 +++++++++++++
 .../DY.OnlineA.Properties.fst                 |  48 +++
 .../Online_with_authn/DY.OnlineA.Protocol.fst | 168 ++++++++
 .../DY.OnlineA.Run.Printing.fst               |  42 ++
 examples/Online_with_authn/DY.OnlineA.Run.fst |  83 ++++
 examples/Online_with_authn/Makefile           |  10 +
 9 files changed, 1174 insertions(+), 1 deletion(-)
 create mode 100644 examples/Online_with_authn/DY.OnlineA.Data.fst
 create mode 100644 examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
 create mode 100644 examples/Online_with_authn/DY.OnlineA.Invariants.fst
 create mode 100644 examples/Online_with_authn/DY.OnlineA.Properties.fst
 create mode 100644 examples/Online_with_authn/DY.OnlineA.Protocol.fst
 create mode 100644 examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
 create mode 100644 examples/Online_with_authn/DY.OnlineA.Run.fst
 create mode 100644 examples/Online_with_authn/Makefile

diff --git a/Makefile b/Makefile
index c6961c3..e977a87 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,7 @@ INNER_SOURCE_DIRS = dy-extensions
 # SOURCE_DIRS = $(addprefix $(DY_HOME)/src/, $(INNER_SOURCE_DIRS))
 SOURCE_DIRS = $(addprefix $(TUTORIAL_HOME)/, $(INNER_SOURCE_DIRS))
 
-INNER_EXAMPLE_DIRS = nsl_pk_only_one_event_lookup TwoMessageP Online Online_with_secrecy
+INNER_EXAMPLE_DIRS = nsl_pk_only_one_event_lookup TwoMessageP Online Online_with_secrecy Online_wiht_authn
 EXAMPLE_DIRS ?= $(addprefix $(TUTORIAL_HOME)/examples/, $(INNER_EXAMPLE_DIRS))
 
 
diff --git a/examples/Online_with_authn/DY.OnlineA.Data.fst b/examples/Online_with_authn/DY.OnlineA.Data.fst
new file mode 100644
index 0000000..02e75d6
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Data.fst
@@ -0,0 +1,202 @@
+module DY.OnlineA.Data
+
+open Comparse
+open DY.Core
+open DY.Lib
+
+/// Here, we define the abstract types for the "Online?" Protocol:
+///
+/// A -> B: enc{Ping (A, n_A)}_B
+/// B -> A: enc{Ack n_A}_A
+///
+/// (They are the same as for the simple 2 message protocol)
+
+(*** Message Type ***)
+
+/// for each of the two messages we define an abstract message type
+
+[@@ with_bytes bytes] // ignore this line for now
+type ping_t = {
+  alice: principal;
+  n_a : bytes;
+}
+
+[@@ with_bytes bytes] // ignore this line for now
+type ack_t = {
+  n_a : bytes;
+}
+
+/// the overall abstract message type
+/// (consisting of constructors for the two messages
+/// and using the above abstract types for each of them)
+
+[@@ with_bytes bytes] // ignore this line for now
+type message_t =
+  | Ping: (ping:ping_t) -> message_t
+  | Ack: (ack:ack_t) -> message_t
+
+
+/// We use Comparse to generate the corresponding message formats.
+/// I.e., we don't need to write parsing and serializing by hand
+///
+/// for this we need the `[@@ with_bytes bytes]` annotation for the message types above
+///
+/// We are not going into the details of how Comparse works.
+
+
+/// We let Comparse generate a parser `ps_ping_t` for the abstract `ping_t` type
+
+%splice [ps_ping_t] (gen_parser (`ping_t))
+
+/// ... and the same for the other abstract message types
+
+%splice [ps_ack_t] (gen_parser (`ack_t))
+
+%splice [ps_message_t] (gen_parser (`message_t))
+
+/// With the above parsers, we can make our `message` type an instance of
+/// Comparse's `parseable_serializeable` class.
+/// Again, the details are not important here,
+/// but this is the step that enables us to call
+/// `parse message buff` and `serialize message msg`
+/// to translate between bytes and our abstract message type.
+
+instance parseable_serializeable_bytes_message_t: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t
+
+
+(*** State Type ***)
+
+/// As for the messages we define abstract state types
+/// for the three states stored by Alice and Bob after each step of the protocol.
+
+[@@ with_bytes bytes]
+type sent_ping_t = {
+  bob : principal;
+  n_a : bytes;
+}
+
+[@@ with_bytes bytes]
+type sent_ack_t = {
+  alice: principal;
+  n_a : bytes;
+}
+
+[@@ with_bytes bytes]
+type received_ack_t = {
+  bob : principal;
+  n_a : bytes;
+}
+
+[@@ with_bytes bytes]
+type state_t = 
+  | SentPing: (ping:sent_ping_t) -> state_t
+  | SentAck: (ack:sent_ack_t) -> state_t
+  | ReceivedAck: (rack:received_ack_t) -> state_t
+
+/// As for messages, we use Comparse to generate
+/// a parser and serializer for our abstract state types.
+
+%splice [ps_sent_ping_t] (gen_parser (`sent_ping_t))
+%splice [ps_sent_ack_t] (gen_parser (`sent_ack_t))
+%splice [ps_received_ack_t] (gen_parser (`received_ack_t))
+%splice [ps_state_t] (gen_parser (`state_t))
+
+/// Now, we can call
+/// `parse state buff` and `serialize state st`
+/// to translate between bytes and the abstract state type.
+
+instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes state_t = mk_parseable_serializeable ps_state_t
+
+/// We tag our protocol level states,
+/// so that they are distinguishable from any internal DY* states. 
+
+instance local_state_state: local_state state_t = {
+  tag = "P.State";
+  format = parseable_serializeable_bytes_state_t;
+}
+
+
+
+(*** PKI ***)
+
+/// For en-/de-cryption we assume some PKI.
+/// I.e., every participant has some private decryption keys
+/// and some public encryption keys from other participants.
+/// All private keys of a participant will be stored in one session
+/// and all public keys that the participant knows will be stored in another session.
+/// For each participant, we collect both these session IDs in a global record.
+
+type global_sess_ids = {
+  pki: state_id;
+  private_keys: state_id;
+}
+
+/// Similarly as for states,
+/// we tag the keys that are used on the protocol level,
+/// so that they can not be confused with other keys.
+/// (TODO: rephrase this)
+
+let key_tag = "P.Key"
+
+
+(*** Event type ***)
+
+/// We are now using events to show the authentication property.
+/// We will have two events for the first two protocol steps,
+/// i.e., there is an Initiating event
+/// that Alice triggers, when she starts a new run
+/// and a Responding event,
+/// that Bob triggers, when he replies to a Ping with an Ack.
+
+/// Just as for messages and states,
+/// we define abstract event types
+
+
+
+/// The abstract type of the Initiating event
+[@@ with_bytes bytes]
+type ev_init_t = {
+  alice:principal;
+  bob:principal;
+  n_a:bytes
+}
+
+/// The abstract type of the Responding event
+[@@ with_bytes bytes]
+type ev_respond_t = {
+  alice:principal;
+  bob:principal;
+  n_a:bytes
+}
+
+
+/// The abstract type of the Finishing event
+[@@ with_bytes bytes]
+type ev_finish_t = {
+  alice:principal;
+  bob:principal;
+  n_a:bytes
+}
+
+
+/// The overall event type
+[@@ with_bytes bytes]
+type event_t =
+  | Initiating: ev_init_t -> event_t
+  | Responding: ev_respond_t -> event_t
+  | Finishing: ev_finish_t -> event_t
+
+
+/// Using Comparse to generate parser and serializer for the abstract event types
+%splice [ps_ev_init_t] (gen_parser (`ev_init_t))
+%splice [ps_ev_respond_t] (gen_parser (`ev_respond_t))
+%splice [ps_ev_finish_t] (gen_parser (`ev_finish_t))
+%splice [ps_event_t] (gen_parser (`event_t))
+%splice [ps_event_t_is_well_formed] (gen_is_well_formed_lemma (`event_t))
+
+
+/// Make the overall event type an instance of DY.Lib event class
+instance event_event_t: event event_t = {
+  tag = "P.Event";
+  format = mk_parseable_serializeable ps_event_t;
+}
diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
new file mode 100644
index 0000000..ebc1451
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
@@ -0,0 +1,359 @@
+module DY.OnlineA.Invariants.Proofs
+
+open Comparse
+open DY.Core
+open DY.Lib
+
+open DY.Simplified
+open DY.Extend
+
+open DY.OnlineA.Data
+open DY.OnlineA.Protocol
+open DY.OnlineA.Invariants
+
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 25  --z3cliopt 'smt.qi.eager_threshold=100'"
+
+/// In this module, we show that
+/// the three protocol steps (send_ping, receive_ping_and_send_ack, and receive_ack)
+/// maintain the protocol invariants.
+///
+/// For every step s we show a lemma of the form:
+/// trace_invariant tr ==> trace_invariant ( trace after step s )
+
+/// Again, we only highlight the differences to the previous model
+/// for nonce secrecy.
+
+(*** Sending a Ping maintains the invariants ***)
+
+val send_ping_invariant_short_version:
+  alice:principal -> bob:principal -> keys_sid:state_id ->
+  tr:trace ->
+  Lemma
+  ( requires trace_invariant tr
+  )
+  (ensures (
+    let (_ , tr_out) = send_ping alice bob keys_sid tr in
+    trace_invariant tr_out
+  ))
+let send_ping_invariant_short_version alice bob keys_sid  tr =
+  let (n_a, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in
+  (* We need to adapt the proof to the new send_ping function,
+     where we trigger the Initiating event right after nonce generation.
+  *)
+  let (_, tr_ev) = trigger_event alice (Initiating {alice; bob; n_a}) tr_rand in
+  let ping = Ping {alice; n_a} in 
+  serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_ev) ping;
+  pke_enc_for_is_publishable tr_ev alice bob keys_sid key_tag ping
+
+
+(*** Replying to a Ping maintains the invariants ***)
+
+val decode_ping_invariant:
+  bob:principal -> keys_sid:state_id ->
+  msg:bytes ->
+  tr:trace ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (_, tr_out) = decode_ping bob keys_sid msg tr in
+    trace_invariant tr_out
+  ))
+let decode_ping_invariant bob keys_sid msg tr = ()
+
+(* For the second protocol step (`receive_ping_and_send_ack`),
+   we need a helper lemma: `decode_ping_proof`.
+
+   Ignore this for now, and jump to the next lemma 
+   `receive_ping_and_send_ack_invariant`
+*)
+
+val decode_ping_proof:
+  tr:trace ->
+  bob:principal -> keys_sid:state_id ->
+  msg:bytes ->
+  Lemma
+  (requires (
+    trace_invariant tr
+    /\ bytes_invariant tr msg
+  ))
+  (ensures (
+    match decode_ping bob keys_sid msg tr with
+    | (None, _) -> True
+    | (Some png, _) -> (
+        let n_a = png.n_a in
+        let (sk_bob, _) = get_private_key bob keys_sid (LongTermPkeKey key_tag) tr in
+        Some? sk_bob /\
+        bytes_invariant tr n_a /\
+        is_knowable_by (nonce_label png.alice bob) tr n_a /\
+        ( is_publishable tr n_a
+        \/ (pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) bob) (pk (Some?.v sk_bob)) (serialize message_t (Ping png)))
+        )
+     )
+   )
+  )
+let decode_ping_proof tr bob keys_sid msg =
+    match decode_ping bob keys_sid msg tr with
+    | (None, _) -> ()
+    | (Some png, _) -> (
+        bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t bob keys_sid key_tag msg;
+        let plain = serialize message_t (Ping png) in
+        parse_wf_lemma message_t (bytes_invariant tr) plain;
+        FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain
+    )
+  
+
+
+/// The invariant lemma for the `receive_ping_and_send_ack` step
+
+
+#push-options "--z3rlimit 30"
+val receive_ping_and_send_ack_invariant:
+  bob:principal -> keys_sid:global_sess_ids -> ts:timestamp ->
+  tr:trace ->
+  Lemma
+  ( requires trace_invariant tr
+  )
+  (ensures (
+    let (_ , tr_out) = receive_ping_and_send_ack bob keys_sid ts tr in
+    trace_invariant tr_out
+  ))
+let receive_ping_and_send_ack_invariant bob bob_keys_sid msg_ts tr =
+  match recv_msg msg_ts tr with
+  | (None, _ ) -> ()
+  | (Some msg, _) -> (
+      match decode_ping bob bob_keys_sid.private_keys msg tr with
+      | (None, _) -> ()
+      | (Some png, _) -> (
+          let n_a = png.n_a in
+          let alice = png.alice in
+          
+          let ack = Ack {n_a} in
+
+          (* We need to adapt the proof to the new receive_ping_and_send_ack function,
+             where Bob triggers a Responding event.
+          *)
+          let (_, tr_ev) = trigger_event bob (Responding {alice; bob; n_a}) tr in
+
+          (* We have to show,
+             that the new trace tr_ev satisfies the trace invariants, i.e.,
+             that the event prediate is satisfied for the Responding event.
+
+             The event prediate says:
+             if the nonce n_a has not leaked,
+             alice should have triggered an Initiating event.
+
+             We get this guarantee from our helper lemma decode_ping_proof:
+             The post-condition says
+             if the nonce has not leaked,
+             the pke_pred holds for the received Ping message.
+
+             Looking at the pke_pred for the Ping,
+             we get that alice must have triggered an Initiating event.
+          *)
+          decode_ping_proof tr bob bob_keys_sid.private_keys msg;
+          (* We thus get that the trace invariant is satisfied after triggering the event.
+          *)
+          assert(trace_invariant tr_ev);
+
+          match pke_enc_for bob alice bob_keys_sid.pki key_tag ack tr_ev with
+          | (None, _) -> ()
+          | (Some ack_encrypted, tr_ack) ->(
+                assert(trace_invariant tr_ack);
+
+                let (ack_ts, tr_msg) = send_msg ack_encrypted tr_ack in
+                  serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr) ack;
+
+                  (* The final requirement for the pke_enc_for_is_publishable lemma is
+                     that the pke_pred for the Ack is satisfied.
+                     Previously this was trivially true, since we didn't have any restrictions.
+
+                     Now, we need to show that
+                     there is some Bob that triggered a Responding event.
+                     We did that just before the call to the encryption.
+                     Hence this is again immediately satisfied.
+
+                     You can check:
+                     assert(pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) alice) (serialize message_t ack));
+                  *)
+                pke_enc_for_is_publishable tr_ev bob alice bob_keys_sid.pki key_tag ack;
+                assert(trace_invariant tr_msg);
+
+                let st = (SentAck {alice = png.alice; n_a = png.n_a}) in
+                let (sess_id, tr_sess) = start_new_session bob st tr_msg in
+                assert(trace_invariant tr_sess)
+           )
+      )
+  )
+#pop-options
+
+
+(*** Receiving an Ack maintains the invariants ***)
+
+val decode_ack_invariant:
+  alice:principal -> keys_sid:state_id -> cipher:bytes ->
+  tr:trace ->
+  Lemma
+  (requires
+    trace_invariant tr
+  )
+  (ensures (
+    let (_, tr_out) = decode_ack alice keys_sid cipher tr in
+    trace_invariant tr_out
+  ))
+let decode_ack_invariant alice keys_sid msg tr = ()
+
+
+/// Since we now have a non-trivial property for the ReceivedAck state,
+/// the proof does not work automatically anymore (as it did for the secrecy model).
+///
+/// In the same manner as for the other functions,
+/// we need a helper lemma for decoding an ack.
+
+val decode_ack_proof:
+  tr:trace ->
+  alice:principal -> keys_sid:state_id ->
+  msg:bytes ->
+  Lemma
+  (requires (
+    trace_invariant tr
+    /\ bytes_invariant tr msg
+  ))
+  (ensures (
+    match decode_ack alice keys_sid msg tr with
+    | (None, _) -> True
+    | (Some ack, _) -> (
+        let n_a = ack.n_a in
+        let (sk_alice, _) = get_private_key alice keys_sid (LongTermPkeKey key_tag) tr in
+        Some? sk_alice /\
+        bytes_invariant tr n_a /\
+        ( is_publishable tr n_a
+        \/ (pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) alice) (pk (Some?.v sk_alice)) (serialize message_t (Ack ack)))
+        )
+    )
+  ))
+let decode_ack_proof tr alice keys_sid msg =
+    match decode_ack alice keys_sid msg tr with
+    | (None, _) -> ()
+    | (Some ack, _) -> (
+        bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t alice keys_sid key_tag msg;
+        let plain = serialize message_t (Ack ack) in
+        parse_wf_lemma message_t (bytes_invariant tr) plain;
+        FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain
+    )
+  
+
+/// Additionally,
+/// we need an injectivity lemma.
+/// The goal is to show that Alice uses the nonces n_a
+/// only once, i.e., the nonces n_a are unique for every run.
+///
+/// We show this with the help of the Initiating event:
+/// If there are two events triggered by the same Alice
+/// using the same nonce n_a,
+/// then the contained other participants (Bob) must also be the same.
+///
+/// The proof is automatic from the event prediate,
+/// which says that the contained nonce n_a
+/// was generated right before the event.
+/// Since nonces are uniquely identified by their time of creation,
+/// this immediately shows that
+/// two events referring to the same nonce,
+/// must be the same event.
+
+val event_initiating_injective:
+  tr:trace ->
+  alice:principal -> bob:principal -> bob':principal ->
+  n_a:bytes ->
+  Lemma
+  (requires
+    trace_invariant tr /\
+    event_triggered tr alice (Initiating {alice; bob; n_a} ) /\
+    event_triggered tr alice (Initiating {alice; bob = bob'; n_a} )
+  )
+  (ensures
+    bob == bob'
+  )
+let event_initiating_injective tr alice bob bob' n_a = ()
+
+
+/// The invariant lemma for the final protocol step `receive_ack_invariant`
+
+#push-options "--z3rlimit 50"
+val receive_ack_invariant:
+  alice:principal -> keys_sid:state_id -> msg_ts:timestamp ->
+  tr:trace ->
+  Lemma
+  (requires
+    trace_invariant tr
+  )
+  (ensures (
+    let (_, tr_out) = receive_ack alice keys_sid msg_ts tr in
+    trace_invariant tr_out
+  ))
+let receive_ack_invariant alice keys_sid msg_ts tr =
+  match recv_msg msg_ts tr with
+  | (None, _) -> ()
+  | (Some msg, _) -> (
+      match decode_ack alice keys_sid msg tr with
+      | (None, _) -> ()
+      | (Some ack, _) -> (
+          let n_a = ack.n_a in
+          let p = (fun (st:state_t) -> SentPing? st && (SentPing?.ping st).n_a = n_a) in
+          match lookup_state #state_t alice p tr with
+          | (None, _) -> ()
+          | (Some (sid, st), _) -> (
+              let bob = (SentPing?.ping st).bob in
+              let ((), tr_ev) = trigger_event alice (Finishing {alice; bob; n_a}) tr in
+              // We show that the trace invariant holds after triggering the event,
+              // that ist, we show that the event prediate for the Finishing event holds.
+
+              // from the SendPing state predicate
+              assert(event_triggered tr alice (Initiating {alice; bob; n_a}));
+
+              // also from the SendPing state predicate
+              assert(is_secret (nonce_label alice bob) tr n_a);
+              // immediate consequence of the exact label of n_a
+              assert(is_publishable tr n_a ==> is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob));
+              (* the more difficult case is the honest case,
+              //    when the nonce is not publishable
+              // *)
+              introduce ~(is_publishable tr n_a) ==> event_triggered tr bob (Responding {alice; bob; n_a})
+              with _. (
+                decode_ack_proof tr alice keys_sid msg;
+                let (sk_alice, _) = get_private_key alice keys_sid (LongTermPkeKey key_tag) tr in
+                assert(pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) alice) (pk (Some?.v sk_alice)) (serialize message_t (Ack ack)));
+                assert(exists bob'. event_triggered tr bob (Responding {alice; bob = bob'; n_a}));
+                (* From the pke_pred for the decoded Ack,
+                   we get that there is some bob' that 
+                   triggered a Responding event with Alice and n_a.
+                   So, we need to show, that this bob' is 
+                   the same as the bob stored in Alice's SendPing state.
+                *)
+                (* The event prediate for the Responding event of bob'
+                    guarantees, that alice must have triggered an Initiating event 
+                    containing bob'.
+                *)
+
+                assert(exists bob'. event_triggered tr alice (Initiating {alice; bob = bob'; n_a}));
+                (* We now use nonce injectivity from above to show that bob' = bob. *)
+                eliminate exists bob'. event_triggered tr alice (Initiating {alice; bob = bob'; n_a})
+                returns _
+                with _. (
+                  // from the state predicate of the looked up SendingPing state of Alice:
+                  assert(event_triggered tr alice (Initiating {alice; bob; n_a}));
+
+                  // the injectivity lemma from above, yields bob' = bob
+                  event_initiating_injective tr alice bob bob' n_a
+                )
+              );
+              assert(trace_invariant tr_ev);
+                                                   
+              let newst = ReceivedAck {bob; n_a} in
+
+              let ((), tr_st) = set_state alice sid newst tr_ev in
+              
+              assert(trace_invariant tr_st)
+          )
+      )
+  )
+#pop-options
diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.fst
new file mode 100644
index 0000000..5cc76a5
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.fst
@@ -0,0 +1,261 @@
+module DY.OnlineA.Invariants
+
+open Comparse 
+open DY.Core
+open DY.Lib
+
+open DY.Extend
+
+open DY.OnlineA.Data
+open DY.OnlineA.Protocol
+
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 25"
+
+/// In this module, we define the protocol invariants.
+/// They consist of
+/// * crypto invariants and
+/// * trace invariants which in turn consist of
+///   * state invariants and
+///   * event invariants
+///
+/// We then have to show
+/// * these invariants imply the secrecy property (see DY.OnlineS.Secrecy) and
+/// * every protocol step maintains these invariants (see DY.OnlineS.Invariants.Proofs)
+/// With this, we then know that
+/// the protocol model satisfies the secrecy property.
+
+/// We only highlight the differences to the previous model
+/// for showing nonce secrecy.
+
+(*** Crypto Invariants ***)
+
+
+%splice [ps_ping_t_is_well_formed] (gen_is_well_formed_lemma (`ping_t))
+%splice [ps_ack_t_is_well_formed] (gen_is_well_formed_lemma (`ack_t))
+%splice [ps_message_t_is_well_formed] (gen_is_well_formed_lemma (`message_t))
+
+instance crypto_usages_p : crypto_usages = default_crypto_usages
+
+#push-options "--ifuel 2"
+let crypto_p : crypto_predicates = { 
+  default_crypto_predicates with 
+  pke_pred = { 
+    pred = (fun tr sk_usage pk msg ->
+    exists prin.
+    (
+      sk_usage == long_term_key_type_to_usage (LongTermPkeKey key_tag) prin /\
+      (match parse message_t msg with
+      | Some (Ping ping) ->
+          let bob = prin in
+          let alice = ping.alice in
+          let n_a = ping.n_a in
+          get_label tr n_a == nonce_label alice bob
+
+          (* We add, that the Alice specified in the Ping message,
+             must have triggered an Initiating event
+             with 
+             * her own name (alice)
+             * the intended receiver of the Ping (bob) and
+             * the nonce n_a in the Ping
+          *)
+          /\ event_triggered tr alice (Initiating {alice; bob; n_a})
+      | Some (Ack ack) ->
+          (* For nonce secrecy,
+             we didn't have any conditions/guarantees in the Ack case.
+             Now, we add that 
+             some Bob must have triggered a Responding event with
+             * the intended receiver of the Ack (alice)
+             * his own name (bob) and
+             * the nonce (n_a) in the Ack
+          *)
+          let alice = prin in
+          exists bob. event_triggered tr bob (Responding {alice; bob; n_a = ack.n_a})
+      | _ -> False
+      ))
+      ); 
+    pred_later = (fun tr1 tr2 sk_usage pk msg -> 
+      parse_wf_lemma message_t (bytes_well_formed tr1) msg
+    ) 
+  } 
+}
+#pop-options
+
+/// Collecting the usages and prediates in the final crypto invariants
+
+instance crypto_invariants_p: crypto_invariants = {
+  usages = crypto_usages_p;
+  preds =  crypto_p
+}
+
+
+(*** State Invariant ***)
+
+%splice [ps_sent_ping_t_is_well_formed] (gen_is_well_formed_lemma (`sent_ping_t))
+%splice [ps_sent_ack_t_is_well_formed] (gen_is_well_formed_lemma (`sent_ack_t))
+%splice [ps_received_ack_t_is_well_formed] (gen_is_well_formed_lemma (`received_ack_t))
+%splice [ps_state_t_is_well_formed] (gen_is_well_formed_lemma (`state_t))
+
+#push-options "--ifuel 2 --z3cliopt 'smt.qi.eager_threshold=50'"
+let state_predicate_p: local_state_predicate state_t = {
+  pred = (fun tr prin sess_id st ->
+    match st with
+    | SentPing ping -> (
+        let alice = prin in
+        let bob = ping.bob in
+        let n_a = ping.n_a in
+        is_secret (nonce_label alice bob) tr n_a
+        (* We add, that the storing principal (alice),
+           must have triggered an Initiating event with:
+           * her own name
+           * the bob stored in the state and
+           * the nonce stored in the state
+        *)
+        /\ event_triggered tr alice (Initiating {alice = alice; bob = bob; n_a = n_a})
+    )
+    | SentAck ack -> (
+        let bob = prin in
+        let alice = ack.alice in
+        let n_a = ack.n_a in
+        is_knowable_by (principal_label bob) tr n_a
+        (* Additionally, we enforce that
+           the storing principal (bob) 
+           must have triggered e Responding event with:
+           * the stored name (alice)
+           * his own name (bob)
+           * the stored nonce (n_a)
+        *)
+        /\ event_triggered tr bob (Responding {alice; bob; n_a})
+    )
+    | ReceivedAck rack  -> (
+        let alice = prin in
+        let bob = rack.bob in
+        let n_a = rack.n_a in
+        is_secret (nonce_label alice bob) tr n_a
+
+        (* We add, that the storing principal (alice),
+          must have triggered a Finishing event with:
+          * her own name
+          * the bob stored in the state and
+          * the nonce stored in the state
+        *)
+        /\ event_triggered tr alice (Finishing {alice; bob; n_a})
+    )
+  );
+  pred_later = (fun tr1 tr2 prin sess_id st -> () );
+  pred_knowable = (fun tr prin sess_id st -> () );
+}
+#pop-options
+
+
+(*** Event Pred ***)
+
+/// As for messages and states,
+/// we also have prediates on events.
+/// The intuition is similar:
+/// They say when an event is allowed to be triggered, or
+/// what guarantees we obtain, if we observe a specific event on the trace.
+
+let event_predicate_event_t: event_predicate event_t =
+  fun tr prin e ->
+  // prin is the principal triggering the event
+    match e with    
+    | Initiating init -> (
+        let alice = init.alice in
+        let bob = init.bob in
+        let n_a = init.n_a in
+        (* We may trigger the Initiating event only if,
+           * the triggering principal is the first principal stored in the event (alice)
+           * the nonce (n_a) in the event is labelled for 
+             the two principals stored in the event (alice and bob)
+           * the stored nonce (n_a) was generated right before the event is triggered
+             (this is crucial and will be used to show an injectivity property,
+             that there will be only one such event for a fixed nonce n_a)
+        *)
+        prin == alice /\
+        is_secret (nonce_label alice bob) tr n_a /\
+        rand_just_generated tr n_a
+    )
+    | Responding resp -> (
+        let alice = resp.alice in
+        let bob = resp.bob in
+        let n_a = resp.n_a in
+        (* A Responding event may only be triggered if,
+           * the triggering principal is the second principal stored in the event (bob)
+           * if the stored nonce n_a has not leaked,
+             then the first stored principal (alice)
+             must have triggered an Initiating event with the same data
+             as the Responding event
+        *)
+        prin == bob
+        /\ (is_publishable tr n_a
+          \/ event_triggered tr alice (Initiating {alice; bob; n_a})
+        )
+    )
+    | Finishing fin -> (
+        let alice = fin.alice in
+        let bob = fin.bob in
+        let n_a = fin.n_a in
+
+        prin == alice /\
+        event_triggered tr alice (Initiating {alice; bob; n_a}) /\
+        ( is_corrupt tr (nonce_label alice bob) \/
+          event_triggered tr bob (Responding {alice; bob; n_a})
+        )
+    )
+
+
+(*** Trace invariants ***)
+
+let all_sessions = [
+  pki_tag_and_invariant;
+  private_keys_tag_and_invariant;
+  (|local_state_state.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_p|);
+]
+
+/// Now we have an event type
+let all_events = [(event_event_t.tag, compile_event_pred event_predicate_event_t)]
+
+let trace_invariants_p: trace_invariants = {
+  state_pred = mk_state_pred all_sessions;
+  event_pred = mk_event_pred all_events;
+}
+
+
+(*** Protocol Invariants ***)
+
+instance protocol_invariants_p: protocol_invariants = {
+  crypto_invs = crypto_invariants_p;
+  trace_invs = trace_invariants_p;
+}
+
+
+(*** Helper Lemmas for the Secrecy Proof ***)
+
+val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate) all_sessions))
+let all_sessions_has_all_sessions () =
+  assert_norm(List.Tot.no_repeats_p (List.Tot.map dfst (all_sessions)));
+  mk_state_pred_correct all_sessions;
+  norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate) all_sessions)
+
+val protocol_invariants_p_has_p_session_invariant: squash (has_local_state_predicate state_predicate_p)
+let protocol_invariants_p_has_p_session_invariant = all_sessions_has_all_sessions ()
+
+val protocol_invariants_p_has_pki_invariant: squash (has_pki_invariant #protocol_invariants_p)
+let protocol_invariants_p_has_pki_invariant = all_sessions_has_all_sessions ()
+
+val protocol_invariants_p_has_private_keys_invariant: squash (has_private_keys_invariant #protocol_invariants_p)
+let protocol_invariants_p_has_private_keys_invariant = all_sessions_has_all_sessions ()
+
+
+/// We need similar lemmas for our event type
+
+val all_events_has_all_events: unit -> Lemma (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events))
+let all_events_has_all_events () =
+  assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_events)));
+  mk_event_pred_correct #protocol_invariants_p all_events;
+  norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events);
+  let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in
+  dumb_lemma (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events))
+
+val protocol_invariants_p_has_event_t_invariant: squash (has_event_pred event_predicate_event_t)
+let protocol_invariants_p_has_event_t_invariant = all_events_has_all_events ()
diff --git a/examples/Online_with_authn/DY.OnlineA.Properties.fst b/examples/Online_with_authn/DY.OnlineA.Properties.fst
new file mode 100644
index 0000000..9179980
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Properties.fst
@@ -0,0 +1,48 @@
+module DY.OnlineA.Properties
+
+open Comparse
+open DY.Core
+open DY.Lib
+
+open DY.Extend
+
+open DY.OnlineA.Data
+open DY.OnlineA.Invariants
+
+/// This is the new property, we want to show:
+/// if Alice finishes a run identified by Bob and a nonce n_a,
+/// then this Bob was involved in the run,
+/// i.e., Bob sent n_a in an acknowledgement to Alice.
+/// Unless one of Alice or Bob are corrupt.
+
+val responder_authentication:
+  tr:trace -> ts:timestamp ->
+  alice:principal -> bob:principal ->
+  n_a:bytes ->
+  Lemma
+  (requires
+     trace_invariant tr /\
+     event_triggered_at tr ts alice (Finishing {alice; bob; n_a})
+  )
+  (ensures
+     is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob) \/
+     event_triggered (prefix tr ts) bob (Responding {alice; bob; n_a})
+  )
+let responder_authentication tr ts alice bob n_a = ()
+
+
+/// We still have nonce secrecy:
+
+val n_a_secrecy:
+  tr:trace -> alice:principal -> bob:principal -> n_a:bytes ->
+  Lemma
+  (requires
+    attacker_knows tr n_a /\
+    trace_invariant tr /\ (
+      (state_was_set_some_id tr alice (SentPing {bob; n_a})) \/
+      (state_was_set_some_id tr alice (ReceivedAck {bob; n_a} ))
+    )
+  )
+  (ensures is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob))
+let n_a_secrecy tr alice bob n_a =
+  attacker_only_knows_publishable_values tr n_a
diff --git a/examples/Online_with_authn/DY.OnlineA.Protocol.fst b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
new file mode 100644
index 0000000..498e04f
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
@@ -0,0 +1,168 @@
+module DY.OnlineA.Protocol
+
+open Comparse
+open DY.Core
+open DY.Lib
+
+open DY.Simplified
+open DY.Extend
+
+open DY.OnlineA.Data
+
+/// Here we define the DY* mode of the "Online?" protocol,
+/// an extension of the simple Two Message protocol:
+/// the two messages are now (asymmetrically) encrypted
+///
+/// A -> B: enc{Ping (A, n_A)}_B
+/// B -> A: enc{Ack n_A}_A
+///
+/// The model consists of 3 functions,
+/// one for each protocol step
+/// (just as for the simple two message protocol):
+/// 1. Alice sends the Ping to Bob (`send_ping`)
+/// 2. Bob receives the Ping and replies with the Ack (`receive_ping_and_send_ack`)
+/// 3. Alice receives the Ack (`receive_ack`)
+///
+/// Additionally, there are two helper functions
+/// for steps 2 and 3 (`decode_ping` and `decode_ack`).
+
+/// We only highlight the differences to the previous model
+/// for nonce secrecy.
+
+(*** Sending the Ping ***)
+
+/// Alice sends the first message to Bob:
+/// * Alice generates a new nonce [n_a]
+/// * encrypts the message (Alice, n_a) for Bob
+/// * sends the encrypted message
+/// * stores n_a and Bob in a state (in a new session)
+/// The step returns the ID of the new state
+/// and the timestamp of the message on the trace
+/// The step fails, if
+/// encryption was not successful, i.e.,
+/// Alice does not have a public key of Bob.
+
+let nonce_label alice bob = join (principal_label alice) (principal_label bob)
+
+val send_ping: principal -> principal -> state_id -> traceful (option (state_id & timestamp))
+let send_ping alice bob keys_sid =
+  let* n_a = gen_rand_labeled (nonce_label alice bob) in
+
+  (* This is the new step of triggering the Initiating event.
+     ATTENTION: it has to be called right after generating the nonce
+     (for the event predicate we will see later)
+  *)
+  trigger_event alice (Initiating {alice = alice; bob = bob; n_a = n_a});*
+
+  let ping = Ping {alice; n_a} in 
+
+  let*? ping_encrypted = pke_enc_for alice bob keys_sid key_tag ping in
+  let* msg_ts = send_msg ping_encrypted in
+
+  let ping_state = SentPing {bob; n_a} in
+  let* sid = start_new_session alice ping_state in
+
+  return (Some (sid, msg_ts))
+
+
+(*** Replying to a Ping with an Ack ***)
+
+
+/// Bob receives the first messages and replies:
+/// * read the message from the trace
+/// * decrypt the message to (Alice, n_a)
+/// * encrypt the reply (n_a) for Alice
+/// * send the encrypted reply
+/// * store n_a and Alice in a state in a new session
+/// The step returns the ID of the new state
+/// and the timestamp of the reply on the trace.
+/// The step fails, if one of
+/// * decryption fails
+/// * the message is not of the right type, i.e., not a first message
+/// * encryption fails
+
+/// Decrypting the message (Step 2 from above) is pulled out to a separate function
+/// The function
+/// * decrypts the message
+/// * checks that the message is of the right type (a Ping)
+/// * returns the content of the message
+/// The function fails if decryption fails.
+
+val decode_ping : principal -> state_id -> bytes -> traceful (option ping_t)
+let decode_ping bob keys_sid msg =
+  let*? png = pke_dec_with_key_lookup #message_t bob keys_sid key_tag msg in
+  
+  guard_tr (Ping? png);*?
+
+  return (Some (Ping?.ping png))
+
+/// Now the actual receive and reply step
+/// using the decode function
+val receive_ping_and_send_ack: principal -> global_sess_ids -> timestamp -> traceful (option (state_id & timestamp))
+let receive_ping_and_send_ack bob global_sids msg_ts =
+  let*? msg = recv_msg msg_ts in
+  let*? png = decode_ping bob global_sids.private_keys msg in
+
+  let n_a = png.n_a in
+  let alice = png.alice in
+  
+  (* This is the new step, where Bob triggers the Responding event for the current run
+  *)
+  trigger_event bob (Responding {alice = alice; bob = bob; n_a = n_a});* 
+
+  let ack = Ack {n_a} in
+  let*? ack_encrypted = pke_enc_for bob alice global_sids.pki key_tag ack in
+  let* ack_ts = send_msg ack_encrypted in
+  
+  let* sess_id = start_new_session bob (SentAck {alice; n_a}) in
+  
+  return (Some (sess_id, ack_ts))
+
+
+(*** Receiving an Ack ***)
+
+
+/// Alice receives the reply from Bob:
+/// * read the message from the trace
+/// * decrypt the message to (n_a)
+/// * check if Alice previously sent n_a in some session
+/// * store completion of this session in a new state
+/// Returns the ID of the session that is marked as completed.
+/// The step fails, if one of
+/// * decryption fails
+/// * the message is not of the right type, i.e., not a reply
+/// * there is no prior session related to n_a
+
+
+/// Again, we pull out decryption of the message (Step 2):
+/// * decrypt the message
+/// * check that the message is of the Ack type
+/// Returns the content of the reply.
+/// Fails if decryption fails.
+
+val decode_ack : principal -> state_id -> bytes -> traceful (option ack_t)
+let decode_ack alice keys_sid cipher =
+  let*? ack = pke_dec_with_key_lookup #message_t alice keys_sid key_tag cipher in
+
+  guard_tr (Ack? ack);*?
+
+  return (Some (Ack?.ack ack))
+
+/// The actual protocol step using the decode function
+val receive_ack: principal -> state_id -> timestamp -> traceful (option state_id)
+let receive_ack alice keys_sid ack_ts =
+  let*? msg = recv_msg ack_ts in
+  let*? ack = decode_ack alice keys_sid msg in
+
+  let n_a = ack.n_a in
+
+  let*? (sid, st) = lookup_state #state_t alice
+    (fun st -> SentPing? st && (SentPing?.ping st).n_a = n_a)
+    in
+  guard_tr(SentPing? st);*?
+  let bob = (SentPing?.ping st).bob in
+
+  trigger_event alice (Finishing {alice; bob; n_a});*
+  set_state alice sid (ReceivedAck {bob; n_a});*
+
+  return (Some sid)
diff --git a/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst b/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
new file mode 100644
index 0000000..3ca8565
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
@@ -0,0 +1,42 @@
+module DY.OnlineA.Run.Printing
+
+open DY.Core
+open DY.Lib
+open Comparse
+
+open DY.OnlineA.Data
+
+/// Helper functions for trace printing.
+/// Here we define how our abstract message and state types
+/// should be printed.
+
+
+val message_to_string: bytes -> option string
+let message_to_string b =
+  match? parse message_t b with
+  | Ping p -> Some (Printf.sprintf "Ping [name = (%s), n_a = (%s)]" (p.alice) (bytes_to_string p.n_a))
+  | Ack a -> Some (Printf.sprintf "Ping [n_a = (%s)]" (bytes_to_string a.n_a))
+
+
+val state_to_string: bytes -> option string
+let state_to_string b =
+  match? parse state_t b with
+  | SentPing p -> Some (Printf.sprintf "SentPing [n_a = (%s), to = (%s)]" (bytes_to_string p.n_a) p.bob)
+  | SentAck a -> Some (Printf.sprintf "SentAck [n_a = (%s), to = (%s)]" (bytes_to_string a.n_a) a.alice)
+  | ReceivedAck r -> Some (Printf.sprintf "ReceivedAck [n_a = (%s), from = (%s)]" (bytes_to_string r.n_a) r.bob)
+
+val event_to_string: bytes -> option string
+let event_to_string b =
+  match? parse event_t b with
+  | Initiating {alice; bob; n_a} -> Some (Printf.sprintf "Initiating [alice = (%s), n_a = (%s), to = (%s)]" alice (bytes_to_string n_a) bob)
+  | Responding {alice; bob; n_a} -> Some (Printf.sprintf "Responding [bob = (%s), n_a = (%s), to = (%s)]" bob (bytes_to_string n_a) alice)
+  | Finishing {alice; bob; n_a} -> Some (Printf.sprintf "Finishing [alice = (%s), n_a = (%s), with = (%s)]" alice (bytes_to_string n_a) bob)
+
+
+
+val get_trace_to_string_printers: trace_to_string_printers
+let get_trace_to_string_printers  = 
+  trace_to_string_printers_builder 
+    message_to_string
+    [(local_state_state.tag, state_to_string)]
+    [(event_event_t.tag, event_to_string)]
diff --git a/examples/Online_with_authn/DY.OnlineA.Run.fst b/examples/Online_with_authn/DY.OnlineA.Run.fst
new file mode 100644
index 0000000..b1462fd
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Run.fst
@@ -0,0 +1,83 @@
+module DY.OnlineA.Run
+
+open DY.Core
+open DY.Lib
+
+open DY.OnlineA.Run.Printing
+open DY.OnlineA.Data
+open DY.OnlineA.Protocol
+
+/// Here, we print the trace after a successful run of the Two Message protocol.
+
+
+let run () : traceful (option unit ) =
+  let _ = IO.debug_print_string "************* Trace *************\n" in
+
+  (*** Protocol Setup ***)
+
+  // the names of the participants
+  let alice = "Alice" in
+  let bob = "Bob" in
+
+  (*** PKI setup ***)
+
+  // Initialize key storage for Alice
+  // private and public keys are stored in separate sessions
+  let* alice_priv_keys_sid = initialize_private_keys alice in
+  let* alice_pub_keys_sid = initialize_pki alice in
+  // we collect both session ids in a global record
+  let alice_global_session_ids : global_sess_ids = 
+    { pki = alice_pub_keys_sid; 
+      private_keys = alice_priv_keys_sid
+    } in
+
+  // Initialize key storage for Bob
+  let* bob_priv_keys_sid = initialize_private_keys bob in
+  let* bob_pub_keys_sid = initialize_pki bob in  
+  let bob_global_session_ids: global_sess_ids = 
+    { pki = bob_pub_keys_sid; 
+      private_keys = bob_priv_keys_sid
+    } in
+
+  // Generate private key for Alice and store it in her private keys session
+  generate_private_key alice alice_global_session_ids.private_keys (LongTermPkeKey key_tag);*
+  
+  // Generate private key for Bob and store it in his private keys session
+  generate_private_key bob bob_global_session_ids.private_keys (LongTermPkeKey key_tag);*
+
+  // Store Bob's public key in Alice's state
+  // Bob's public key is computed from his private key
+  // 1. Retrieve Bob's private key from his private key session
+  // 2. Compute the public key from the private key
+  // 3. Install Bob's public key in Alice's public key store
+  let*? priv_key_bob = get_private_key bob bob_global_session_ids.private_keys (LongTermPkeKey key_tag) in
+  let pub_key_bob = pk priv_key_bob in
+  install_public_key alice alice_global_session_ids.pki (LongTermPkeKey key_tag) bob pub_key_bob;*
+
+  // Store Alice's public key in Bob's state in the same way
+  let*? priv_key_alice = get_private_key alice alice_global_session_ids.private_keys (LongTermPkeKey key_tag) in
+  let pub_key_alice = pk priv_key_alice in
+  install_public_key bob bob_global_session_ids.pki (LongTermPkeKey key_tag) alice pub_key_alice;*
+
+
+
+  (*** The actual protocol run ***)
+
+  // Alice sends a Ping to Bob
+  let*? (alice_sid, ping_ts) = send_ping alice bob alice_global_session_ids.pki in
+  // Bob replies with an Ack (reading the ping at the given timestamp)
+  let*? (bob_sid, ack_ts) = receive_ping_and_send_ack bob bob_global_session_ids ping_ts in
+  // Alice receives the Ack (at the given ack timestamp)
+  let*? _ = receive_ack alice alice_global_session_ids.private_keys ack_ts in
+
+
+ (*** Printing the Trace ***)
+
+  let* tr = get_trace in
+  let _ = IO.debug_print_string (
+      trace_to_string get_trace_to_string_printers tr
+    ) in
+
+  return (Some ())
+
+let _ = run () empty_trace
diff --git a/examples/Online_with_authn/Makefile b/examples/Online_with_authn/Makefile
new file mode 100644
index 0000000..32351e4
--- /dev/null
+++ b/examples/Online_with_authn/Makefile
@@ -0,0 +1,10 @@
+TUTORIAL_HOME ?= ../..
+
+EXAMPLES = Online_with_authn
+EXAMPLE_DIRS = $(addprefix $(TUTORIAL_HOME)/examples/, $(EXAMPLES))
+
+include $(TUTORIAL_HOME)/Makefile
+
+test:
+	cd $(TUTORIAL_HOME)/obj; $(FSTAR_EXE) --ocamlenv ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib DY_OnlineA_Run.native
+	$(TUTORIAL_HOME)/obj/DY_OnlineA_Run.native

From 432a388a5005784c1da66d78242ff5bfd62508cc Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Wed, 19 Feb 2025 13:31:54 +0100
Subject: [PATCH 2/9] adapt online authn to online secrecy

---
 .../Online_with_authn/DY.OnlineA.Data.fst     | 22 +-----
 .../DY.OnlineA.Invariants.Proofs.fst          | 70 +++++++++----------
 .../DY.OnlineA.Properties.fst                 | 10 +--
 .../Online_with_authn/DY.OnlineA.Protocol.fst | 43 +++++++-----
 examples/Online_with_authn/DY.OnlineA.Run.fst | 45 ++++--------
 5 files changed, 81 insertions(+), 109 deletions(-)

diff --git a/examples/Online_with_authn/DY.OnlineA.Data.fst b/examples/Online_with_authn/DY.OnlineA.Data.fst
index 02e75d6..9daf1ef 100644
--- a/examples/Online_with_authn/DY.OnlineA.Data.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Data.fst
@@ -111,7 +111,7 @@ instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes st
 /// so that they are distinguishable from any internal DY* states. 
 
 instance local_state_state: local_state state_t = {
-  tag = "P.State";
+  tag = "Online.State";
   format = parseable_serializeable_bytes_state_t;
 }
 
@@ -119,24 +119,11 @@ instance local_state_state: local_state state_t = {
 
 (*** PKI ***)
 
-/// For en-/de-cryption we assume some PKI.
-/// I.e., every participant has some private decryption keys
-/// and some public encryption keys from other participants.
-/// All private keys of a participant will be stored in one session
-/// and all public keys that the participant knows will be stored in another session.
-/// For each participant, we collect both these session IDs in a global record.
-
-type global_sess_ids = {
-  pki: state_id;
-  private_keys: state_id;
-}
-
 /// Similarly as for states,
 /// we tag the keys that are used on the protocol level,
 /// so that they can not be confused with other keys.
-/// (TODO: rephrase this)
 
-let key_tag = "P.Key"
+let key_tag = "Online.Key"
 
 
 (*** Event type ***)
@@ -151,8 +138,6 @@ let key_tag = "P.Key"
 /// Just as for messages and states,
 /// we define abstract event types
 
-
-
 /// The abstract type of the Initiating event
 [@@ with_bytes bytes]
 type ev_init_t = {
@@ -169,7 +154,6 @@ type ev_respond_t = {
   n_a:bytes
 }
 
-
 /// The abstract type of the Finishing event
 [@@ with_bytes bytes]
 type ev_finish_t = {
@@ -197,6 +181,6 @@ type event_t =
 
 /// Make the overall event type an instance of DY.Lib event class
 instance event_event_t: event event_t = {
-  tag = "P.Event";
+  tag = "Online.Event";
   format = mk_parseable_serializeable ps_event_t;
 }
diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
index ebc1451..b372278 100644
--- a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
@@ -26,16 +26,16 @@ open DY.OnlineA.Invariants
 (*** Sending a Ping maintains the invariants ***)
 
 val send_ping_invariant_short_version:
-  alice:principal -> bob:principal -> keys_sid:state_id ->
+  alice:principal -> bob:principal -> alice_private_keys_sid:state_id ->
   tr:trace ->
   Lemma
   ( requires trace_invariant tr
   )
   (ensures (
-    let (_ , tr_out) = send_ping alice bob keys_sid tr in
+    let (_ , tr_out) = send_ping alice bob alice_private_keys_sid tr in
     trace_invariant tr_out
   ))
-let send_ping_invariant_short_version alice bob keys_sid  tr =
+let send_ping_invariant_short_version alice bob alice_private_keys_sid  tr =
   let (n_a, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in
   (* We need to adapt the proof to the new send_ping function,
      where we trigger the Initiating event right after nonce generation.
@@ -43,22 +43,22 @@ let send_ping_invariant_short_version alice bob keys_sid  tr =
   let (_, tr_ev) = trigger_event alice (Initiating {alice; bob; n_a}) tr_rand in
   let ping = Ping {alice; n_a} in 
   serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_ev) ping;
-  pke_enc_for_is_publishable tr_ev alice bob keys_sid key_tag ping
+  pke_enc_for_is_publishable tr_ev alice bob alice_private_keys_sid key_tag ping
 
 
 (*** Replying to a Ping maintains the invariants ***)
 
 val decode_ping_invariant:
-  bob:principal -> keys_sid:state_id ->
+  bob:principal -> bob_private_keys_sid:state_id ->
   msg:bytes ->
   tr:trace ->
   Lemma
   (requires trace_invariant tr)
   (ensures (
-    let (_, tr_out) = decode_ping bob keys_sid msg tr in
+    let (_, tr_out) = decode_ping bob bob_private_keys_sid msg tr in
     trace_invariant tr_out
   ))
-let decode_ping_invariant bob keys_sid msg tr = ()
+let decode_ping_invariant bob bob_private_keys_sid msg tr = ()
 
 (* For the second protocol step (`receive_ping_and_send_ack`),
    we need a helper lemma: `decode_ping_proof`.
@@ -69,7 +69,7 @@ let decode_ping_invariant bob keys_sid msg tr = ()
 
 val decode_ping_proof:
   tr:trace ->
-  bob:principal -> keys_sid:state_id ->
+  bob:principal -> bob_private_keys_sid:state_id ->
   msg:bytes ->
   Lemma
   (requires (
@@ -77,11 +77,11 @@ val decode_ping_proof:
     /\ bytes_invariant tr msg
   ))
   (ensures (
-    match decode_ping bob keys_sid msg tr with
+    match decode_ping bob bob_private_keys_sid msg tr with
     | (None, _) -> True
     | (Some png, _) -> (
         let n_a = png.n_a in
-        let (sk_bob, _) = get_private_key bob keys_sid (LongTermPkeKey key_tag) tr in
+        let (sk_bob, _) = get_private_key bob bob_private_keys_sid (LongTermPkeKey key_tag) tr in
         Some? sk_bob /\
         bytes_invariant tr n_a /\
         is_knowable_by (nonce_label png.alice bob) tr n_a /\
@@ -91,11 +91,11 @@ val decode_ping_proof:
      )
    )
   )
-let decode_ping_proof tr bob keys_sid msg =
-    match decode_ping bob keys_sid msg tr with
+let decode_ping_proof tr bob bob_private_keys_sid msg =
+    match decode_ping bob bob_private_keys_sid msg tr with
     | (None, _) -> ()
     | (Some png, _) -> (
-        bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t bob keys_sid key_tag msg;
+        bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t bob bob_private_keys_sid key_tag msg;
         let plain = serialize message_t (Ping png) in
         parse_wf_lemma message_t (bytes_invariant tr) plain;
         FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain
@@ -108,20 +108,20 @@ let decode_ping_proof tr bob keys_sid msg =
 
 #push-options "--z3rlimit 30"
 val receive_ping_and_send_ack_invariant:
-  bob:principal -> keys_sid:global_sess_ids -> ts:timestamp ->
+  bob:principal -> bob_private_keys_sid:state_id -> bob_public_keys_sid:state_id -> ts:timestamp ->
   tr:trace ->
   Lemma
   ( requires trace_invariant tr
   )
   (ensures (
-    let (_ , tr_out) = receive_ping_and_send_ack bob keys_sid ts tr in
+    let (_ , tr_out) = receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid ts tr in
     trace_invariant tr_out
   ))
-let receive_ping_and_send_ack_invariant bob bob_keys_sid msg_ts tr =
+let receive_ping_and_send_ack_invariant bob bob_private_keys_sid bob_public_keys_sid msg_ts tr =
   match recv_msg msg_ts tr with
   | (None, _ ) -> ()
   | (Some msg, _) -> (
-      match decode_ping bob bob_keys_sid.private_keys msg tr with
+      match decode_ping bob bob_private_keys_sid msg tr with
       | (None, _) -> ()
       | (Some png, _) -> (
           let n_a = png.n_a in
@@ -150,12 +150,12 @@ let receive_ping_and_send_ack_invariant bob bob_keys_sid msg_ts tr =
              Looking at the pke_pred for the Ping,
              we get that alice must have triggered an Initiating event.
           *)
-          decode_ping_proof tr bob bob_keys_sid.private_keys msg;
+          decode_ping_proof tr bob bob_private_keys_sid msg;
           (* We thus get that the trace invariant is satisfied after triggering the event.
           *)
           assert(trace_invariant tr_ev);
 
-          match pke_enc_for bob alice bob_keys_sid.pki key_tag ack tr_ev with
+          match pke_enc_for bob alice bob_public_keys_sid key_tag ack tr_ev with
           | (None, _) -> ()
           | (Some ack_encrypted, tr_ack) ->(
                 assert(trace_invariant tr_ack);
@@ -175,7 +175,7 @@ let receive_ping_and_send_ack_invariant bob bob_keys_sid msg_ts tr =
                      You can check:
                      assert(pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) alice) (serialize message_t ack));
                   *)
-                pke_enc_for_is_publishable tr_ev bob alice bob_keys_sid.pki key_tag ack;
+                pke_enc_for_is_publishable tr_ev bob alice bob_public_keys_sid key_tag ack;
                 assert(trace_invariant tr_msg);
 
                 let st = (SentAck {alice = png.alice; n_a = png.n_a}) in
@@ -190,17 +190,17 @@ let receive_ping_and_send_ack_invariant bob bob_keys_sid msg_ts tr =
 (*** Receiving an Ack maintains the invariants ***)
 
 val decode_ack_invariant:
-  alice:principal -> keys_sid:state_id -> cipher:bytes ->
+  alice:principal -> alice_private_keys_sid:state_id -> cipher:bytes ->
   tr:trace ->
   Lemma
   (requires
     trace_invariant tr
   )
   (ensures (
-    let (_, tr_out) = decode_ack alice keys_sid cipher tr in
+    let (_, tr_out) = decode_ack alice alice_private_keys_sid cipher tr in
     trace_invariant tr_out
   ))
-let decode_ack_invariant alice keys_sid msg tr = ()
+let decode_ack_invariant alice alice_private_keys_sid msg tr = ()
 
 
 /// Since we now have a non-trivial property for the ReceivedAck state,
@@ -211,7 +211,7 @@ let decode_ack_invariant alice keys_sid msg tr = ()
 
 val decode_ack_proof:
   tr:trace ->
-  alice:principal -> keys_sid:state_id ->
+  alice:principal -> alice_private_keys_sid:state_id ->
   msg:bytes ->
   Lemma
   (requires (
@@ -219,11 +219,11 @@ val decode_ack_proof:
     /\ bytes_invariant tr msg
   ))
   (ensures (
-    match decode_ack alice keys_sid msg tr with
+    match decode_ack alice alice_private_keys_sid msg tr with
     | (None, _) -> True
     | (Some ack, _) -> (
         let n_a = ack.n_a in
-        let (sk_alice, _) = get_private_key alice keys_sid (LongTermPkeKey key_tag) tr in
+        let (sk_alice, _) = get_private_key alice alice_private_keys_sid (LongTermPkeKey key_tag) tr in
         Some? sk_alice /\
         bytes_invariant tr n_a /\
         ( is_publishable tr n_a
@@ -231,11 +231,11 @@ val decode_ack_proof:
         )
     )
   ))
-let decode_ack_proof tr alice keys_sid msg =
-    match decode_ack alice keys_sid msg tr with
+let decode_ack_proof tr alice alice_private_keys_sid msg =
+    match decode_ack alice alice_private_keys_sid msg tr with
     | (None, _) -> ()
     | (Some ack, _) -> (
-        bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t alice keys_sid key_tag msg;
+        bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t alice alice_private_keys_sid key_tag msg;
         let plain = serialize message_t (Ack ack) in
         parse_wf_lemma message_t (bytes_invariant tr) plain;
         FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain
@@ -280,21 +280,21 @@ let event_initiating_injective tr alice bob bob' n_a = ()
 
 #push-options "--z3rlimit 50"
 val receive_ack_invariant:
-  alice:principal -> keys_sid:state_id -> msg_ts:timestamp ->
+  alice:principal -> alice_private_keys_sid:state_id -> msg_ts:timestamp ->
   tr:trace ->
   Lemma
   (requires
     trace_invariant tr
   )
   (ensures (
-    let (_, tr_out) = receive_ack alice keys_sid msg_ts tr in
+    let (_, tr_out) = receive_ack alice alice_private_keys_sid msg_ts tr in
     trace_invariant tr_out
   ))
-let receive_ack_invariant alice keys_sid msg_ts tr =
+let receive_ack_invariant alice alice_private_keys_sid msg_ts tr =
   match recv_msg msg_ts tr with
   | (None, _) -> ()
   | (Some msg, _) -> (
-      match decode_ack alice keys_sid msg tr with
+      match decode_ack alice alice_private_keys_sid msg tr with
       | (None, _) -> ()
       | (Some ack, _) -> (
           let n_a = ack.n_a in
@@ -319,8 +319,8 @@ let receive_ack_invariant alice keys_sid msg_ts tr =
               // *)
               introduce ~(is_publishable tr n_a) ==> event_triggered tr bob (Responding {alice; bob; n_a})
               with _. (
-                decode_ack_proof tr alice keys_sid msg;
-                let (sk_alice, _) = get_private_key alice keys_sid (LongTermPkeKey key_tag) tr in
+                decode_ack_proof tr alice alice_private_keys_sid msg;
+                let (sk_alice, _) = get_private_key alice alice_private_keys_sid (LongTermPkeKey key_tag) tr in
                 assert(pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) alice) (pk (Some?.v sk_alice)) (serialize message_t (Ack ack)));
                 assert(exists bob'. event_triggered tr bob (Responding {alice; bob = bob'; n_a}));
                 (* From the pke_pred for the decoded Ack,
diff --git a/examples/Online_with_authn/DY.OnlineA.Properties.fst b/examples/Online_with_authn/DY.OnlineA.Properties.fst
index 9179980..e64312d 100644
--- a/examples/Online_with_authn/DY.OnlineA.Properties.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Properties.fst
@@ -3,7 +3,7 @@ module DY.OnlineA.Properties
 open Comparse
 open DY.Core
 open DY.Lib
-
+open DY.Simplified
 open DY.Extend
 
 open DY.OnlineA.Data
@@ -25,7 +25,7 @@ val responder_authentication:
      event_triggered_at tr ts alice (Finishing {alice; bob; n_a})
   )
   (ensures
-     is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob) \/
+     principal_is_corrupt tr alice \/ principal_is_corrupt tr bob \/
      event_triggered (prefix tr ts) bob (Responding {alice; bob; n_a})
   )
 let responder_authentication tr ts alice bob n_a = ()
@@ -37,12 +37,12 @@ val n_a_secrecy:
   tr:trace -> alice:principal -> bob:principal -> n_a:bytes ->
   Lemma
   (requires
-    attacker_knows tr n_a /\
     trace_invariant tr /\ (
       (state_was_set_some_id tr alice (SentPing {bob; n_a})) \/
       (state_was_set_some_id tr alice (ReceivedAck {bob; n_a} ))
-    )
+    ) /\
+    attacker_knows tr n_a
   )
-  (ensures is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob))
+  (ensures principal_is_corrupt tr alice \/ principal_is_corrupt tr bob)
 let n_a_secrecy tr alice bob n_a =
   attacker_only_knows_publishable_values tr n_a
diff --git a/examples/Online_with_authn/DY.OnlineA.Protocol.fst b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
index 498e04f..d01b99d 100644
--- a/examples/Online_with_authn/DY.OnlineA.Protocol.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
@@ -18,7 +18,7 @@ open DY.OnlineA.Data
 ///
 /// The model consists of 3 functions,
 /// one for each protocol step
-/// (just as for the simple two message protocol):
+/// (just as for the simple Two-Message protocol):
 /// 1. Alice sends the Ping to Bob (`send_ping`)
 /// 2. Bob receives the Ping and replies with the Ack (`receive_ping_and_send_ack`)
 /// 3. Alice receives the Ack (`receive_ack`)
@@ -45,7 +45,7 @@ open DY.OnlineA.Data
 let nonce_label alice bob = join (principal_label alice) (principal_label bob)
 
 val send_ping: principal -> principal -> state_id -> traceful (option (state_id & timestamp))
-let send_ping alice bob keys_sid =
+let send_ping alice bob alice_public_keys_sid =
   let* n_a = gen_rand_labeled (nonce_label alice bob) in
 
   (* This is the new step of triggering the Initiating event.
@@ -56,7 +56,7 @@ let send_ping alice bob keys_sid =
 
   let ping = Ping {alice; n_a} in 
 
-  let*? ping_encrypted = pke_enc_for alice bob keys_sid key_tag ping in
+  let*? ping_encrypted = pke_enc_for alice bob alice_public_keys_sid key_tag ping in
   let* msg_ts = send_msg ping_encrypted in
 
   let ping_state = SentPing {bob; n_a} in
@@ -79,7 +79,7 @@ let send_ping alice bob keys_sid =
 /// The step fails, if one of
 /// * decryption fails
 /// * the message is not of the right type, i.e., not a first message
-/// * encryption fails
+/// * encryption fails (for example, if Bob doesn't have a public key for Alice)
 
 /// Decrypting the message (Step 2 from above) is pulled out to a separate function
 /// The function
@@ -89,8 +89,8 @@ let send_ping alice bob keys_sid =
 /// The function fails if decryption fails.
 
 val decode_ping : principal -> state_id -> bytes -> traceful (option ping_t)
-let decode_ping bob keys_sid msg =
-  let*? png = pke_dec_with_key_lookup #message_t bob keys_sid key_tag msg in
+let decode_ping bob bob_private_keys_sid msg =
+  let*? png = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in
   
   guard_tr (Ping? png);*?
 
@@ -98,10 +98,10 @@ let decode_ping bob keys_sid msg =
 
 /// Now the actual receive and reply step
 /// using the decode function
-val receive_ping_and_send_ack: principal -> global_sess_ids -> timestamp -> traceful (option (state_id & timestamp))
-let receive_ping_and_send_ack bob global_sids msg_ts =
+val receive_ping_and_send_ack: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp))
+let receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid msg_ts =
   let*? msg = recv_msg msg_ts in
-  let*? png = decode_ping bob global_sids.private_keys msg in
+  let*? png = decode_ping bob bob_private_keys_sid msg in
 
   let n_a = png.n_a in
   let alice = png.alice in
@@ -111,10 +111,11 @@ let receive_ping_and_send_ack bob global_sids msg_ts =
   trigger_event bob (Responding {alice = alice; bob = bob; n_a = n_a});* 
 
   let ack = Ack {n_a} in
-  let*? ack_encrypted = pke_enc_for bob alice global_sids.pki key_tag ack in
+  let*? ack_encrypted = pke_enc_for bob alice bob_public_keys_sid key_tag ack in
   let* ack_ts = send_msg ack_encrypted in
-  
-  let* sess_id = start_new_session bob (SentAck {alice; n_a}) in
+
+  let ack_state = SentAck {alice; n_a} in
+  let* sess_id = start_new_session bob ack_state in
   
   return (Some (sess_id, ack_ts))
 
@@ -141,8 +142,8 @@ let receive_ping_and_send_ack bob global_sids msg_ts =
 /// Fails if decryption fails.
 
 val decode_ack : principal -> state_id -> bytes -> traceful (option ack_t)
-let decode_ack alice keys_sid cipher =
-  let*? ack = pke_dec_with_key_lookup #message_t alice keys_sid key_tag cipher in
+let decode_ack alice alice_private_keys_sid cipher =
+  let*? ack = pke_dec_with_key_lookup #message_t alice alice_private_keys_sid key_tag cipher in
 
   guard_tr (Ack? ack);*?
 
@@ -150,18 +151,22 @@ let decode_ack alice keys_sid cipher =
 
 /// The actual protocol step using the decode function
 val receive_ack: principal -> state_id -> timestamp -> traceful (option state_id)
-let receive_ack alice keys_sid ack_ts =
+let receive_ack alice alice_private_keys_sid ack_ts =
   let*? msg = recv_msg ack_ts in
-  let*? ack = decode_ack alice keys_sid msg in
+  let*? ack = decode_ack alice alice_private_keys_sid msg in
 
   let n_a = ack.n_a in
 
   let*? (sid, st) = lookup_state #state_t alice
-    (fun st -> SentPing? st && (SentPing?.ping st).n_a = n_a)
-    in
+    (fun st -> 
+          SentPing? st
+      && (SentPing?.ping st).n_a = n_a
+    ) in
   guard_tr(SentPing? st);*?
   let bob = (SentPing?.ping st).bob in
-
+  
+  (* This is the new step, where Alice triggers the Finishing event for the current run
+  *)
   trigger_event alice (Finishing {alice; bob; n_a});*
   set_state alice sid (ReceivedAck {bob; n_a});*
 
diff --git a/examples/Online_with_authn/DY.OnlineA.Run.fst b/examples/Online_with_authn/DY.OnlineA.Run.fst
index b1462fd..5f82698 100644
--- a/examples/Online_with_authn/DY.OnlineA.Run.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Run.fst
@@ -3,6 +3,8 @@ module DY.OnlineA.Run
 open DY.Core
 open DY.Lib
 
+open DY.Simplified
+
 open DY.OnlineA.Run.Printing
 open DY.OnlineA.Data
 open DY.OnlineA.Protocol
@@ -23,52 +25,33 @@ let run () : traceful (option unit ) =
 
   // Initialize key storage for Alice
   // private and public keys are stored in separate sessions
-  let* alice_priv_keys_sid = initialize_private_keys alice in
-  let* alice_pub_keys_sid = initialize_pki alice in
-  // we collect both session ids in a global record
-  let alice_global_session_ids : global_sess_ids = 
-    { pki = alice_pub_keys_sid; 
-      private_keys = alice_priv_keys_sid
-    } in
+  let* alice_private_keys_sid = initialize_private_keys alice in
+  let* alice_public_keys_sid = initialize_pki alice in
 
   // Initialize key storage for Bob
-  let* bob_priv_keys_sid = initialize_private_keys bob in
-  let* bob_pub_keys_sid = initialize_pki bob in  
-  let bob_global_session_ids: global_sess_ids = 
-    { pki = bob_pub_keys_sid; 
-      private_keys = bob_priv_keys_sid
-    } in
+  let* bob_private_keys_sid = initialize_private_keys bob in
+  let* bob_public_keys_sid = initialize_pki bob in  
 
   // Generate private key for Alice and store it in her private keys session
-  generate_private_key alice alice_global_session_ids.private_keys (LongTermPkeKey key_tag);*
+  generate_private_pke_key alice alice_private_keys_sid key_tag;*
   
   // Generate private key for Bob and store it in his private keys session
-  generate_private_key bob bob_global_session_ids.private_keys (LongTermPkeKey key_tag);*
+  generate_private_pke_key bob bob_private_keys_sid key_tag;*
 
   // Store Bob's public key in Alice's state
-  // Bob's public key is computed from his private key
-  // 1. Retrieve Bob's private key from his private key session
-  // 2. Compute the public key from the private key
-  // 3. Install Bob's public key in Alice's public key store
-  let*? priv_key_bob = get_private_key bob bob_global_session_ids.private_keys (LongTermPkeKey key_tag) in
-  let pub_key_bob = pk priv_key_bob in
-  install_public_key alice alice_global_session_ids.pki (LongTermPkeKey key_tag) bob pub_key_bob;*
-
-  // Store Alice's public key in Bob's state in the same way
-  let*? priv_key_alice = get_private_key alice alice_global_session_ids.private_keys (LongTermPkeKey key_tag) in
-  let pub_key_alice = pk priv_key_alice in
-  install_public_key bob bob_global_session_ids.pki (LongTermPkeKey key_tag) alice pub_key_alice;*
-
+  install_public_pke_key alice alice_public_keys_sid key_tag bob bob_private_keys_sid;*
 
+  // Store Alice's public key in Bob's state
+  install_public_pke_key bob bob_public_keys_sid key_tag alice alice_private_keys_sid;*
 
   (*** The actual protocol run ***)
 
   // Alice sends a Ping to Bob
-  let*? (alice_sid, ping_ts) = send_ping alice bob alice_global_session_ids.pki in
+  let*? (alice_sid, ping_ts) = send_ping alice bob alice_public_keys_sid in
   // Bob replies with an Ack (reading the ping at the given timestamp)
-  let*? (bob_sid, ack_ts) = receive_ping_and_send_ack bob bob_global_session_ids ping_ts in
+  let*? (bob_sid, ack_ts) = receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid ping_ts in
   // Alice receives the Ack (at the given ack timestamp)
-  let*? _ = receive_ack alice alice_global_session_ids.private_keys ack_ts in
+  receive_ack alice alice_private_keys_sid ack_ts;*?
 
 
  (*** Printing the Trace ***)

From 795acf20062256d4d5f44dbbed80fd86b13e94aa Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Wed, 19 Feb 2025 13:45:33 +0100
Subject: [PATCH 3/9] repair makefile

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index e977a87..6b546e3 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,7 @@ INNER_SOURCE_DIRS = dy-extensions
 # SOURCE_DIRS = $(addprefix $(DY_HOME)/src/, $(INNER_SOURCE_DIRS))
 SOURCE_DIRS = $(addprefix $(TUTORIAL_HOME)/, $(INNER_SOURCE_DIRS))
 
-INNER_EXAMPLE_DIRS = nsl_pk_only_one_event_lookup TwoMessageP Online Online_with_secrecy Online_wiht_authn
+INNER_EXAMPLE_DIRS = nsl_pk_only_one_event_lookup TwoMessageP Online Online_with_secrecy Online_with_authn
 EXAMPLE_DIRS ?= $(addprefix $(TUTORIAL_HOME)/examples/, $(INNER_EXAMPLE_DIRS))
 
 

From 68057f972ef3b7b9f2646a5bdfca91690c56ae66 Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Wed, 19 Feb 2025 16:31:20 +0100
Subject: [PATCH 4/9] cleanup

---
 .../Online_with_authn/DY.OnlineA.Data.fst     | 63 ++++---------------
 .../DY.OnlineA.Run.Printing.fst               |  7 +--
 2 files changed, 15 insertions(+), 55 deletions(-)

diff --git a/examples/Online_with_authn/DY.OnlineA.Data.fst b/examples/Online_with_authn/DY.OnlineA.Data.fst
index 9daf1ef..b44c715 100644
--- a/examples/Online_with_authn/DY.OnlineA.Data.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Data.fst
@@ -11,64 +11,41 @@ open DY.Lib
 ///
 /// (They are the same as for the simple 2 message protocol)
 
-(*** Message Type ***)
 
-/// for each of the two messages we define an abstract message type
+/// We only highlight the differences to the previous model
+/// for showing nonce secrecy.
+
+(*** Message Type ***)
 
-[@@ with_bytes bytes] // ignore this line for now
+[@@ with_bytes bytes]
 type ping_t = {
   alice: principal;
   n_a : bytes;
 }
 
-[@@ with_bytes bytes] // ignore this line for now
+[@@ with_bytes bytes]
 type ack_t = {
   n_a : bytes;
 }
 
 /// the overall abstract message type
-/// (consisting of constructors for the two messages
-/// and using the above abstract types for each of them)
 
-[@@ with_bytes bytes] // ignore this line for now
+[@@ with_bytes bytes]
 type message_t =
   | Ping: (ping:ping_t) -> message_t
   | Ack: (ack:ack_t) -> message_t
 
-
-/// We use Comparse to generate the corresponding message formats.
-/// I.e., we don't need to write parsing and serializing by hand
-///
-/// for this we need the `[@@ with_bytes bytes]` annotation for the message types above
-///
-/// We are not going into the details of how Comparse works.
-
-
-/// We let Comparse generate a parser `ps_ping_t` for the abstract `ping_t` type
-
 %splice [ps_ping_t] (gen_parser (`ping_t))
 
-/// ... and the same for the other abstract message types
-
 %splice [ps_ack_t] (gen_parser (`ack_t))
 
 %splice [ps_message_t] (gen_parser (`message_t))
 
-/// With the above parsers, we can make our `message` type an instance of
-/// Comparse's `parseable_serializeable` class.
-/// Again, the details are not important here,
-/// but this is the step that enables us to call
-/// `parse message buff` and `serialize message msg`
-/// to translate between bytes and our abstract message type.
-
 instance parseable_serializeable_bytes_message_t: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t
 
 
 (*** State Type ***)
 
-/// As for the messages we define abstract state types
-/// for the three states stored by Alice and Bob after each step of the protocol.
-
 [@@ with_bytes bytes]
 type sent_ping_t = {
   bob : principal;
@@ -93,23 +70,13 @@ type state_t =
   | SentAck: (ack:sent_ack_t) -> state_t
   | ReceivedAck: (rack:received_ack_t) -> state_t
 
-/// As for messages, we use Comparse to generate
-/// a parser and serializer for our abstract state types.
-
 %splice [ps_sent_ping_t] (gen_parser (`sent_ping_t))
 %splice [ps_sent_ack_t] (gen_parser (`sent_ack_t))
 %splice [ps_received_ack_t] (gen_parser (`received_ack_t))
 %splice [ps_state_t] (gen_parser (`state_t))
 
-/// Now, we can call
-/// `parse state buff` and `serialize state st`
-/// to translate between bytes and the abstract state type.
-
 instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes state_t = mk_parseable_serializeable ps_state_t
 
-/// We tag our protocol level states,
-/// so that they are distinguishable from any internal DY* states. 
-
 instance local_state_state: local_state state_t = {
   tag = "Online.State";
   format = parseable_serializeable_bytes_state_t;
@@ -119,22 +86,18 @@ instance local_state_state: local_state state_t = {
 
 (*** PKI ***)
 
-/// Similarly as for states,
-/// we tag the keys that are used on the protocol level,
-/// so that they can not be confused with other keys.
-
 let key_tag = "Online.Key"
 
 
 (*** Event type ***)
 
 /// We are now using events to show the authentication property.
-/// We will have two events for the first two protocol steps,
-/// i.e., there is an Initiating event
-/// that Alice triggers, when she starts a new run
-/// and a Responding event,
-/// that Bob triggers, when he replies to a Ping with an Ack.
-
+/// We have one event for each protocol step,
+/// that is
+/// * an Initiating event, that Alice triggers, when she starts a new run
+/// * a Responding event, that Bob triggers, when he replies to a Ping with an Ack
+/// * and a Finishing event, that Alice triggers, when she finishes a run.
+/// 
 /// Just as for messages and states,
 /// we define abstract event types
 
diff --git a/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst b/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
index 3ca8565..1272dd7 100644
--- a/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
@@ -7,17 +7,15 @@ open Comparse
 open DY.OnlineA.Data
 
 /// Helper functions for trace printing.
-/// Here we define how our abstract message and state types
+/// Here we define how our abstract message, state and event types
 /// should be printed.
 
-
 val message_to_string: bytes -> option string
 let message_to_string b =
   match? parse message_t b with
   | Ping p -> Some (Printf.sprintf "Ping [name = (%s), n_a = (%s)]" (p.alice) (bytes_to_string p.n_a))
   | Ack a -> Some (Printf.sprintf "Ping [n_a = (%s)]" (bytes_to_string a.n_a))
 
-
 val state_to_string: bytes -> option string
 let state_to_string b =
   match? parse state_t b with
@@ -31,8 +29,7 @@ let event_to_string b =
   | Initiating {alice; bob; n_a} -> Some (Printf.sprintf "Initiating [alice = (%s), n_a = (%s), to = (%s)]" alice (bytes_to_string n_a) bob)
   | Responding {alice; bob; n_a} -> Some (Printf.sprintf "Responding [bob = (%s), n_a = (%s), to = (%s)]" bob (bytes_to_string n_a) alice)
   | Finishing {alice; bob; n_a} -> Some (Printf.sprintf "Finishing [alice = (%s), n_a = (%s), with = (%s)]" alice (bytes_to_string n_a) bob)
-
-
+  
 
 val get_trace_to_string_printers: trace_to_string_printers
 let get_trace_to_string_printers  = 

From 81d7c00eb6f2de58e6a37bdcf0f3c46f1b65d2cd Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Wed, 19 Feb 2025 17:15:15 +0100
Subject: [PATCH 5/9] .

---
 examples/Online_with_authn/DY.OnlineA.Protocol.fst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/Online_with_authn/DY.OnlineA.Protocol.fst b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
index d01b99d..fbe59e8 100644
--- a/examples/Online_with_authn/DY.OnlineA.Protocol.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
@@ -10,7 +10,7 @@ open DY.Extend
 open DY.OnlineA.Data
 
 /// Here we define the DY* mode of the "Online?" protocol,
-/// an extension of the simple Two Message protocol:
+/// an extension of the simple Two-Message protocol:
 /// the two messages are now (asymmetrically) encrypted
 ///
 /// A -> B: enc{Ping (A, n_A)}_B

From 4ce62df77a47a95bd081b54f9d5717059fd6a5ff Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Mon, 24 Feb 2025 12:54:51 +0100
Subject: [PATCH 6/9] online: simplified the decode_xy post-conditions

---
 .../DY.OnlineA.Invariants.Proofs.fst          | 80 +++----------------
 1 file changed, 12 insertions(+), 68 deletions(-)

diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
index b372278..d4f7aa8 100644
--- a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
@@ -73,20 +73,18 @@ val decode_ping_proof:
   msg:bytes ->
   Lemma
   (requires (
-    trace_invariant tr
-    /\ bytes_invariant tr msg
+    trace_invariant tr /\ 
+    bytes_invariant tr msg
   ))
   (ensures (
     match decode_ping bob bob_private_keys_sid msg tr with
     | (None, _) -> True
     | (Some png, _) -> (
         let n_a = png.n_a in
-        let (sk_bob, _) = get_private_key bob bob_private_keys_sid (LongTermPkeKey key_tag) tr in
-        Some? sk_bob /\
-        bytes_invariant tr n_a /\
-        is_knowable_by (nonce_label png.alice bob) tr n_a /\
-        ( is_publishable tr n_a
-        \/ (pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) bob) (pk (Some?.v sk_bob)) (serialize message_t (Ping png)))
+        let alice = png.alice in
+        is_knowable_by (nonce_label alice bob) tr n_a /\
+        ( is_publishable tr n_a \/ 
+          event_triggered tr alice (Initiating {alice; bob; n_a}) 
         )
      )
    )
@@ -102,7 +100,6 @@ let decode_ping_proof tr bob bob_private_keys_sid msg =
     )
   
 
-
 /// The invariant lemma for the `receive_ping_and_send_ack` step
 
 
@@ -142,13 +139,7 @@ let receive_ping_and_send_ack_invariant bob bob_private_keys_sid bob_public_keys
              if the nonce n_a has not leaked,
              alice should have triggered an Initiating event.
 
-             We get this guarantee from our helper lemma decode_ping_proof:
-             The post-condition says
-             if the nonce has not leaked,
-             the pke_pred holds for the received Ping message.
-
-             Looking at the pke_pred for the Ping,
-             we get that alice must have triggered an Initiating event.
+             We get this guarantee from our helper lemma decode_ping_proof
           *)
           decode_ping_proof tr bob bob_private_keys_sid msg;
           (* We thus get that the trace invariant is satisfied after triggering the event.
@@ -215,20 +206,16 @@ val decode_ack_proof:
   msg:bytes ->
   Lemma
   (requires (
-    trace_invariant tr
-    /\ bytes_invariant tr msg
+    trace_invariant tr /\ 
+    bytes_invariant tr msg
   ))
   (ensures (
     match decode_ack alice alice_private_keys_sid msg tr with
     | (None, _) -> True
     | (Some ack, _) -> (
         let n_a = ack.n_a in
-        let (sk_alice, _) = get_private_key alice alice_private_keys_sid (LongTermPkeKey key_tag) tr in
-        Some? sk_alice /\
-        bytes_invariant tr n_a /\
-        ( is_publishable tr n_a
-        \/ (pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) alice) (pk (Some?.v sk_alice)) (serialize message_t (Ack ack)))
-        )
+        is_publishable tr n_a \/ 
+        exists bob. event_triggered tr bob (Responding {alice; bob; n_a})
     )
   ))
 let decode_ack_proof tr alice alice_private_keys_sid msg =
@@ -278,7 +265,6 @@ let event_initiating_injective tr alice bob bob' n_a = ()
 
 /// The invariant lemma for the final protocol step `receive_ack_invariant`
 
-#push-options "--z3rlimit 50"
 val receive_ack_invariant:
   alice:principal -> alice_private_keys_sid:state_id -> msg_ts:timestamp ->
   tr:trace ->
@@ -304,48 +290,7 @@ let receive_ack_invariant alice alice_private_keys_sid msg_ts tr =
           | (Some (sid, st), _) -> (
               let bob = (SentPing?.ping st).bob in
               let ((), tr_ev) = trigger_event alice (Finishing {alice; bob; n_a}) tr in
-              // We show that the trace invariant holds after triggering the event,
-              // that ist, we show that the event prediate for the Finishing event holds.
-
-              // from the SendPing state predicate
-              assert(event_triggered tr alice (Initiating {alice; bob; n_a}));
-
-              // also from the SendPing state predicate
-              assert(is_secret (nonce_label alice bob) tr n_a);
-              // immediate consequence of the exact label of n_a
-              assert(is_publishable tr n_a ==> is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob));
-              (* the more difficult case is the honest case,
-              //    when the nonce is not publishable
-              // *)
-              introduce ~(is_publishable tr n_a) ==> event_triggered tr bob (Responding {alice; bob; n_a})
-              with _. (
-                decode_ack_proof tr alice alice_private_keys_sid msg;
-                let (sk_alice, _) = get_private_key alice alice_private_keys_sid (LongTermPkeKey key_tag) tr in
-                assert(pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) alice) (pk (Some?.v sk_alice)) (serialize message_t (Ack ack)));
-                assert(exists bob'. event_triggered tr bob (Responding {alice; bob = bob'; n_a}));
-                (* From the pke_pred for the decoded Ack,
-                   we get that there is some bob' that 
-                   triggered a Responding event with Alice and n_a.
-                   So, we need to show, that this bob' is 
-                   the same as the bob stored in Alice's SendPing state.
-                *)
-                (* The event prediate for the Responding event of bob'
-                    guarantees, that alice must have triggered an Initiating event 
-                    containing bob'.
-                *)
-
-                assert(exists bob'. event_triggered tr alice (Initiating {alice; bob = bob'; n_a}));
-                (* We now use nonce injectivity from above to show that bob' = bob. *)
-                eliminate exists bob'. event_triggered tr alice (Initiating {alice; bob = bob'; n_a})
-                returns _
-                with _. (
-                  // from the state predicate of the looked up SendingPing state of Alice:
-                  assert(event_triggered tr alice (Initiating {alice; bob; n_a}));
-
-                  // the injectivity lemma from above, yields bob' = bob
-                  event_initiating_injective tr alice bob bob' n_a
-                )
-              );
+              decode_ack_proof tr alice alice_private_keys_sid msg;
               assert(trace_invariant tr_ev);
                                                    
               let newst = ReceivedAck {bob; n_a} in
@@ -356,4 +301,3 @@ let receive_ack_invariant alice alice_private_keys_sid msg_ts tr =
           )
       )
   )
-#pop-options

From 3abcacdbd1ea405a4fe1c11ad1580cda09fb84b4 Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Tue, 25 Feb 2025 10:17:37 +0100
Subject: [PATCH 7/9] small cleanup

---
 .../DY.OnlineA.Invariants.Proofs.fst          |  25 ++---
 .../DY.OnlineA.Invariants.fst                 | 106 +++++++-----------
 2 files changed, 49 insertions(+), 82 deletions(-)

diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
index d4f7aa8..b32ff6a 100644
--- a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
@@ -26,16 +26,16 @@ open DY.OnlineA.Invariants
 (*** Sending a Ping maintains the invariants ***)
 
 val send_ping_invariant_short_version:
-  alice:principal -> bob:principal -> alice_private_keys_sid:state_id ->
+  alice:principal -> bob:principal -> alice_public_keys_sid:state_id ->
   tr:trace ->
   Lemma
   ( requires trace_invariant tr
   )
   (ensures (
-    let (_ , tr_out) = send_ping alice bob alice_private_keys_sid tr in
+    let (_ , tr_out) = send_ping alice bob alice_public_keys_sid tr in
     trace_invariant tr_out
   ))
-let send_ping_invariant_short_version alice bob alice_private_keys_sid  tr =
+let send_ping_invariant_short_version alice bob alice_public_keys_sid tr =
   let (n_a, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in
   (* We need to adapt the proof to the new send_ping function,
      where we trigger the Initiating event right after nonce generation.
@@ -43,7 +43,7 @@ let send_ping_invariant_short_version alice bob alice_private_keys_sid  tr =
   let (_, tr_ev) = trigger_event alice (Initiating {alice; bob; n_a}) tr_rand in
   let ping = Ping {alice; n_a} in 
   serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_ev) ping;
-  pke_enc_for_is_publishable tr_ev alice bob alice_private_keys_sid key_tag ping
+  pke_enc_for_is_publishable tr_ev alice bob alice_public_keys_sid key_tag ping
 
 
 (*** Replying to a Ping maintains the invariants ***)
@@ -79,9 +79,7 @@ val decode_ping_proof:
   (ensures (
     match decode_ping bob bob_private_keys_sid msg tr with
     | (None, _) -> True
-    | (Some png, _) -> (
-        let n_a = png.n_a in
-        let alice = png.alice in
+    | (Some {alice; n_a}, _) -> (
         is_knowable_by (nonce_label alice bob) tr n_a /\
         ( is_publishable tr n_a \/ 
           event_triggered tr alice (Initiating {alice; bob; n_a}) 
@@ -102,8 +100,6 @@ let decode_ping_proof tr bob bob_private_keys_sid msg =
 
 /// The invariant lemma for the `receive_ping_and_send_ack` step
 
-
-#push-options "--z3rlimit 30"
 val receive_ping_and_send_ack_invariant:
   bob:principal -> bob_private_keys_sid:state_id -> bob_public_keys_sid:state_id -> ts:timestamp ->
   tr:trace ->
@@ -120,10 +116,7 @@ let receive_ping_and_send_ack_invariant bob bob_private_keys_sid bob_public_keys
   | (Some msg, _) -> (
       match decode_ping bob bob_private_keys_sid msg tr with
       | (None, _) -> ()
-      | (Some png, _) -> (
-          let n_a = png.n_a in
-          let alice = png.alice in
-          
+      | (Some {alice; n_a}, _) -> (          
           let ack = Ack {n_a} in
 
           (* We need to adapt the proof to the new receive_ping_and_send_ack function,
@@ -169,13 +162,12 @@ let receive_ping_and_send_ack_invariant bob bob_private_keys_sid bob_public_keys
                 pke_enc_for_is_publishable tr_ev bob alice bob_public_keys_sid key_tag ack;
                 assert(trace_invariant tr_msg);
 
-                let st = (SentAck {alice = png.alice; n_a = png.n_a}) in
+                let st = (SentAck {alice; n_a}) in
                 let (sess_id, tr_sess) = start_new_session bob st tr_msg in
                 assert(trace_invariant tr_sess)
            )
       )
   )
-#pop-options
 
 
 (*** Receiving an Ack maintains the invariants ***)
@@ -212,8 +204,7 @@ val decode_ack_proof:
   (ensures (
     match decode_ack alice alice_private_keys_sid msg tr with
     | (None, _) -> True
-    | (Some ack, _) -> (
-        let n_a = ack.n_a in
+    | (Some {n_a}, _) -> (
         is_publishable tr n_a \/ 
         exists bob. event_triggered tr bob (Responding {alice; bob; n_a})
     )
diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.fst
index 5cc76a5..02cff20 100644
--- a/examples/Online_with_authn/DY.OnlineA.Invariants.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.fst
@@ -3,7 +3,6 @@ module DY.OnlineA.Invariants
 open Comparse 
 open DY.Core
 open DY.Lib
-
 open DY.Extend
 
 open DY.OnlineA.Data
@@ -34,21 +33,18 @@ open DY.OnlineA.Protocol
 %splice [ps_ack_t_is_well_formed] (gen_is_well_formed_lemma (`ack_t))
 %splice [ps_message_t_is_well_formed] (gen_is_well_formed_lemma (`message_t))
 
-instance crypto_usages_p : crypto_usages = default_crypto_usages
+instance crypto_usages_online : crypto_usages = default_crypto_usages
 
-#push-options "--ifuel 2"
-let crypto_p : crypto_predicates = { 
+#push-options "--ifuel 3"
+let crypto_predicates_online : crypto_predicates = { 
   default_crypto_predicates with 
   pke_pred = { 
     pred = (fun tr sk_usage pk msg ->
-    exists prin.
-    (
+    exists prin. (
       sk_usage == long_term_key_type_to_usage (LongTermPkeKey key_tag) prin /\
       (match parse message_t msg with
-      | Some (Ping ping) ->
+      | Some (Ping {alice; n_a}) ->
           let bob = prin in
-          let alice = ping.alice in
-          let n_a = ping.n_a in
           get_label tr n_a == nonce_label alice bob
 
           (* We add, that the Alice specified in the Ping message,
@@ -59,7 +55,7 @@ let crypto_p : crypto_predicates = {
              * the nonce n_a in the Ping
           *)
           /\ event_triggered tr alice (Initiating {alice; bob; n_a})
-      | Some (Ack ack) ->
+      | Some (Ack {n_a}) ->
           (* For nonce secrecy,
              we didn't have any conditions/guarantees in the Ack case.
              Now, we add that 
@@ -69,7 +65,7 @@ let crypto_p : crypto_predicates = {
              * the nonce (n_a) in the Ack
           *)
           let alice = prin in
-          exists bob. event_triggered tr bob (Responding {alice; bob; n_a = ack.n_a})
+          exists bob. event_triggered tr bob (Responding {alice; bob; n_a})
       | _ -> False
       ))
       ); 
@@ -82,9 +78,9 @@ let crypto_p : crypto_predicates = {
 
 /// Collecting the usages and prediates in the final crypto invariants
 
-instance crypto_invariants_p: crypto_invariants = {
-  usages = crypto_usages_p;
-  preds =  crypto_p
+instance crypto_invariants_online: crypto_invariants = {
+  usages = crypto_usages_online;
+  preds =  crypto_predicates_online
 }
 
 
@@ -96,13 +92,11 @@ instance crypto_invariants_p: crypto_invariants = {
 %splice [ps_state_t_is_well_formed] (gen_is_well_formed_lemma (`state_t))
 
 #push-options "--ifuel 2 --z3cliopt 'smt.qi.eager_threshold=50'"
-let state_predicate_p: local_state_predicate state_t = {
+let state_predicate_online: local_state_predicate state_t = {
   pred = (fun tr prin sess_id st ->
     match st with
-    | SentPing ping -> (
+    | SentPing {bob; n_a} -> (
         let alice = prin in
-        let bob = ping.bob in
-        let n_a = ping.n_a in
         is_secret (nonce_label alice bob) tr n_a
         (* We add, that the storing principal (alice),
            must have triggered an Initiating event with:
@@ -110,12 +104,10 @@ let state_predicate_p: local_state_predicate state_t = {
            * the bob stored in the state and
            * the nonce stored in the state
         *)
-        /\ event_triggered tr alice (Initiating {alice = alice; bob = bob; n_a = n_a})
+        /\ event_triggered tr alice (Initiating {alice; bob; n_a})
     )
-    | SentAck ack -> (
+    | SentAck {alice; n_a} -> (
         let bob = prin in
-        let alice = ack.alice in
-        let n_a = ack.n_a in
         is_knowable_by (principal_label bob) tr n_a
         (* Additionally, we enforce that
            the storing principal (bob) 
@@ -126,10 +118,8 @@ let state_predicate_p: local_state_predicate state_t = {
         *)
         /\ event_triggered tr bob (Responding {alice; bob; n_a})
     )
-    | ReceivedAck rack  -> (
+    | ReceivedAck {bob; n_a}  -> (
         let alice = prin in
-        let bob = rack.bob in
-        let n_a = rack.n_a in
         is_secret (nonce_label alice bob) tr n_a
 
         (* We add, that the storing principal (alice),
@@ -147,22 +137,19 @@ let state_predicate_p: local_state_predicate state_t = {
 #pop-options
 
 
-(*** Event Pred ***)
+(*** Event Predicates ***)
 
 /// As for messages and states,
-/// we also have prediates on events.
+/// we also have predicates on events.
 /// The intuition is similar:
 /// They say when an event is allowed to be triggered, or
 /// what guarantees we obtain, if we observe a specific event on the trace.
 
-let event_predicate_event_t: event_predicate event_t =
+let event_predicate_online: event_predicate event_t =
   fun tr prin e ->
   // prin is the principal triggering the event
     match e with    
-    | Initiating init -> (
-        let alice = init.alice in
-        let bob = init.bob in
-        let n_a = init.n_a in
+    | Initiating {alice; bob; n_a} -> (
         (* We may trigger the Initiating event only if,
            * the triggering principal is the first principal stored in the event (alice)
            * the nonce (n_a) in the event is labelled for 
@@ -175,10 +162,7 @@ let event_predicate_event_t: event_predicate event_t =
         is_secret (nonce_label alice bob) tr n_a /\
         rand_just_generated tr n_a
     )
-    | Responding resp -> (
-        let alice = resp.alice in
-        let bob = resp.bob in
-        let n_a = resp.n_a in
+    | Responding {alice; bob; n_a} -> (
         (* A Responding event may only be triggered if,
            * the triggering principal is the second principal stored in the event (bob)
            * if the stored nonce n_a has not leaked,
@@ -186,21 +170,15 @@ let event_predicate_event_t: event_predicate event_t =
              must have triggered an Initiating event with the same data
              as the Responding event
         *)
-        prin == bob
-        /\ (is_publishable tr n_a
-          \/ event_triggered tr alice (Initiating {alice; bob; n_a})
-        )
+        prin == bob /\ 
+        ( is_publishable tr n_a \/
+          event_triggered tr alice (Initiating {alice; bob; n_a}))
     )
-    | Finishing fin -> (
-        let alice = fin.alice in
-        let bob = fin.bob in
-        let n_a = fin.n_a in
-
+    | Finishing {alice; bob; n_a} -> (
         prin == alice /\
         event_triggered tr alice (Initiating {alice; bob; n_a}) /\
         ( is_corrupt tr (nonce_label alice bob) \/
-          event_triggered tr bob (Responding {alice; bob; n_a})
-        )
+          event_triggered tr bob (Responding {alice; bob; n_a}))
     )
 
 
@@ -209,13 +187,13 @@ let event_predicate_event_t: event_predicate event_t =
 let all_sessions = [
   pki_tag_and_invariant;
   private_keys_tag_and_invariant;
-  (|local_state_state.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_p|);
+  (|local_state_state.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_online|);
 ]
 
 /// Now we have an event type
-let all_events = [(event_event_t.tag, compile_event_pred event_predicate_event_t)]
+let all_events = [(event_event_t.tag, compile_event_pred event_predicate_online)]
 
-let trace_invariants_p: trace_invariants = {
+let trace_invariants_online: trace_invariants = {
   state_pred = mk_state_pred all_sessions;
   event_pred = mk_event_pred all_events;
 }
@@ -223,13 +201,12 @@ let trace_invariants_p: trace_invariants = {
 
 (*** Protocol Invariants ***)
 
-instance protocol_invariants_p: protocol_invariants = {
-  crypto_invs = crypto_invariants_p;
-  trace_invs = trace_invariants_p;
+instance protocol_invariants_online: protocol_invariants = {
+  crypto_invs = crypto_invariants_online;
+  trace_invs = trace_invariants_online;
 }
 
-
-(*** Helper Lemmas for the Secrecy Proof ***)
+/// Lemmas that the global state predicate contains all the local ones
 
 val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate) all_sessions))
 let all_sessions_has_all_sessions () =
@@ -237,25 +214,24 @@ let all_sessions_has_all_sessions () =
   mk_state_pred_correct all_sessions;
   norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate) all_sessions)
 
-val protocol_invariants_p_has_p_session_invariant: squash (has_local_state_predicate state_predicate_p)
+val protocol_invariants_p_has_p_session_invariant: squash (has_local_state_predicate state_predicate_online)
 let protocol_invariants_p_has_p_session_invariant = all_sessions_has_all_sessions ()
 
-val protocol_invariants_p_has_pki_invariant: squash (has_pki_invariant #protocol_invariants_p)
+val protocol_invariants_p_has_pki_invariant: squash (has_pki_invariant #protocol_invariants_online)
 let protocol_invariants_p_has_pki_invariant = all_sessions_has_all_sessions ()
 
-val protocol_invariants_p_has_private_keys_invariant: squash (has_private_keys_invariant #protocol_invariants_p)
+val protocol_invariants_p_has_private_keys_invariant: squash (has_private_keys_invariant #protocol_invariants_online)
 let protocol_invariants_p_has_private_keys_invariant = all_sessions_has_all_sessions ()
 
+/// Lemmas that the global event predicate contains all the local ones
 
-/// We need similar lemmas for our event type
-
-val all_events_has_all_events: unit -> Lemma (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events))
+val all_events_has_all_events: unit -> Lemma (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_online) all_events))
 let all_events_has_all_events () =
   assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_events)));
-  mk_event_pred_correct #protocol_invariants_p all_events;
-  norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events);
+  mk_event_pred_correct #protocol_invariants_online all_events;
+  norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_online) all_events);
   let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in
-  dumb_lemma (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_p) all_events))
+  dumb_lemma (for_allP (has_compiled_event_pred #protocol_invariants_online) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_online) all_events))
 
-val protocol_invariants_p_has_event_t_invariant: squash (has_event_pred event_predicate_event_t)
+val protocol_invariants_p_has_event_t_invariant: squash (has_event_pred event_predicate_online)
 let protocol_invariants_p_has_event_t_invariant = all_events_has_all_events ()

From ec5be9df3fa16f1eb0d0b5b52302ca03193cd90a Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Thu, 27 Feb 2025 12:33:30 +0100
Subject: [PATCH 8/9] cleanup

---
 examples/Online/DY.Online.Data.fst            |  2 +-
 examples/Online/DY.Online.Run.Printing.fst    |  6 +-
 .../Online_with_authn/DY.OnlineA.Data.fst     |  2 +-
 .../DY.OnlineA.Invariants.Proofs.fst          | 23 +++-----
 .../DY.OnlineA.Invariants.fst                 | 11 +++-
 .../DY.OnlineA.Properties.fst                 |  1 +
 .../Online_with_authn/DY.OnlineA.Protocol.fst |  7 ++-
 .../DY.OnlineA.Run.Printing.fst               |  4 +-
 .../Online_with_secrecy/DY.OnlineS.Data.fst   |  2 +-
 .../DY.OnlineS.Invariants.Proofs.fst          | 48 ++++++----------
 .../DY.OnlineS.Invariants.fst                 | 55 ++++++++-----------
 .../DY.OnlineS.Protocol.fst                   |  2 -
 .../DY.OnlineS.Run.Printing.fst               |  8 +--
 examples/TwoMessageP/DY.TwoMessage.Data.fst   |  2 +-
 .../DY.TwoMessage.Run.Printing.fst            |  2 +-
 15 files changed, 71 insertions(+), 104 deletions(-)

diff --git a/examples/Online/DY.Online.Data.fst b/examples/Online/DY.Online.Data.fst
index 741569b..57c5a9e 100644
--- a/examples/Online/DY.Online.Data.fst
+++ b/examples/Online/DY.Online.Data.fst
@@ -110,7 +110,7 @@ instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes st
 /// We tag our protocol level states,
 /// so that they are distinguishable from any internal DY* states. 
 
-instance local_state_state: local_state state_t = {
+instance local_state_state_t: local_state state_t = {
   tag = "Online.State";
   format = parseable_serializeable_bytes_state_t;
 }
diff --git a/examples/Online/DY.Online.Run.Printing.fst b/examples/Online/DY.Online.Run.Printing.fst
index 60faa8a..908cfa7 100644
--- a/examples/Online/DY.Online.Run.Printing.fst
+++ b/examples/Online/DY.Online.Run.Printing.fst
@@ -12,13 +12,11 @@ open DY.Online.Data
 /// Here we define how our abstract message and state types
 /// should be printed.
 
-
 val message_to_string: bytes -> option string
 let message_to_string b =
   match? parse message_t b with
   | Ping p -> Some (Printf.sprintf "Ping [name = (%s), n_a = (%s)]" (p.alice) (bytes_to_string p.n_a))
-  | Ack a -> Some (Printf.sprintf "Ping [n_a = (%s)]" (bytes_to_string a.n_a))
-
+  | Ack a -> Some (Printf.sprintf "Ack [n_a = (%s)]" (bytes_to_string a.n_a))
 
 val state_to_string: bytes -> option string
 let state_to_string b =
@@ -32,5 +30,5 @@ val get_trace_to_string_printers: trace_to_string_printers
 let get_trace_to_string_printers  = 
   trace_to_string_printers_builder 
     message_to_string
-    ((local_state_state.tag, state_to_string) :: default_state_to_string)
+    ((local_state_state_t.tag, state_to_string) :: default_state_to_string)
     []
diff --git a/examples/Online_with_authn/DY.OnlineA.Data.fst b/examples/Online_with_authn/DY.OnlineA.Data.fst
index b44c715..d9c72b9 100644
--- a/examples/Online_with_authn/DY.OnlineA.Data.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Data.fst
@@ -77,7 +77,7 @@ type state_t =
 
 instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes state_t = mk_parseable_serializeable ps_state_t
 
-instance local_state_state: local_state state_t = {
+instance local_state_state_t: local_state state_t = {
   tag = "Online.State";
   format = parseable_serializeable_bytes_state_t;
 }
diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
index b32ff6a..b1b1172 100644
--- a/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
@@ -29,8 +29,7 @@ val send_ping_invariant_short_version:
   alice:principal -> bob:principal -> alice_public_keys_sid:state_id ->
   tr:trace ->
   Lemma
-  ( requires trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
     let (_ , tr_out) = send_ping alice bob alice_public_keys_sid tr in
     trace_invariant tr_out
@@ -73,7 +72,7 @@ val decode_ping_proof:
   msg:bytes ->
   Lemma
   (requires (
-    trace_invariant tr /\ 
+    trace_invariant tr /\
     bytes_invariant tr msg
   ))
   (ensures (
@@ -84,9 +83,8 @@ val decode_ping_proof:
         ( is_publishable tr n_a \/ 
           event_triggered tr alice (Initiating {alice; bob; n_a}) 
         )
-     )
-   )
-  )
+    )
+  ))
 let decode_ping_proof tr bob bob_private_keys_sid msg =
     match decode_ping bob bob_private_keys_sid msg tr with
     | (None, _) -> ()
@@ -104,8 +102,7 @@ val receive_ping_and_send_ack_invariant:
   bob:principal -> bob_private_keys_sid:state_id -> bob_public_keys_sid:state_id -> ts:timestamp ->
   tr:trace ->
   Lemma
-  ( requires trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
     let (_ , tr_out) = receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid ts tr in
     trace_invariant tr_out
@@ -176,9 +173,7 @@ val decode_ack_invariant:
   alice:principal -> alice_private_keys_sid:state_id -> cipher:bytes ->
   tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
     let (_, tr_out) = decode_ack alice alice_private_keys_sid cipher tr in
     trace_invariant tr_out
@@ -260,9 +255,7 @@ val receive_ack_invariant:
   alice:principal -> alice_private_keys_sid:state_id -> msg_ts:timestamp ->
   tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
     let (_, tr_out) = receive_ack alice alice_private_keys_sid msg_ts tr in
     trace_invariant tr_out
@@ -285,9 +278,7 @@ let receive_ack_invariant alice alice_private_keys_sid msg_ts tr =
               assert(trace_invariant tr_ev);
                                                    
               let newst = ReceivedAck {bob; n_a} in
-
               let ((), tr_st) = set_state alice sid newst tr_ev in
-              
               assert(trace_invariant tr_st)
           )
       )
diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.fst
index 02cff20..9ac5abb 100644
--- a/examples/Online_with_authn/DY.OnlineA.Invariants.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.fst
@@ -175,9 +175,16 @@ let event_predicate_online: event_predicate event_t =
           event_triggered tr alice (Initiating {alice; bob; n_a}))
     )
     | Finishing {alice; bob; n_a} -> (
+        (* A Finishing event may only be triggered if,
+           * the triggering principal is the first principal stored in the event (alice)
+           * the same principal triggered an Initiating event with the same bob and n_a
+           * if the stored nonce n_a has not leaked,
+             then the second stored principal (bob)
+             must have triggered a Responding event with the same data
+        *)
         prin == alice /\
         event_triggered tr alice (Initiating {alice; bob; n_a}) /\
-        ( is_corrupt tr (nonce_label alice bob) \/
+        ( is_publishable tr n_a \/
           event_triggered tr bob (Responding {alice; bob; n_a}))
     )
 
@@ -187,7 +194,7 @@ let event_predicate_online: event_predicate event_t =
 let all_sessions = [
   pki_tag_and_invariant;
   private_keys_tag_and_invariant;
-  (|local_state_state.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_online|);
+  (|local_state_state_t.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_online|);
 ]
 
 /// Now we have an event type
diff --git a/examples/Online_with_authn/DY.OnlineA.Properties.fst b/examples/Online_with_authn/DY.OnlineA.Properties.fst
index e64312d..7168c26 100644
--- a/examples/Online_with_authn/DY.OnlineA.Properties.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Properties.fst
@@ -27,6 +27,7 @@ val responder_authentication:
   (ensures
      principal_is_corrupt tr alice \/ principal_is_corrupt tr bob \/
      event_triggered (prefix tr ts) bob (Responding {alice; bob; n_a})
+     // /\ event_triggered (prefix tr ts) alice (Initiating {alice; bob; n_a})
   )
 let responder_authentication tr ts alice bob n_a = ()
 
diff --git a/examples/Online_with_authn/DY.OnlineA.Protocol.fst b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
index fbe59e8..738295a 100644
--- a/examples/Online_with_authn/DY.OnlineA.Protocol.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
@@ -33,6 +33,7 @@ open DY.OnlineA.Data
 
 /// Alice sends the first message to Bob:
 /// * Alice generates a new nonce [n_a]
+/// * triggers an "Initiating" event
 /// * encrypts the message (Alice, n_a) for Bob
 /// * sends the encrypted message
 /// * stores n_a and Bob in a state (in a new session)
@@ -71,6 +72,7 @@ let send_ping alice bob alice_public_keys_sid =
 /// Bob receives the first messages and replies:
 /// * read the message from the trace
 /// * decrypt the message to (Alice, n_a)
+/// * trigger a "Responding" event
 /// * encrypt the reply (n_a) for Alice
 /// * send the encrypted reply
 /// * store n_a and Alice in a state in a new session
@@ -102,9 +104,8 @@ val receive_ping_and_send_ack: principal -> state_id -> state_id -> timestamp ->
 let receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid msg_ts =
   let*? msg = recv_msg msg_ts in
   let*? png = decode_ping bob bob_private_keys_sid msg in
-
+  let alice = png.alice in  
   let n_a = png.n_a in
-  let alice = png.alice in
   
   (* This is the new step, where Bob triggers the Responding event for the current run
   *)
@@ -127,6 +128,7 @@ let receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid msg_t
 /// * read the message from the trace
 /// * decrypt the message to (n_a)
 /// * check if Alice previously sent n_a in some session
+/// * trigger a "Finishing" event
 /// * store completion of this session in a new state
 /// Returns the ID of the session that is marked as completed.
 /// The step fails, if one of
@@ -154,7 +156,6 @@ val receive_ack: principal -> state_id -> timestamp -> traceful (option state_id
 let receive_ack alice alice_private_keys_sid ack_ts =
   let*? msg = recv_msg ack_ts in
   let*? ack = decode_ack alice alice_private_keys_sid msg in
-
   let n_a = ack.n_a in
 
   let*? (sid, st) = lookup_state #state_t alice
diff --git a/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst b/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
index 1272dd7..0dc14c9 100644
--- a/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
@@ -14,7 +14,7 @@ val message_to_string: bytes -> option string
 let message_to_string b =
   match? parse message_t b with
   | Ping p -> Some (Printf.sprintf "Ping [name = (%s), n_a = (%s)]" (p.alice) (bytes_to_string p.n_a))
-  | Ack a -> Some (Printf.sprintf "Ping [n_a = (%s)]" (bytes_to_string a.n_a))
+  | Ack a -> Some (Printf.sprintf "Ack [n_a = (%s)]" (bytes_to_string a.n_a))
 
 val state_to_string: bytes -> option string
 let state_to_string b =
@@ -35,5 +35,5 @@ val get_trace_to_string_printers: trace_to_string_printers
 let get_trace_to_string_printers  = 
   trace_to_string_printers_builder 
     message_to_string
-    [(local_state_state.tag, state_to_string)]
+    [(local_state_state_t.tag, state_to_string)]
     [(event_event_t.tag, event_to_string)]
diff --git a/examples/Online_with_secrecy/DY.OnlineS.Data.fst b/examples/Online_with_secrecy/DY.OnlineS.Data.fst
index 18c14d8..9d02365 100644
--- a/examples/Online_with_secrecy/DY.OnlineS.Data.fst
+++ b/examples/Online_with_secrecy/DY.OnlineS.Data.fst
@@ -110,7 +110,7 @@ instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes st
 /// We tag our protocol level states,
 /// so that they are distinguishable from any internal DY* states. 
 
-instance local_state_state: local_state state_t = {
+instance local_state_state_t: local_state state_t = {
   tag = "Online.State";
   format = parseable_serializeable_bytes_state_t;
 }
diff --git a/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst b/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst
index 81536eb..11f3585 100644
--- a/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst
+++ b/examples/Online_with_secrecy/DY.OnlineS.Invariants.Proofs.fst
@@ -192,7 +192,7 @@ let send_ping_invariant alice bob alice_private_keys_sid  tr =
          bob is stored in the first component of the state.
          So the state prediate is satisfied:
       *)
-      assert(state_predicate_p.pred tr_msg alice sid st);
+      assert(state_predicate_online.pred tr_msg alice sid st);
       (* With this, we have all pre-conditions of `set_state_invariant`.
          Since that lemma comes with an SMT pattern,
          it is applied automatically.
@@ -208,20 +208,19 @@ let send_ping_invariant alice bob alice_private_keys_sid  tr =
    we end up with the following very short proof.
 *)
 val send_ping_invariant_short_version:
-  alice:principal -> bob:principal -> alice_private_keys_sid:state_id ->
+  alice:principal -> bob:principal -> alice_public_keys_sid:state_id ->
   tr:trace ->
   Lemma
-  ( requires trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
-    let (_ , tr_out) = send_ping alice bob alice_private_keys_sid tr in
+    let (_ , tr_out) = send_ping alice bob alice_public_keys_sid tr in
     trace_invariant tr_out
   ))
-let send_ping_invariant_short_version alice bob alice_private_keys_sid  tr =
+let send_ping_invariant_short_version alice bob alice_public_keys_sid tr =
   let (n_a, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in
   let ping = Ping {alice; n_a} in 
   serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_rand) ping;
-  pke_enc_for_is_publishable tr_rand alice bob alice_private_keys_sid key_tag ping
+  pke_enc_for_is_publishable tr_rand alice bob alice_public_keys_sid key_tag ping
 
 
 (*** Replying to a Ping maintains the invariants ***)
@@ -251,22 +250,14 @@ val decode_ping_proof:
   msg:bytes ->
   Lemma
   (requires (
-    trace_invariant tr
-    /\ bytes_invariant tr msg
+    trace_invariant tr /\
+    bytes_invariant tr msg
   ))
   (ensures (
     match decode_ping bob bob_private_keys_sid msg tr with
     | (None, _) -> True
-    | (Some png, _) -> (
-        let n_a = png.n_a in
-        let (sk_bob, _) = get_private_key bob bob_private_keys_sid (LongTermPkeKey key_tag) tr in
-        Some? sk_bob /\
-        bytes_invariant tr n_a /\
-        is_knowable_by (nonce_label png.alice bob) tr n_a /\
-        ( is_publishable tr n_a
-        \/ (pke_pred.pred tr (long_term_key_type_to_usage (LongTermPkeKey key_tag) bob) (pk (Some?.v sk_bob)) (serialize message_t (Ping png)))
-        )
-    )
+    | (Some {alice; n_a}, _) ->
+        is_knowable_by (nonce_label alice bob) tr n_a
   ))
 let decode_ping_proof tr bob bob_private_keys_sid msg =
     match decode_ping bob bob_private_keys_sid msg tr with
@@ -279,15 +270,13 @@ let decode_ping_proof tr bob bob_private_keys_sid msg =
     )
   
 
-
 /// The invariant lemma for the `receive_ping_and_send_ack` step
 
 val receive_ping_and_send_ack_invariant:
   bob:principal -> bob_private_keys_sid:state_id -> bob_public_keys_sid:state_id -> ts:timestamp ->
   tr:trace ->
   Lemma
-  ( requires trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
     let (_ , tr_out) = receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid ts tr in
     trace_invariant tr_out
@@ -322,8 +311,8 @@ let receive_ping_and_send_ack_invariant bob bob_private_keys_sid bob_public_keys
              //       tr_out == tr )
              //    = () in
           
-          let n_a = png.n_a in
           let alice = png.alice in
+          let n_a = png.n_a in
           
           let ack = Ack {n_a} in
           
@@ -385,7 +374,7 @@ let receive_ping_and_send_ack_invariant bob bob_private_keys_sid bob_public_keys
 
                    We get this property from our helper lemma `decode_ping_proof`.
                 *)
-                let st = (SentAck {alice = png.alice; n_a = png.n_a}) in
+                let st = (SentAck {alice; n_a}) in
                 let (sess_id, tr_sess) = start_new_session bob st tr_msg in
                 assert(trace_invariant tr_sess)
            )
@@ -393,21 +382,18 @@ let receive_ping_and_send_ack_invariant bob bob_private_keys_sid bob_public_keys
   )
 
 
-
 (*** Receiving an Ack maintains the invariants ***)
 
 val decode_ack_invariant:
   alice:principal -> alice_private_keys_sid:state_id -> cipher:bytes ->
   tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
     let (_, tr_out) = decode_ack alice alice_private_keys_sid cipher tr in
     trace_invariant tr_out
   ))
-let decode_ack_invariant alice keys_sid msg tr = ()
+let decode_ack_invariant alice alice_private_keys_sid msg tr = ()
 
 
 /// The invariant lemma for the final protocol step `receive_ack_invariant`
@@ -417,9 +403,7 @@ val receive_ack_invariant:
   alice:principal -> alice_private_keys_sid:state_id -> msg_ts:timestamp ->
   tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr
-  )
+  (requires trace_invariant tr)
   (ensures (
     let (_, tr_out) = receive_ack alice alice_private_keys_sid msg_ts tr in
     trace_invariant tr_out
diff --git a/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst b/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst
index 340e03d..8e7948d 100644
--- a/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst
+++ b/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst
@@ -35,10 +35,10 @@ open DY.OnlineS.Protocol
 
 
 // ignore this for now
-instance crypto_usages_p : crypto_usages = default_crypto_usages
+instance crypto_usages_online : crypto_usages = default_crypto_usages
 
-#push-options "--ifuel 2"
-let crypto_p : crypto_predicates = { 
+#push-options "--ifuel 3"
+let crypto_predicates_online : crypto_predicates = { 
   default_crypto_predicates with 
   (* we restrict when a message is allowed to be encrypted 
      with some secret key
@@ -57,7 +57,7 @@ let crypto_p : crypto_predicates = {
       *)
       sk_usage == long_term_key_type_to_usage (LongTermPkeKey key_tag) prin /\
       (match parse message_t msg with
-      | Some (Ping ping) ->
+      | Some (Ping {alice; n_a}) ->
           (* a Ping message can only be encrypted if
              (Or: if you decrypt a Ping from an honest party 
              you get the guarantees that:)
@@ -67,10 +67,8 @@ let crypto_p : crypto_predicates = {
              * and the intended receiver of the message (bob)
           *)
           let bob = prin in
-          let alice = ping.alice in
-          let n_a = ping.n_a in
           get_label tr n_a == nonce_label alice bob
-      | Some (Ack ack) ->
+      | Some (Ack {n_a}) ->
          (* No conditions / guarantees needed for an Ack *)
           True
       | _ -> False // other messages can not be encrypted
@@ -89,9 +87,9 @@ let crypto_p : crypto_predicates = {
 
 /// Collecting the usages and prediates in the final crypto invariants
 
-instance crypto_invariants_p: crypto_invariants = {
-  usages = crypto_usages_p;
-  preds =  crypto_p
+instance crypto_invariants_online: crypto_invariants = {
+  usages = crypto_usages_online;
+  preds =  crypto_predicates_online
 }
 
 
@@ -106,10 +104,10 @@ instance crypto_invariants_p: crypto_invariants = {
 
 #push-options "--ifuel 2 --z3cliopt 'smt.qi.eager_threshold=50'"
 (* We restrict what states are allowed to be stored by principals *)
-let state_predicate_p: local_state_predicate state_t = {
+let state_predicate_online: local_state_predicate state_t = {
   pred = (fun tr prin sess_id st ->
     match st with
-    | SentPing ping -> (
+    | SentPing {bob; n_a} -> (
         (* a SentPing state may only be stored if
            the stored nonce is labeled for
            * the storing principal (alice)
@@ -117,11 +115,9 @@ let state_predicate_p: local_state_predicate state_t = {
              (the intended receiver of the Ping: bob)
         *) 
         let alice = prin in
-        let bob = ping.bob in
-        let n_a = ping.n_a in
         is_secret (nonce_label alice bob) tr n_a
     )
-    | SentAck ack -> (
+    | SentAck {alice; n_a} -> (
         (* a SentAck state may only be stored if
            the stored nonce is readable by
            the storing principal (bob)
@@ -130,10 +126,9 @@ let state_predicate_p: local_state_predicate state_t = {
            and is enforced by the `pred_knowable` Lemma.
         *)
         let bob = prin in
-        let n_a = ack.n_a in
         is_knowable_by (principal_label bob) tr n_a
     )
-    | ReceivedAck rack  -> (
+    | ReceivedAck {bob; n_a}  -> (
         (* a ReceivedAck state may only be stored if
            the stored nonce is labeled for
            * the storing principal (alice)
@@ -141,8 +136,6 @@ let state_predicate_p: local_state_predicate state_t = {
              (the expected sender of the Ack)
         *)
         let alice = prin in
-        let bob = rack.bob in
-        let n_a = rack.n_a in
         is_secret (nonce_label alice bob) tr n_a
     )
   );
@@ -165,7 +158,7 @@ let state_predicate_p: local_state_predicate state_t = {
 let all_sessions = [
   pki_tag_and_invariant;
   private_keys_tag_and_invariant;
-  (|local_state_state.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_p|);
+  (|local_state_state_t.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_online|);
 ]
 
 /// We have no events here,
@@ -178,7 +171,7 @@ let all_events = []
 /// * the state invariant and
 /// * the event invariant
 
-let trace_invariants_p: trace_invariants = {
+let trace_invariants_online: trace_invariants = {
   state_pred = mk_state_pred all_sessions;
   event_pred = mk_event_pred all_events;
 }
@@ -191,17 +184,15 @@ let trace_invariants_p: trace_invariants = {
 /// * the crypto invariants and
 /// * the trace invariants
 
-instance protocol_invariants_p: protocol_invariants = {
-  crypto_invs = crypto_invariants_p;
-  trace_invs = trace_invariants_p;
+instance protocol_invariants_online: protocol_invariants = {
+  crypto_invs = crypto_invariants_online;
+  trace_invs = trace_invariants_online;
 }
 
+let complies_with_online_protocol tr = trace_invariant #protocol_invariants_online tr
 
-let complies_with_online_protocol tr = trace_invariant #protocol_invariants_p tr
-
-(*** Helper Lemmas for the Secrecy Proof ***)
-
-// TODO: Can all of this be hidden somehow?
+/// Lemmas that the global state predicate contains all the local ones
+(*TODO: can all of this be hidden ?*)
 
 val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate) all_sessions))
 let all_sessions_has_all_sessions () =
@@ -209,11 +200,11 @@ let all_sessions_has_all_sessions () =
   mk_state_pred_correct all_sessions;
   norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate) all_sessions)
 
-val protocol_invariants_p_has_p_session_invariant: squash (has_local_state_predicate state_predicate_p)
+val protocol_invariants_p_has_p_session_invariant: squash (has_local_state_predicate state_predicate_online)
 let protocol_invariants_p_has_p_session_invariant = all_sessions_has_all_sessions ()
 
-val protocol_invariants_p_has_pki_invariant: squash (has_pki_invariant #protocol_invariants_p)
+val protocol_invariants_p_has_pki_invariant: squash (has_pki_invariant #protocol_invariants_online)
 let protocol_invariants_p_has_pki_invariant = all_sessions_has_all_sessions ()
 
-val protocol_invariants_p_has_private_keys_invariant: squash (has_private_keys_invariant #protocol_invariants_p)
+val protocol_invariants_p_has_private_keys_invariant: squash (has_private_keys_invariant #protocol_invariants_online)
 let protocol_invariants_p_has_private_keys_invariant = all_sessions_has_all_sessions ()
diff --git a/examples/Online_with_secrecy/DY.OnlineS.Protocol.fst b/examples/Online_with_secrecy/DY.OnlineS.Protocol.fst
index 952b44d..be2f0b8 100644
--- a/examples/Online_with_secrecy/DY.OnlineS.Protocol.fst
+++ b/examples/Online_with_secrecy/DY.OnlineS.Protocol.fst
@@ -103,7 +103,6 @@ let receive_ping_and_send_ack bob bob_private_keys_sid bob_public_keys_sid msg_t
   let*? msg = recv_msg msg_ts in
   // decode the received expected ping
   let*? png = decode_ping bob bob_private_keys_sid msg in
-
   let alice = png.alice in
   let n_a = png.n_a in
 
@@ -157,7 +156,6 @@ let receive_ack alice alice_private_keys_sid ack_ts =
   let*? msg = recv_msg ack_ts in
   // decode the received expected ack
   let*? ack = decode_ack alice alice_private_keys_sid msg in
-
   let n_a = ack.n_a in
 
   let*? (sid, st) = lookup_state #state_t alice
diff --git a/examples/Online_with_secrecy/DY.OnlineS.Run.Printing.fst b/examples/Online_with_secrecy/DY.OnlineS.Run.Printing.fst
index 627327f..5d989d7 100644
--- a/examples/Online_with_secrecy/DY.OnlineS.Run.Printing.fst
+++ b/examples/Online_with_secrecy/DY.OnlineS.Run.Printing.fst
@@ -12,13 +12,11 @@ open DY.OnlineS.Data
 /// Here we define how our abstract message and state types
 /// should be printed.
 
-
 val message_to_string: bytes -> option string
 let message_to_string b =
   match? parse message_t b with
   | Ping p -> Some (Printf.sprintf "Ping [name = (%s), n_a = (%s)]" (p.alice) (bytes_to_string p.n_a))
-  | Ack a -> Some (Printf.sprintf "Ping [n_a = (%s)]" (bytes_to_string a.n_a))
-
+  | Ack a -> Some (Printf.sprintf "Ack [n_a = (%s)]" (bytes_to_string a.n_a))
 
 val state_to_string: bytes -> option string
 let state_to_string b =
@@ -28,11 +26,9 @@ let state_to_string b =
   | ReceivedAck r -> Some (Printf.sprintf "ReceivedAck [n_a = (%s), from = (%s)]" (bytes_to_string r.n_a) r.bob)
 
 
-
-
 val get_trace_to_string_printers: trace_to_string_printers
 let get_trace_to_string_printers  = 
   trace_to_string_printers_builder 
     message_to_string
-    ((local_state_state.tag, state_to_string) :: default_state_to_string)
+    ((local_state_state_t.tag, state_to_string) :: default_state_to_string)
     []
diff --git a/examples/TwoMessageP/DY.TwoMessage.Data.fst b/examples/TwoMessageP/DY.TwoMessage.Data.fst
index 5ac4e04..a8cd4e7 100644
--- a/examples/TwoMessageP/DY.TwoMessage.Data.fst
+++ b/examples/TwoMessageP/DY.TwoMessage.Data.fst
@@ -109,7 +109,7 @@ instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes st
 /// We tag our protocol level states,
 /// so that they are distinguishable from any internal DY* states. 
 
-instance local_state_state: local_state state_t = {
+instance local_state_state_t: local_state state_t = {
   tag = "TwoMessage.State";
   format = parseable_serializeable_bytes_state_t;
 }
diff --git a/examples/TwoMessageP/DY.TwoMessage.Run.Printing.fst b/examples/TwoMessageP/DY.TwoMessage.Run.Printing.fst
index 3605f64..cd83c87 100644
--- a/examples/TwoMessageP/DY.TwoMessage.Run.Printing.fst
+++ b/examples/TwoMessageP/DY.TwoMessage.Run.Printing.fst
@@ -30,5 +30,5 @@ val get_trace_to_string_printers: trace_to_string_printers
 let get_trace_to_string_printers  = 
   trace_to_string_printers_builder 
     message_to_string
-    [(local_state_state.tag, state_to_string)]
+    [(local_state_state_t.tag, state_to_string)]
     []

From 18148a64b25feeeba0c7b5d91b588d66dce0eb11 Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Thu, 27 Feb 2025 19:27:50 +0100
Subject: [PATCH 9/9] using event_triggered_before to hide prefix in
 authentication property

---
 examples/Online_with_authn/DY.OnlineA.Properties.fst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/Online_with_authn/DY.OnlineA.Properties.fst b/examples/Online_with_authn/DY.OnlineA.Properties.fst
index 7168c26..2f84485 100644
--- a/examples/Online_with_authn/DY.OnlineA.Properties.fst
+++ b/examples/Online_with_authn/DY.OnlineA.Properties.fst
@@ -26,8 +26,8 @@ val responder_authentication:
   )
   (ensures
      principal_is_corrupt tr alice \/ principal_is_corrupt tr bob \/
-     event_triggered (prefix tr ts) bob (Responding {alice; bob; n_a})
-     // /\ event_triggered (prefix tr ts) alice (Initiating {alice; bob; n_a})
+     event_triggered_before tr ts bob (Responding {alice; bob; n_a})
+     // /\ event_triggered_before tr ts alice (Initiating {alice; bob; n_a})
   )
 let responder_authentication tr ts alice bob n_a = ()