diff --git a/Makefile b/Makefile
index bd36999..e7d8c26 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 NSL_with_properties TwoMessageP Online Online_with_secrecy Basics
+INNER_EXAMPLE_DIRS = NSL NSL_with_properties TwoMessageP Online Online_with_secrecy Online_with_authn Basics
 EXAMPLE_DIRS ?= $(addprefix $(TUTORIAL_HOME)/examples/, $(INNER_EXAMPLE_DIRS))
 
 
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 a15fabe..908cfa7 100644
--- a/examples/Online/DY.Online.Run.Printing.fst
+++ b/examples/Online/DY.Online.Run.Printing.fst
@@ -12,14 +12,12 @@ 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 "Ack [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
@@ -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
new file mode 100644
index 0000000..d9c72b9
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Data.fst
@@ -0,0 +1,149 @@
+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)
+
+
+/// We only highlight the differences to the previous model
+/// for showing nonce secrecy.
+
+(*** Message Type ***)
+
+[@@ with_bytes bytes]
+type ping_t = {
+  alice: principal;
+  n_a : bytes;
+}
+
+[@@ with_bytes bytes]
+type ack_t = {
+  n_a : bytes;
+}
+
+/// the overall abstract message type
+
+[@@ with_bytes bytes]
+type message_t =
+  | Ping: (ping:ping_t) -> message_t
+  | Ack: (ack:ack_t) -> message_t
+
+%splice [ps_ping_t] (gen_parser (`ping_t))
+
+%splice [ps_ack_t] (gen_parser (`ack_t))
+
+%splice [ps_message_t] (gen_parser (`message_t))
+
+instance parseable_serializeable_bytes_message_t: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t
+
+
+(*** State Type ***)
+
+[@@ 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
+
+%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))
+
+instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes state_t = mk_parseable_serializeable ps_state_t
+
+instance local_state_state_t: local_state state_t = {
+  tag = "Online.State";
+  format = parseable_serializeable_bytes_state_t;
+}
+
+
+
+(*** PKI ***)
+
+let key_tag = "Online.Key"
+
+
+(*** Event type ***)
+
+/// We are now using events to show the authentication property.
+/// 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
+
+/// 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 = "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
new file mode 100644
index 0000000..b1b1172
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst
@@ -0,0 +1,285 @@
+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 -> alice_public_keys_sid:state_id ->
+  tr:trace ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    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_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.
+  *)
+  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_public_keys_sid key_tag ping
+
+
+(*** Replying to a Ping maintains the invariants ***)
+
+val decode_ping_invariant:
+  bob:principal -> bob_private_keys_sid:state_id ->
+  msg:bytes ->
+  tr:trace ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (_, tr_out) = decode_ping bob bob_private_keys_sid msg tr in
+    trace_invariant tr_out
+  ))
+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`.
+
+   Ignore this for now, and jump to the next lemma 
+   `receive_ping_and_send_ack_invariant`
+*)
+
+val decode_ping_proof:
+  tr:trace ->
+  bob:principal -> bob_private_keys_sid:state_id ->
+  msg:bytes ->
+  Lemma
+  (requires (
+    trace_invariant tr /\
+    bytes_invariant tr msg
+  ))
+  (ensures (
+    match decode_ping bob bob_private_keys_sid msg tr with
+    | (None, _) -> True
+    | (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}) 
+        )
+    )
+  ))
+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 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
+    )
+  
+
+/// 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)
+  (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
+  ))
+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_private_keys_sid msg tr with
+      | (None, _) -> ()
+      | (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,
+             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
+          *)
+          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_public_keys_sid 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_public_keys_sid key_tag ack;
+                assert(trace_invariant tr_msg);
+
+                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)
+           )
+      )
+  )
+
+
+(*** 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)
+  (ensures (
+    let (_, tr_out) = decode_ack alice alice_private_keys_sid cipher tr in
+    trace_invariant tr_out
+  ))
+let decode_ack_invariant alice alice_private_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 -> alice_private_keys_sid:state_id ->
+  msg:bytes ->
+  Lemma
+  (requires (
+    trace_invariant tr /\ 
+    bytes_invariant tr msg
+  ))
+  (ensures (
+    match decode_ack alice alice_private_keys_sid msg tr with
+    | (None, _) -> True
+    | (Some {n_a}, _) -> (
+        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 =
+    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 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
+    )
+  
+
+/// 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`
+
+val receive_ack_invariant:
+  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 alice_private_keys_sid msg_ts tr in
+    trace_invariant tr_out
+  ))
+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 alice_private_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
+              decode_ack_proof tr alice alice_private_keys_sid msg;
+              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
new file mode 100644
index 0000000..9ac5abb
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Invariants.fst
@@ -0,0 +1,244 @@
+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_online : crypto_usages = default_crypto_usages
+
+#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. (
+      sk_usage == long_term_key_type_to_usage (LongTermPkeKey key_tag) prin /\
+      (match parse message_t msg with
+      | Some (Ping {alice; n_a}) ->
+          let bob = prin 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 {n_a}) ->
+          (* 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})
+      | _ -> 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_online: crypto_invariants = {
+  usages = crypto_usages_online;
+  preds =  crypto_predicates_online
+}
+
+
+(*** 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_online: local_state_predicate state_t = {
+  pred = (fun tr prin sess_id st ->
+    match st with
+    | SentPing {bob; n_a} -> (
+        let alice = prin 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; bob; n_a})
+    )
+    | SentAck {alice; n_a} -> (
+        let bob = prin 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 {bob; n_a}  -> (
+        let alice = prin 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 Predicates ***)
+
+/// As for messages and states,
+/// 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_online: event_predicate event_t =
+  fun tr prin e ->
+  // prin is the principal triggering the event
+    match e with    
+    | 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 
+             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 {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,
+             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 {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_publishable tr n_a \/
+          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_t.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_online)]
+
+let trace_invariants_online: trace_invariants = {
+  state_pred = mk_state_pred all_sessions;
+  event_pred = mk_event_pred all_events;
+}
+
+
+(*** Protocol Invariants ***)
+
+instance protocol_invariants_online: protocol_invariants = {
+  crypto_invs = crypto_invariants_online;
+  trace_invs = trace_invariants_online;
+}
+
+/// 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 () =
+  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_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_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_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
+
+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_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_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_online)
+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..2f84485
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Properties.fst
@@ -0,0 +1,49 @@
+module DY.OnlineA.Properties
+
+open Comparse
+open DY.Core
+open DY.Lib
+open DY.Simplified
+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
+     principal_is_corrupt tr alice \/ principal_is_corrupt tr bob \/
+     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 = ()
+
+
+/// We still have nonce secrecy:
+
+val n_a_secrecy:
+  tr:trace -> alice:principal -> bob:principal -> n_a:bytes ->
+  Lemma
+  (requires
+    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 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
new file mode 100644
index 0000000..738295a
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Protocol.fst
@@ -0,0 +1,174 @@
+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]
+/// * 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)
+/// 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 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.
+     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 alice_public_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)
+/// * 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
+/// 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 (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
+/// * 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 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);*?
+
+  return (Some (Ping?.ping png))
+
+/// Now the actual receive and reply step
+/// using the decode function
+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 bob_private_keys_sid msg in
+  let alice = png.alice in  
+  let n_a = png.n_a 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 bob_public_keys_sid key_tag ack in
+  let* ack_ts = send_msg ack_encrypted 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))
+
+
+(*** 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
+/// * 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
+/// * 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 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);*?
+
+  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 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
+    (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});*
+
+  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..0dc14c9
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Run.Printing.fst
@@ -0,0 +1,39 @@
+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, 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 "Ack [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_t.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..5f82698
--- /dev/null
+++ b/examples/Online_with_authn/DY.OnlineA.Run.fst
@@ -0,0 +1,66 @@
+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
+
+/// 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_private_keys_sid = initialize_private_keys alice in
+  let* alice_public_keys_sid = initialize_pki alice in
+
+  // Initialize key storage for Bob
+  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_pke_key alice alice_private_keys_sid key_tag;*
+  
+  // Generate private key for Bob and store it in his private keys session
+  generate_private_pke_key bob bob_private_keys_sid key_tag;*
+
+  // Store Bob's public key in Alice's state
+  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_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_private_keys_sid bob_public_keys_sid ping_ts in
+  // Alice receives the Ack (at the given ack timestamp)
+  receive_ack alice alice_private_keys_sid ack_ts;*?
+
+
+ (*** 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
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)]
     []