diff --git a/.fst.config.json b/.fst.config.json
index 57d6d32..075a446 100644
--- a/.fst.config.json
+++ b/.fst.config.json
@@ -1,5 +1,5 @@
 { "fstar_exe":"fstar.exe",
   "options":["--cache_dir", "cache", "--hint_dir", "hints", "--use_hints", "--record_hints"],
   "include_dirs":[
-    "../comparse/src", "src/core", "src/lib", "src/lib/comparse", "src/lib/event", "src/lib/state", "src/lib/utils", "examples/nsl_pk"] 
+    "../comparse/src", "src/core", "src/lib", "src/lib/comparse", "src/lib/event", "src/lib/state", "src/lib/utils", "examples/nsl_pk", "examples/iso_dh"] 
 }
\ No newline at end of file
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 72a7dd0..4aea25e 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -216,6 +216,9 @@ In general the `requires` is a big conjunction,
 each hypothesis should be on a separate line.
 The `ensures` often contains a `let`, a `match`,
 in that case extra parenthesis are needed for F\*'s parser.
+Defining variables with the `let` keyword should be 
+replaced by inlining the statement directly into the function that 
+requires the variable if it does not blow up the statement too much.
 
 When the lemma is very short, it may be written on one line.
 
diff --git a/Makefile b/Makefile
index 0c617bf..f95d0dd 100644
--- a/Makefile
+++ b/Makefile
@@ -5,7 +5,7 @@ COMPARSE_HOME 	?= $(DY_HOME)/../comparse
 
 INNER_SOURCE_DIRS = core lib lib/comparse lib/event lib/state lib/utils
 SOURCE_DIRS = $(addprefix $(DY_HOME)/src/, $(INNER_SOURCE_DIRS))
-INNER_EXAMPLE_DIRS = nsl_pk
+INNER_EXAMPLE_DIRS = nsl_pk iso_dh
 EXAMPLE_DIRS = $(addprefix $(DY_HOME)/examples/, $(INNER_EXAMPLE_DIRS))
 
 INCLUDE_DIRS = $(SOURCE_DIRS) $(EXAMPLE_DIRS) $(COMPARSE_HOME)/src
diff --git a/README.md b/README.md
index 66e5b51..48cf201 100644
--- a/README.md
+++ b/README.md
@@ -15,7 +15,8 @@ we can find functions and theorems built on top of [`DY.Core`](src/core/DY.Core.
 
 ### Examples
 
-The NSL protocol is proved secure in the namespace [`DY.Example.NSL`](examples/nsl_pk/DY.Example.NSL.SecurityProperties.fst).
+The NSL protocol has been proven secure in the namespace [`DY.Example.NSL`](examples/nsl_pk/DY.Example.NSL.SecurityProperties.fst), and the ISO-DH protocol has been
+proven secure in the namespace [`DY.Example.DH`](examples/iso_dh).
 
 ## How to build
 
diff --git a/examples/iso_dh/DY.Example.DH.Debug.Proof.fst b/examples/iso_dh/DY.Example.DH.Debug.Proof.fst
new file mode 100644
index 0000000..a39b5ab
--- /dev/null
+++ b/examples/iso_dh/DY.Example.DH.Debug.Proof.fst
@@ -0,0 +1,30 @@
+module DY.Example.DH.Debug.Proof
+
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Stateful
+open DY.Example.DH.Protocol.Stateful.Proof
+open DY.Example.DH.Debug
+
+/// This module proves that the debug function
+/// fulfills the trace invariants.
+///
+/// The proof works automatically because each
+/// stateful proof as a SMTPat (`[SMTPat (trace_invariant tr); SMTPat (protocol_function)]`).
+/// Another way to do this proof is to basically
+/// duplicate the code from the debug function and
+/// call all the lemmas for the stateful code manually.
+
+#set-options "--fuel 0 --ifuel 0 --z3rlimit 10 --z3cliopt 'smt.qi.eager_threshold=100'"
+val debug_proof:
+  tr:trace ->
+  Lemma
+  (requires
+    trace_invariant tr
+  )
+  (ensures (
+    let (_, tr_out) = debug () tr in
+    trace_invariant tr_out
+    )
+  )
+let debug_proof tr = ()
diff --git a/examples/iso_dh/DY.Example.DH.Debug.fst b/examples/iso_dh/DY.Example.DH.Debug.fst
new file mode 100644
index 0000000..6338d15
--- /dev/null
+++ b/examples/iso_dh/DY.Example.DH.Debug.fst
@@ -0,0 +1,67 @@
+module DY.Example.DH.Debug
+
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Stateful
+
+
+let debug () : traceful (option unit)  =
+  let _ = IO.debug_print_string "************* Trace *************\n" in
+  (*** Initialize protocol run ***)
+  let alice = "alice" in
+  let bob = "bob" in
+
+  // Generate private key for Alice
+  let* alice_global_session_priv_key_id = initialize_private_keys alice in
+  generate_private_key alice alice_global_session_priv_key_id (Sign "DH.SigningKey");*
+  
+  // Generate private key for Bob
+  let* bob_global_session_priv_key_id = initialize_private_keys bob in
+  generate_private_key bob bob_global_session_priv_key_id (Sign "DH.SigningKey");*
+
+  // Store Bob's public key in Alice's state
+  // 1. Retrieve Bob's private key from his session
+  // 2. Compute the public key from the private key
+  // 3. Initialize Alice's session to store public keys
+  // 4. Install Bob's public key in Alice's public key store
+  let*? priv_key_bob = get_private_key bob bob_global_session_priv_key_id (Sign "DH.SigningKey") in
+  let pub_key_bob = vk priv_key_bob in
+  let* alice_global_session_pub_key_id = initialize_pki alice in
+  install_public_key alice alice_global_session_pub_key_id (Verify "DH.SigningKey") bob pub_key_bob;*
+
+  // Store Alice's public key in Bob's state
+  let*? priv_key_alice = get_private_key alice alice_global_session_priv_key_id (Sign "DH.SigningKey") in
+  let pub_key_alice = vk priv_key_alice in
+  let* bob_global_session_pub_key_id = initialize_pki bob in
+  install_public_key bob bob_global_session_pub_key_id (Verify "DH.SigningKey") alice pub_key_alice;*
+
+  let alice_global_session_ids: dh_global_sess_ids = {pki=alice_global_session_pub_key_id; private_keys=alice_global_session_priv_key_id} in
+  let bob_global_session_ids: dh_global_sess_ids = {pki=bob_global_session_pub_key_id; private_keys=bob_global_session_priv_key_id} in
+
+  (*** Run the protocol ***)
+  // Alice
+  let* alice_session_id = prepare_msg1 alice bob in
+  let*? msg1_id = send_msg1 alice alice_session_id in
+
+  // Bob
+  let*? bob_session_id = prepare_msg2 alice bob msg1_id in
+  let*? msg2_id = send_msg2 bob_global_session_ids bob bob_session_id in
+
+  // Alice
+  prepare_msg3 alice_global_session_ids alice alice_session_id bob msg2_id;*
+  let*? msg3_id = send_msg3 alice_global_session_ids alice bob alice_session_id in
+
+  // Bob
+  verify_msg3 bob_global_session_ids alice bob msg3_id bob_session_id;*
+
+  let* tr = get_trace in
+  let _ = IO.debug_print_string (
+      trace_to_string default_trace_to_string_printers tr
+    ) in
+
+  return (Some ())
+
+//Run ``debug ()`` when the module loads
+#push-options "--warn_error -272"
+let _ = debug () Nil
+#pop-options
\ No newline at end of file
diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst
new file mode 100644
index 0000000..2778bb4
--- /dev/null
+++ b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst
@@ -0,0 +1,386 @@
+module DY.Example.DH.Protocol.Stateful.Proof
+
+open Comparse
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Total
+open DY.Example.DH.Protocol.Total.Proof
+open DY.Example.DH.Protocol.Stateful
+
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 25  --z3cliopt 'smt.qi.eager_threshold=100'"
+
+(*** Trace invariants ***)
+
+/// The (local) state predicate.
+
+val is_dh_shared_key: trace -> principal -> principal -> bytes -> prop
+let is_dh_shared_key tr alice bob k = exists si sj.
+  // We are using the equivalent relation here because depending on the party we are looking at
+  // the label is either ``join (principal_state_label alice si) (principal_state_label bob sj)`` or
+  // ``join (principal_state_label bob sj) (principal_state_label alice si)``.
+  // This is because k is either build from ``dh x (dh_pk y)`` or ``dh y (dh_pk x)``.
+  get_label k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj) /\ 
+  get_usage k == AeadKey "DH.aead_key"
+
+let dh_session_pred: local_state_predicate dh_session = {
+  pred = (fun tr prin sess_id st ->
+    match st with
+    | InitiatorSentMsg1 bob x -> (
+      let alice = prin in
+      is_secret (principal_state_label alice sess_id) tr x /\
+      get_usage x == DhKey "DH.dh_key" /\
+      event_triggered tr alice (Initiate1 alice bob x)
+    )
+    | ResponderSentMsg2 alice gx gy y -> (
+      let bob = prin in
+      is_publishable tr gx /\ is_publishable tr gy /\
+      is_secret (principal_state_label bob sess_id) tr y /\ get_usage y  == DhKey "DH.dh_key" /\
+      gy == dh_pk y /\
+      event_triggered tr bob (Respond1 alice bob gx gy y)
+    )
+    | InitiatorSendMsg3 bob gx gy k -> (
+      let alice = prin in
+      is_publishable tr gx /\ is_publishable tr gy /\
+      is_knowable_by (principal_state_label alice sess_id) tr k /\
+      (exists x. gx == dh_pk x /\ k == dh x gy /\ is_secret (principal_state_label alice sess_id) tr x) /\
+      event_triggered tr alice (Initiate2 alice bob gx gy k) /\
+      (is_corrupt tr (principal_label bob) \/ is_corrupt tr (principal_state_label alice sess_id) \/
+      (exists y. k == dh y gx /\ is_dh_shared_key tr alice bob k /\ 
+        event_triggered tr bob (Respond1 alice bob gx gy y)))
+    )
+    | ResponderReceivedMsg3 alice gx gy k -> (
+      let bob = prin in
+      is_publishable tr gx /\ is_publishable tr gy /\
+      is_knowable_by (principal_state_label bob sess_id) tr k /\
+      (exists y. gy == dh_pk y /\ k == dh y gx /\ is_secret (principal_state_label bob sess_id) tr y) /\
+      event_triggered tr bob (Respond2 alice bob gx gy k) /\
+      (is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_state_label bob sess_id) \/
+        (is_dh_shared_key tr alice bob k /\ 
+        event_triggered tr alice (Initiate2 alice bob gx gy k)))
+    )
+  );
+  pred_later = (fun tr1 tr2 prin sess_id st -> ());
+  pred_knowable = (fun tr prin sess_id st -> ());
+}
+
+/// The (local) event predicate.
+
+let dh_event_pred: event_predicate dh_event =
+  fun tr prin e ->
+    match e with
+    | Initiate1 alice bob x -> True
+    | Respond1 alice bob gx gy y -> (
+      is_publishable tr gx /\ is_publishable tr gy /\
+      (exists sess_id. is_secret (principal_state_label bob sess_id) tr y) /\
+      get_usage y == DhKey "DH.dh_key" /\
+      gy = dh_pk y
+    )
+    | Initiate2 alice bob gx gy k -> (
+      is_publishable tr gx /\ is_publishable tr gy /\
+      (exists x sess_id. is_secret (principal_state_label alice sess_id) tr x /\
+      gx = dh_pk x /\ k == dh x gy) /\
+      ((exists alice_si. is_corrupt tr (principal_state_label alice alice_si)) \/ is_corrupt tr (principal_label bob) \/
+        (exists y. k == dh y gx /\ is_dh_shared_key tr alice bob k /\ event_triggered tr bob (Respond1 alice bob gx gy y)))
+    )
+    | Respond2 alice bob gx gy k -> (
+      is_corrupt tr (principal_label alice) \/ (exists bob_si. is_corrupt tr (principal_state_label bob bob_si)) \/
+      (is_dh_shared_key tr alice bob k /\
+        event_triggered tr alice (Initiate2 alice bob gx gy k))
+    )
+
+/// List of all local state predicates.
+
+let all_sessions = [
+  pki_tag_and_invariant;
+  private_keys_tag_and_invariant;
+  (local_state_dh_session.tag, local_state_predicate_to_local_bytes_state_predicate dh_session_pred);
+]
+
+/// List of all local event predicates.
+
+let all_events = [
+  (dh_event_instance.tag, compile_event_pred dh_event_pred)
+]
+
+/// Create the global trace invariants.
+
+let dh_trace_invs: trace_invariants (dh_crypto_invs) = {
+  state_pred = mk_state_predicate dh_crypto_invs all_sessions;
+  event_pred = mk_event_pred all_events;
+}
+
+instance dh_protocol_invs: protocol_invariants = {
+  crypto_invs = dh_crypto_invs;
+  trace_invs = dh_trace_invs;
+}
+
+/// 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 dh_protocol_invs) all_sessions))
+let all_sessions_has_all_sessions () =
+  assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sessions)));
+  mk_global_local_bytes_state_predicate_correct dh_protocol_invs all_sessions;
+  norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate dh_protocol_invs) all_sessions)
+
+val full_dh_session_pred_has_pki_invariant: squash (has_pki_invariant dh_protocol_invs)
+let full_dh_session_pred_has_pki_invariant = all_sessions_has_all_sessions ()
+
+val full_dh_session_pred_has_private_keys_invariant: squash (has_private_keys_invariant dh_protocol_invs)
+let full_dh_session_pred_has_private_keys_invariant = all_sessions_has_all_sessions ()
+
+val full_dh_session_pred_has_dh_invariant: squash (has_local_state_predicate dh_protocol_invs dh_session_pred)
+let full_dh_session_pred_has_dh_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 dh_protocol_invs) 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 dh_protocol_invs all_events;
+  norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) 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 dh_protocol_invs) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) all_events))
+
+val full_dh_event_pred_has_dh_invariant: squash (has_event_pred dh_protocol_invs dh_event_pred)
+let full_dh_event_pred_has_dh_invariant = all_events_has_all_events ()
+
+(*** Proofs ****)
+
+val prepare_msg1_proof:
+  tr:trace ->
+  alice:principal -> bob:principal ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (_, tr_out) = prepare_msg1 alice bob tr in
+    trace_invariant tr_out
+  ))
+  // The SMTPat is used to automatically proof that
+  // the debug trace fulfills the trace invariants.
+  // The SMTPat says that if the trace invariants hold on tr
+  // and the function prepare_msg1 is called then instantiate
+  // this lemma.
+  [SMTPat (trace_invariant tr); SMTPat (prepare_msg1 alice bob tr)]
+let prepare_msg1_proof tr alice bob = ()
+
+val send_msg1_proof:
+  tr:trace ->
+  alice:principal -> alice_si:state_id ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (msg_id, tr_out) = send_msg1 alice alice_si tr in
+    trace_invariant tr_out
+  ))
+  [SMTPat (trace_invariant tr); SMTPat (send_msg1 alice alice_si tr)]
+let send_msg1_proof tr alice alice_si =
+  match get_state alice alice_si tr with
+  | (Some (InitiatorSentMsg1 bob x), tr) -> (
+    compute_message1_proof tr alice bob x
+  )
+  | _ -> ()
+
+val prepare_msg2_proof:
+  tr:trace ->
+  alice:principal -> bob:principal -> msg_id:nat ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (msg_id, tr_out) = prepare_msg2 alice bob msg_id tr in
+    trace_invariant tr_out
+  ))
+  [SMTPat (trace_invariant tr); SMTPat (prepare_msg2 alice bob msg_id tr)]
+let prepare_msg2_proof tr alice bob msg_id =
+  match recv_msg msg_id tr with
+  | (Some msg, tr) -> (
+    decode_message1_proof tr msg
+  )
+  | (None, tr) -> ()
+
+val send_msg2_proof:
+  tr:trace ->
+  global_sess_id:dh_global_sess_ids -> bob:principal -> bob_si:state_id ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (msg_id, tr_out) = send_msg2 global_sess_id bob bob_si tr in
+    trace_invariant tr_out
+  ))
+  [SMTPat (trace_invariant tr); SMTPat (send_msg2 global_sess_id bob bob_si tr)]
+let send_msg2_proof tr global_sess_id bob bob_si =
+  match get_state bob bob_si tr with
+  | (Some (ResponderSentMsg2 alice gx gy y), tr) -> (
+    match get_private_key bob global_sess_id.private_keys (Sign "DH.SigningKey") tr with
+    | (Some sk_b, tr) -> (
+      let (n_sig, tr) = mk_rand SigNonce (principal_label bob) 32 tr in
+      compute_message2_proof tr alice bob gx y sk_b n_sig
+    )
+    | (None, tr) -> ()
+  )
+  | _ -> ()
+
+val prepare_msg3_proof:
+  tr:trace ->
+  global_sess_id:dh_global_sess_ids ->
+  alice:principal -> alice_si:state_id -> bob:principal ->
+  msg_id:nat ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (_, tr_out) = prepare_msg3 global_sess_id alice alice_si bob msg_id tr in
+    trace_invariant tr_out
+  ))
+  [SMTPat (trace_invariant tr); SMTPat (prepare_msg3 global_sess_id alice alice_si bob msg_id tr)]
+let prepare_msg3_proof tr global_sess_id alice alice_si bob msg_id =
+  match get_state alice alice_si tr with
+  | (Some (InitiatorSentMsg1 bob x), tr) -> (
+    match recv_msg msg_id tr with
+    | (Some msg_bytes, tr) -> (
+      match get_public_key alice global_sess_id.pki (Verify "DH.SigningKey") bob tr with
+      | (Some pk_b, tr) -> (
+        match decode_and_verify_message2 msg_bytes alice x pk_b with
+        | Some res -> (
+          decode_and_verify_message2_proof tr msg_bytes alice alice_si bob x pk_b;
+          
+          let k = dh x res.gy in
+
+          assert((exists x. res.gx == dh_pk x /\ k == dh x res.gy /\ is_secret (principal_state_label alice alice_si) tr x));
+
+          assert(is_publishable tr res.gx);
+          assert(is_publishable tr res.gy);
+          assert(is_knowable_by (principal_state_label alice alice_si) tr k);
+
+          assert((exists x sess_id. is_secret (principal_state_label alice sess_id) tr x /\
+            res.gx = dh_pk x));
+          assert(get_usage k = AeadKey "DH.aead_key");
+          assert(exists si. is_knowable_by (principal_state_label alice si) tr k);
+
+          let alice_and_bob_not_corrupt = (~(is_corrupt tr (principal_state_label alice alice_si) \/ is_corrupt tr (principal_label bob))) in
+          let dh_key_and_event_respond1 = (exists y. k == dh y res.gx /\ is_dh_shared_key tr alice bob k /\ event_triggered tr bob (Respond1 alice bob res.gx res.gy y)) in
+          introduce alice_and_bob_not_corrupt ==> dh_key_and_event_respond1 
+          with _. (
+            assert(exists y k'. k' == dh y res.gx /\ res.gy == dh_pk y /\ event_triggered tr bob (Respond1 alice bob res.gx res.gy y));
+            eliminate exists y k'. k' == dh y res.gx /\ event_triggered tr bob (Respond1 alice bob res.gx res.gy y)
+            returns dh_key_and_event_respond1
+            with _. (
+              assert(event_triggered tr bob (Respond1 alice bob res.gx res.gy y));
+              
+              assert(dh_pk y == res.gy);
+              assert(dh_pk x = res.gx);              
+              dh_shared_secret_lemma x y;
+              assert(dh y res.gx == dh x res.gy);
+              assert(k == k');
+              
+              assert(exists si sj. get_label k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj));
+
+              assert(dh_key_and_event_respond1);
+              ()
+            )
+          )
+        )
+        | None -> ()
+      )
+      | (None, tr) -> ()
+    )
+    | (None, tr) -> ()
+  )
+  | _ -> ()
+
+val send_msg3_proof:
+  tr:trace ->
+  global_sess_id:dh_global_sess_ids -> alice:principal -> alice_si:state_id -> bob:principal ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (_, tr_out) = send_msg3 global_sess_id alice bob alice_si tr in
+    trace_invariant tr_out
+  ))
+  [SMTPat (trace_invariant tr); SMTPat (send_msg3 global_sess_id alice bob alice_si tr)]
+let send_msg3_proof tr global_sess_id alice alice_si bob =
+  match get_state alice alice_si tr with
+  | (Some (InitiatorSendMsg3 bob gx gy k), tr') -> (
+    match get_private_key alice global_sess_id.private_keys (Sign "DH.SigningKey") tr' with
+    | (Some sk_a, tr') -> (
+      let (n_sig, tr') = mk_rand SigNonce (principal_label alice) 32 tr' in
+
+      // The following code is not needed for the proof.
+      // It just shows what we need to show to prove the lemma.
+      assert(event_triggered tr alice (Initiate2 alice bob gx gy k));
+      assert(exists x. event_triggered tr alice (Initiate2 alice bob gx gy (dh x gy)) /\ gx = dh_pk x);
+
+      eliminate exists x. event_triggered tr alice (Initiate2 alice bob gx gy (dh x gy)) /\ gx = dh_pk x
+      returns trace_invariant (snd (send_msg3 global_sess_id alice bob alice_si tr))
+      with _. (
+        compute_message3_proof tr' alice bob gx gy x sk_a n_sig
+      )
+    )
+    | (None, tr') -> ()
+  )
+  | _ -> ()
+
+#push-options "--z3rlimit 50"
+val verify_msg3_proof:
+  tr:trace ->
+  global_sess_id:dh_global_sess_ids -> alice:principal -> bob:principal -> msg_id:nat -> bob_si:state_id ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (_, tr_out) = verify_msg3 global_sess_id alice bob msg_id bob_si tr in
+    trace_invariant tr_out
+  ))
+  [SMTPat (trace_invariant tr); SMTPat (verify_msg3 global_sess_id alice bob msg_id bob_si tr)]
+let verify_msg3_proof tr global_sess_id alice bob msg_id bob_si =
+  match get_state bob bob_si tr with
+  | (Some (ResponderSentMsg2 alice gx gy y), tr) -> (
+    match recv_msg msg_id tr with
+    | (Some msg_bytes, tr) -> (
+      match get_public_key bob global_sess_id.pki (Verify "DH.SigningKey") alice tr with
+      | (Some pk_a, tr) -> (
+          decode_and_verify_message3_proof tr msg_bytes alice bob bob_si gx y pk_a;
+          
+          match decode_and_verify_message3 msg_bytes bob gx gy y pk_a with
+          | Some res -> (
+            assert(exists y. gy == dh_pk y /\ res.k == dh y gx /\ is_secret (principal_state_label bob bob_si) tr y);
+
+            assert(event_triggered tr bob (Respond1 alice bob gx gy y));
+            // The decode_message3_proof gives us that there exists a k' such that 
+            // the event Initiate2 has been triggered or alice is corrupt.
+            // On a high level we need to show now that this event was triggered
+            // for our concrete k.
+            assert(exists x. gx == dh_pk x /\ event_triggered tr alice (Initiate2 alice bob gx gy (dh x gy)) \/ 
+              is_corrupt tr (principal_label alice)  \/ is_corrupt tr (principal_state_label bob bob_si));
+
+            // Proof strategy: We want to work without the corruption case
+            // so we introduce this implication.
+            let alice_and_bob_not_corrupt = (~(is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_state_label bob bob_si))) in
+            let event_initiate2 = event_triggered tr alice (Initiate2 alice bob gx gy res.k) in
+            introduce alice_and_bob_not_corrupt ==> event_initiate2
+            with _. (
+              // We can now assert that there exists a x such that the event Initiate2 has been triggered
+              // without the corruption case.
+              assert(exists x. gx == dh_pk x /\ event_triggered tr alice (Initiate2 alice bob gx gy (dh x gy)));
+              // We now introduce x to concretely reason about it.
+              eliminate exists x. gx == dh_pk x /\ event_triggered tr alice (Initiate2 alice bob gx gy (dh x gy))
+              returns event_initiate2
+              with _. (
+                // We use commutativity of DH to reconcile the (dh x gy) in our hypothesis,
+                // and the (dh y gx) in event_initiate2
+                dh_shared_secret_lemma x y
+              )
+            );
+
+            assert(is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_state_label bob bob_si) \/ 
+              (exists si. get_label res.k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob bob_si)));
+            assert(get_usage res.k == AeadKey "DH.aead_key");
+            assert(is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_state_label bob bob_si) \/
+              (is_dh_shared_key tr alice bob res.k /\ event_triggered tr alice (Initiate2 alice bob gx gy res.k)));
+            ()
+          )
+          | None -> ()
+        )
+        | (None, tr) -> ()
+      )
+      | (None, tr) -> ()
+    )
+  | (_, tr) -> ()
+#pop-options
diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst
new file mode 100644
index 0000000..95f1c60
--- /dev/null
+++ b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst
@@ -0,0 +1,149 @@
+module DY.Example.DH.Protocol.Stateful
+
+open Comparse
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Total
+
+(*** Definition of state ***)
+
+[@@ with_bytes bytes]
+type dh_session =
+  | InitiatorSentMsg1: b:principal -> x:bytes -> dh_session
+  | ResponderSentMsg2: a:principal -> gx:bytes -> gy:bytes -> y:bytes -> dh_session
+  | InitiatorSendMsg3: b:principal -> gx:bytes -> gy:bytes -> k:bytes -> dh_session
+  | ResponderReceivedMsg3: a:principal -> gx:bytes -> gy:bytes -> k:bytes -> dh_session
+
+%splice [ps_dh_session] (gen_parser (`dh_session))
+%splice [ps_dh_session_is_well_formed] (gen_is_well_formed_lemma (`dh_session))
+
+instance dh_session_parseable_serializeable: parseable_serializeable bytes dh_session
+ = mk_parseable_serializeable ps_dh_session
+
+(*** Definition of events ***)
+[@@ with_bytes bytes]
+type dh_event =
+  | Initiate1: a:principal -> b:principal -> x:bytes -> dh_event
+  | Respond1: a:principal -> b:principal -> gx:bytes -> gy:bytes -> y:bytes -> dh_event
+  | Initiate2: a:principal -> b:principal -> gx:bytes -> gy:bytes -> k:bytes -> dh_event
+  | Respond2: a:principal -> b:principal -> gx:bytes -> gy:bytes -> k:bytes -> dh_event
+
+%splice [ps_dh_event] (gen_parser (`dh_event))
+%splice [ps_dh_event_is_well_formed] (gen_is_well_formed_lemma (`dh_event))
+
+instance dh_event_instance: event dh_event = {
+  tag = "DH.Event";
+  format = mk_parseable_serializeable ps_dh_event;
+}
+
+(*** Setup for the stateful code ***)
+
+instance local_state_dh_session: local_state dh_session = {
+  tag = "DH.Session";
+  format = mk_parseable_serializeable ps_dh_session;
+}
+
+type dh_global_sess_ids = {
+  pki: state_id;
+  private_keys: state_id;
+}
+
+(*** Stateful code ***)
+
+// Alice prepares message 1
+//
+// This method is separated from the send_msg1 method
+// to give the attacker more flexibility. With this
+// separation an attacker can set a state without sending
+// a message over the network.
+val prepare_msg1: principal -> principal -> traceful state_id
+let prepare_msg1 alice bob =
+  let* alice_si = new_session_id alice in
+  let* x = mk_rand (DhKey "DH.dh_key") (principal_state_label alice alice_si) 32 in
+  trigger_event alice (Initiate1 alice bob x);*
+  set_state alice alice_si (InitiatorSentMsg1 bob x <: dh_session);*
+  return alice_si
+
+// Alice sends message 1
+val send_msg1: principal -> state_id -> traceful (option nat)
+let send_msg1 alice alice_si =
+  let*? session_state: dh_session = get_state alice alice_si in
+  match session_state with
+  | InitiatorSentMsg1 bob x -> (
+    let msg = compute_message1 alice x in
+    let* msg_id = send_msg msg in
+    return (Some msg_id)
+  )
+  | _ -> return None
+
+// Bob prepares message 2
+val prepare_msg2: principal -> principal -> nat -> traceful (option state_id)
+let prepare_msg2 alice bob msg_id =
+  let*? msg = recv_msg msg_id in
+  let*? msg1: message1 = return (decode_message1 msg) in
+  let* bob_si = new_session_id bob in
+  let* y = mk_rand (DhKey "DH.dh_key") (principal_state_label bob bob_si) 32 in
+  trigger_event bob (Respond1 alice bob msg1.gx (dh_pk y) y);*
+  set_state bob bob_si (ResponderSentMsg2 alice msg1.gx (dh_pk y) y <: dh_session);*
+  return (Some bob_si)
+
+// Bob sends message 2
+val send_msg2: dh_global_sess_ids -> principal -> state_id -> traceful (option nat)
+let send_msg2 global_sess_id bob bob_si =
+  let*? session_state: dh_session = get_state bob bob_si in
+  match session_state with
+  | ResponderSentMsg2 alice gx gy y -> (
+    let*? sk_b = get_private_key bob global_sess_id.private_keys (Sign "DH.SigningKey") in
+    let* n_sig = mk_rand SigNonce (principal_label bob) 32 in
+    let msg = compute_message2 alice bob gx gy sk_b n_sig in
+    let* msg_id = send_msg msg in
+    return (Some msg_id)
+  )
+  | _ -> return None
+
+// Alice prepares message 3
+//
+// This function has to verify the signature from message 2
+val prepare_msg3: dh_global_sess_ids -> principal -> state_id -> principal -> nat -> traceful (option unit)
+let prepare_msg3 global_sess_id alice alice_si bob msg_id =
+  let*? session_state: dh_session = get_state alice alice_si in
+  match session_state with
+  | InitiatorSentMsg1 bob x -> (
+    let*? pk_b = get_public_key alice global_sess_id.pki (Verify "DH.SigningKey") bob in
+    let*? msg = recv_msg msg_id in
+    let*? res:verify_msg2_result = return (decode_and_verify_message2 msg alice x pk_b) in
+    trigger_event alice (Initiate2 alice bob res.gx res.gy res.k);*
+    set_state alice alice_si (InitiatorSendMsg3 bob res.gx res.gy res.k <: dh_session);*
+    return (Some ())
+  )
+  | _ -> return None
+
+// Alice send message 3
+val send_msg3: dh_global_sess_ids -> principal -> principal -> state_id -> traceful (option nat)
+let send_msg3 global_sess_id alice bob alice_si =
+  let*? session_state: dh_session = get_state alice alice_si in
+  match session_state with
+  | InitiatorSendMsg3 bob gx gy x -> (
+    let*? sk_a = get_private_key alice global_sess_id.private_keys (Sign "DH.SigningKey") in
+    let* n_sig = mk_rand SigNonce (principal_label alice) 32 in
+    let msg = compute_message3 alice bob gx gy sk_a n_sig in
+    let* msg_id = send_msg msg in
+    return (Some msg_id)
+  )
+  | _ -> return None
+
+// Bob verifies message 3
+val verify_msg3: dh_global_sess_ids -> principal -> principal -> nat -> state_id -> traceful (option unit)
+let verify_msg3 global_sess_id alice bob msg_id bob_si =
+  let*? session_state: dh_session = get_state bob bob_si in
+  match session_state with
+  | ResponderSentMsg2 alice gx gy y -> (
+    let*? pk_a = get_public_key bob global_sess_id.pki (Verify "DH.SigningKey") alice in
+    let*? msg = recv_msg msg_id in
+    let*? res:verify_msg3_result = return (decode_and_verify_message3 msg bob gx gy y pk_a) in
+    trigger_event bob (Respond2 alice bob gx gy res.k);*
+    set_state bob bob_si (ResponderReceivedMsg3 alice gx gy res.k <: dh_session);*
+    return (Some ())
+  )
+  | _ -> return None
+    
\ No newline at end of file
diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst b/examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst
new file mode 100644
index 0000000..9427fb1
--- /dev/null
+++ b/examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst
@@ -0,0 +1,279 @@
+module DY.Example.DH.Protocol.Total.Proof
+
+open Comparse
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Total
+open DY.Example.DH.Protocol.Stateful
+
+#set-options "--fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'"
+
+(*** Cryptographic invariants ***)
+
+val dh_crypto_usages: crypto_usages
+instance dh_crypto_usages = {
+  default_crypto_usages with
+
+  dh_known_peer_usage = (fun s1 s2 ->
+    match s1, s2 with
+    | "DH.dh_key", _ -> AeadKey "DH.aead_key"
+    | _, "DH.dh_key" -> AeadKey "DH.aead_key"
+    | _, _ -> NoUsage
+  );
+  dh_unknown_peer_usage = (fun s1 -> 
+    match s1 with
+    | "DH.dh_key" -> AeadKey "DH.aead_key"
+    | _ -> NoUsage);
+  dh_known_peer_usage_commutes = (fun s1 s2 -> ());
+  dh_unknown_peer_usage_implies = (fun s1 s2 -> ());
+}
+
+#push-options "--ifuel 2 --fuel 0"
+val dh_crypto_preds: crypto_predicates dh_crypto_usages
+let dh_crypto_preds = {
+  default_crypto_predicates dh_crypto_usages with
+
+  sign_pred = (fun tr vk sig_msg ->
+    get_signkey_usage vk == SigKey "DH.SigningKey" /\
+    (exists prin. get_signkey_label vk = principal_label prin /\ (
+      match parse sig_message sig_msg with
+      | Some (SigMsg2 sig_msg2) -> (
+        exists y. sig_msg2.gy == (dh_pk y) /\ event_triggered tr prin (Respond1 sig_msg2.alice prin sig_msg2.gx sig_msg2.gy y)
+      )
+      | Some (SigMsg3 sig_msg3) -> (
+        exists x. sig_msg3.gx == (dh_pk x) /\ event_triggered tr prin (Initiate2 prin sig_msg3.bob sig_msg3.gx sig_msg3.gy (dh x sig_msg3.gy))
+      )
+      | None -> False
+    ))
+  );
+  sign_pred_later = (fun tr1 tr2 vk msg -> ())
+}
+#pop-options
+
+instance dh_crypto_invs: crypto_invariants = {
+  usages = dh_crypto_usages;
+  preds = dh_crypto_preds;
+}
+
+(*** Proofs ***)
+
+val compute_message1_proof:
+  tr:trace ->
+  alice:principal -> bob:principal -> x:bytes ->
+  Lemma
+    (requires
+      event_triggered tr alice (Initiate1 alice bob x) /\
+      bytes_invariant tr x /\
+      DhKey? (get_usage x)
+    )
+    (ensures 
+      is_publishable tr (compute_message1 alice x)
+    )
+let compute_message1_proof tr alice bob x =
+  let gx = dh_pk x in
+  assert(is_publishable tr gx);
+  let msg = Msg1 {alice; gx} in
+
+  // This lemma
+  // - requires that msg.gx is is publishable
+  // - ensures that `serialize _ msg` is publishable
+  serialize_wf_lemma message (is_publishable tr) msg;
+
+  // The following code is not needed for the proof.
+  // It just shows what we need to show to prove the lemma.
+  let msgb = compute_message1 alice x in 
+  assert(bytes_invariant tr msgb);
+  assert(get_label msgb `can_flow tr` public);
+  assert(is_publishable tr msgb);
+  ()
+
+val decode_message1_proof:
+  tr:trace ->
+  msg1_bytes:bytes ->
+  Lemma
+  (requires is_publishable tr msg1_bytes)
+  (ensures (
+    match decode_message1 msg1_bytes with
+    | Some msg1 -> (
+      is_publishable tr msg1.gx
+    )
+    | None -> True
+  ))
+let decode_message1_proof tr msg1_bytes =
+  match decode_message1 msg1_bytes with
+    | Some msg1 -> (
+      // This lemma
+      // - requires that msg_bytes is publishable
+      // - ensures that `msg1.gx` is publishable
+      //   (`msg1` being the result of parsing `msg_bytes` to the type `message1`)
+      parse_wf_lemma message (is_publishable tr) msg1_bytes;
+      
+      // The following code is not needed for the proof.
+      // It just shows what we need to show to prove the lemma.
+      assert(bytes_invariant tr msg1.gx);
+      assert(get_label msg1.gx `can_flow tr` public);
+      ()
+    )
+    | None -> ()
+
+val compute_message2_proof:
+  tr:trace -> 
+  alice:principal -> bob:principal ->
+  gx:bytes -> y:bytes ->
+  sk_b:bytes -> n_sig:bytes ->
+  Lemma
+  (requires
+    event_triggered tr bob (Respond1 alice bob gx (dh_pk y) y) /\
+    is_publishable tr gx /\
+    bytes_invariant tr y /\
+    is_signature_key "DH.SigningKey" (principal_label bob) tr sk_b /\
+    is_secret (principal_label bob) tr n_sig /\
+    SigNonce? (get_usage n_sig)
+  )
+  (ensures
+    is_publishable tr (compute_message2 alice bob gx (dh_pk y) sk_b n_sig)
+  )
+let compute_message2_proof tr alice bob gx y sk_b n_sig =
+  // Proof that the SigMsg2 is publishable
+  // From the precondition we know that
+  // msg1.gx and gy are publishable.
+  let gy = dh_pk y in
+  let sig_msg = SigMsg2 {alice; gx; gy} in
+  serialize_wf_lemma sig_message (is_publishable tr) sig_msg;
+  let sig_msg_bytes = serialize sig_message sig_msg in
+
+  // This assert is not needed for the proof
+  // but shows that the serialized SigMsg2 is publishable.
+  assert(is_publishable tr sig_msg_bytes);
+
+  let sg = sign sk_b n_sig sig_msg_bytes in
+
+  // This assert is not needed for the proof
+  // but shows that the signature is also publishable.
+  assert(is_publishable tr sg);
+  
+  // Since all parts of the Msg2 are publishable, we
+  // can show that the serialized Msg2 is also publishable.
+  let msg = Msg2 {bob; gy; sg} in
+  serialize_wf_lemma message (is_publishable tr) msg;
+
+  // This proves the post-condition
+  assert(is_publishable tr (compute_message2 alice bob gx gy sk_b n_sig));
+  ()
+
+#push-options "--ifuel 1 --z3rlimit 10"
+val decode_and_verify_message2_proof:
+  tr:trace ->
+  msg2_bytes:bytes ->
+  alice:principal -> alice_si:state_id -> bob:principal ->
+  x:bytes -> pk_b:bytes ->
+  Lemma
+  (requires
+    is_publishable tr msg2_bytes /\
+    is_secret (principal_state_label alice alice_si) tr x /\
+    is_verification_key "DH.SigningKey" (principal_label bob) tr pk_b
+  )
+  (ensures (
+    match decode_and_verify_message2 msg2_bytes alice x pk_b with
+    | Some res -> (
+      let sig_msg = SigMsg2 {alice; gx=(dh_pk x); gy=res.gy} in
+      is_publishable tr res.gy /\
+      (is_corrupt tr (principal_state_label alice alice_si) \/ is_corrupt tr (principal_label bob) \/
+      (exists y. event_triggered tr bob (Respond1 alice bob (dh_pk x) res.gy y)))
+    )
+    | None -> True
+  ))
+let decode_and_verify_message2_proof tr msg2_bytes alice alice_si bob x pk_b =
+  match decode_and_verify_message2 msg2_bytes alice x pk_b with
+    | Some res -> (
+      parse_wf_lemma message (is_publishable tr) msg2_bytes;
+      let gx = dh_pk x in
+      let gy = res.gy in
+      serialize_wf_lemma sig_message (bytes_invariant tr) (SigMsg2 {alice; gx; gy});
+
+      // The following code is not needed for the proof.
+      // It just shows what we need to show to prove the lemma.
+      assert(is_publishable tr res.gy);
+      
+      assert(is_corrupt tr (principal_label alice) \/
+        is_corrupt tr (principal_label bob) \/
+        (exists y. res.gy == dh_pk y /\ event_triggered tr bob (Respond1 alice bob gx gy y))
+      );
+      ()
+    )
+    | None -> ()
+#pop-options
+
+val compute_message3_proof:
+  tr:trace ->
+  alice:principal -> bob:principal ->
+  gx:bytes -> gy:bytes -> x:bytes ->
+  sk_a:bytes -> n_sig:bytes ->
+  Lemma
+  (requires
+    event_triggered tr alice (Initiate2 alice bob (dh_pk x) gy (dh x gy)) /\
+    is_publishable tr gx /\ is_publishable tr gy /\
+    gx = dh_pk x /\
+    is_signature_key "DH.SigningKey" (principal_label alice) tr sk_a /\
+    is_secret (principal_label alice) tr n_sig /\
+    SigNonce? (get_usage n_sig)
+  )
+  (ensures
+    is_publishable tr (compute_message3 alice bob (dh_pk x) gy sk_a n_sig)
+  )
+let compute_message3_proof tr alice bob gx gy x sk_a n_sig =
+  let sig_msg = SigMsg3 {bob; gx; gy} in
+  serialize_wf_lemma sig_message (is_publishable tr) sig_msg;
+  
+  // The following code is not needed for the proof.
+  // It just shows what we need to show to prove the lemma.
+  assert(is_publishable tr (serialize sig_message sig_msg));
+  let sg = sign sk_a n_sig (serialize sig_message sig_msg) in 
+
+  // The following code is not needed for the proof.
+  // It just shows what we need to show to prove the lemma. 
+  assert(get_label sg `can_flow tr` public);
+  assert(bytes_invariant tr sg);
+  assert(is_publishable tr sg);
+
+  let msg = Msg3 {sg} in
+  serialize_wf_lemma message (is_publishable tr) msg;
+
+  // The following code is not needed for the proof.
+  // It just shows what we need to show to prove the lemma.
+  assert(is_publishable tr (serialize message msg));
+  ()
+
+#push-options "--ifuel 1 --z3rlimit 10"
+val decode_and_verify_message3_proof:
+  tr:trace ->
+  msg3_bytes:bytes ->
+  alice:principal -> bob:principal -> bob_si:state_id ->
+  gx:bytes -> y:bytes -> pk_a:bytes ->
+  Lemma
+  (requires
+    is_publishable tr msg3_bytes /\
+    is_publishable tr gx /\
+    is_secret (principal_state_label bob bob_si) tr y /\
+    is_verification_key "DH.SigningKey" (principal_label alice) tr pk_a
+  )
+  (ensures (
+    let gy = dh_pk y in
+    match decode_and_verify_message3 msg3_bytes bob gx gy y pk_a with
+    | Some res -> (
+      let sig_msg = SigMsg3 {bob; gx; gy} in
+      (is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_state_label bob bob_si) \/
+      (exists x. gx == dh_pk x /\ event_triggered tr alice (Initiate2 alice bob gx gy (dh x gy))))
+    )
+    | None -> True
+  ))
+let decode_and_verify_message3_proof tr msg3_bytes alice bob bob_si gx y pk_a =
+  let gy = dh_pk y in
+  match decode_and_verify_message3 msg3_bytes bob gx gy y pk_a with
+    | Some res -> (
+      parse_wf_lemma message (is_publishable tr) msg3_bytes;
+      serialize_wf_lemma sig_message (is_publishable tr) (SigMsg3 {bob; gx; gy});
+      ()
+    )
+    | None -> ()
+#pop-options
diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Total.fst b/examples/iso_dh/DY.Example.DH.Protocol.Total.fst
new file mode 100644
index 0000000..b5e92f3
--- /dev/null
+++ b/examples/iso_dh/DY.Example.DH.Protocol.Total.fst
@@ -0,0 +1,170 @@
+module DY.Example.DH.Protocol.Total
+
+open Comparse
+open DY.Core
+open DY.Lib
+
+(*
+ *** ISO-DH Protocol ***
+
+ Diffie-Hellman key exchange protocol with digital signatures based on
+ ISO/IEC 9798-3:2019(E): IT Security techniques — Entity authentication — Part
+ 3: Mechanisms using digital signature techniques. Tech. rep. (Jan 2019)
+
+ A -> B: {A, gx}                            msg1
+ B -> A: {B, gy, sign({A; gx; gy}, privB)}  msg2
+ A -> B: {sign({B; gx; gy}, privA)}         msg3
+
+*)
+
+(*** Definition of messages ***)
+// Annotation is needed for comparse to generate serialization methods
+[@@ with_bytes bytes]
+type message1 = {
+  alice:principal;
+  gx:bytes;
+}
+
+%splice [ps_message1] (gen_parser (`message1))
+%splice [ps_message1_is_well_formed] (gen_is_well_formed_lemma (`message1))
+
+[@@ with_bytes bytes]
+type message2 = {
+  bob:principal;
+  gy:bytes;
+  sg:bytes;
+}
+
+%splice [ps_message2] (gen_parser (`message2))
+%splice [ps_message2_is_well_formed] (gen_is_well_formed_lemma (`message2))
+
+[@@ with_bytes bytes]
+type message3 = {
+  sg:bytes;
+}
+
+%splice [ps_message3] (gen_parser (`message3))
+%splice [ps_message3_is_well_formed] (gen_is_well_formed_lemma (`message3))
+
+
+[@@ with_bytes bytes]
+type message =
+  | Msg1: msg:message1 -> message
+  | Msg2: msg:message2 -> message
+  | Msg3: msg:message3 -> message
+
+%splice [ps_message] (gen_parser (`message))
+%splice [ps_message_is_well_formed] (gen_is_well_formed_lemma (`message))
+
+instance parseable_serializeable_message: parseable_serializeable bytes message = mk_parseable_serializeable ps_message
+
+// Definition of signature terms
+[@@ with_bytes bytes]
+type sig_message2 = {
+  alice:principal;
+  gx:bytes;
+  gy:bytes;
+}
+
+%splice [ps_sig_message2] (gen_parser (`sig_message2))
+%splice [ps_sig_message2_is_well_formed] (gen_is_well_formed_lemma (`sig_message2))
+
+[@@ with_bytes bytes]
+type sig_message3 = {
+  bob:principal;
+  gx:bytes;
+  gy:bytes;
+}
+
+%splice [ps_sig_message3] (gen_parser (`sig_message3))
+%splice [ps_sig_message3_is_well_formed] (gen_is_well_formed_lemma (`sig_message3))
+
+[@@ with_bytes bytes]
+type sig_message =
+  | SigMsg2: msg:sig_message2 -> sig_message
+  | SigMsg3: msg:sig_message3 -> sig_message
+
+%splice [ps_sig_message] (gen_parser (`sig_message))
+%splice [ps_sig_message_is_well_formed] (gen_is_well_formed_lemma (`sig_message))
+
+instance parseable_serializeable_sig_message: parseable_serializeable bytes sig_message = mk_parseable_serializeable ps_sig_message
+
+
+(*** Message Processing ***)
+
+// Alice generates message 1
+val compute_message1: principal -> bytes -> bytes
+let compute_message1 alice x =
+  let gx = dh_pk x in
+  let msg = Msg1 {alice; gx} in
+  serialize message msg
+
+// Bob parses message 1
+val decode_message1: bytes -> option message1
+let decode_message1 msg1_bytes =
+  let? msg1 = parse message msg1_bytes in
+  // These lines are the...
+  guard (Msg1? msg1);?
+  Some (Msg1?.msg msg1)
+  // ...short version of the following match:
+  (*    
+  match msg1 with
+  | Msg1 msg -> Some msg
+  | _ -> None
+  *)
+
+// Bob generates message 2
+val compute_message2: principal -> principal -> bytes -> bytes -> bytes -> bytes -> bytes
+let compute_message2 alice bob gx gy sk_b n_sig =
+  let sig_msg = SigMsg2 {alice; gx; gy} in
+  let sg = sign sk_b n_sig (serialize sig_message sig_msg) in
+  let msg = Msg2 {bob; gy; sg} in
+  serialize message msg
+
+// Alice parses message 2
+type verify_msg2_result = {gy:bytes; gx:bytes; k:bytes}
+val decode_and_verify_message2: bytes -> principal -> bytes -> bytes -> option verify_msg2_result
+let decode_and_verify_message2 msg2_bytes alice x pk_b =
+  let? msg2_parsed = parse message msg2_bytes in
+  guard (Msg2? msg2_parsed);?
+  let msg2 = Msg2?.msg msg2_parsed in
+  // Verify the signature contained in the message 2
+  // with the gy value from the message and the gx
+  // value from Alice's state.
+  let gx = dh_pk x in
+  let gy = msg2.gy in
+  let sig_msg = SigMsg2 {alice; gx; gy} in
+  // These lines are the...
+  guard(verify pk_b (serialize sig_message sig_msg) msg2.sg);?
+  let k = dh x gy in
+  Some {gy; gx; k}
+  // ...short version of the following if-else block:
+  (*  
+  if verify pk_b (serialize sig_message sig_msg) msg2.sg then 
+    let k = dh x gy in
+    Some {gy; gx; k}
+  else 
+    None
+  *)
+
+// Alice generates message3
+val compute_message3: principal -> principal -> bytes -> bytes -> bytes -> bytes -> bytes
+let compute_message3 alice bob gx gy sk_a n_sig =
+  let sig_msg = SigMsg3 {bob; gx; gy} in
+  let sg = sign sk_a n_sig (serialize sig_message sig_msg) in
+  let msg = Msg3 {sg} in
+  serialize message msg
+
+// Bob parses message3
+type verify_msg3_result = {k:bytes}
+val decode_and_verify_message3: bytes -> principal -> bytes -> bytes -> bytes -> bytes -> option verify_msg3_result
+let decode_and_verify_message3 msg3_bytes bob gx gy y pk_a =
+  let? msg3_parsed = parse message msg3_bytes in
+  guard (Msg3? msg3_parsed);?
+  let msg3:message3 = Msg3?.msg msg3_parsed in
+  // Verify the signature contained in message 3
+  // with the gx and gy values from Bob's state.
+  let sig_msg = SigMsg3 {bob; gx; gy} in
+  guard(verify pk_a (serialize sig_message sig_msg) msg3.sg);?
+  let k = dh y gx in
+  Some {k}
diff --git a/examples/iso_dh/DY.Example.DH.SecurityProperties.fst b/examples/iso_dh/DY.Example.DH.SecurityProperties.fst
new file mode 100644
index 0000000..eae6699
--- /dev/null
+++ b/examples/iso_dh/DY.Example.DH.SecurityProperties.fst
@@ -0,0 +1,153 @@
+module DY.Example.DH.SecurityProperties
+
+open Comparse
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Total.Proof
+open DY.Example.DH.Protocol.Stateful
+open DY.Example.DH.Protocol.Stateful.Proof
+
+#set-options "--fuel 0 --ifuel 0 --z3rlimit 25  --z3cliopt 'smt.qi.eager_threshold=100'"
+
+
+(*** Authentication Properties ***)
+
+val initiator_authentication:
+  tr:trace -> i:nat ->
+  alice:principal -> bob:principal ->
+  gx:bytes -> gy:bytes -> k:bytes ->
+  Lemma
+  (requires 
+    trace_invariant tr /\
+    event_triggered_at tr i alice (Initiate2 alice bob gx gy k)
+  )
+  (ensures 
+    (exists alice_si. is_corrupt tr (principal_state_label alice alice_si)) \/ 
+    is_corrupt tr (principal_label bob) \/
+    (exists y. event_triggered (prefix tr i) bob (Respond1 alice bob gx gy y) /\
+    k == dh y gx)
+  )
+let initiator_authentication tr i alice bob gx gy k = ()
+
+val responder_authentication: 
+  tr:trace -> i:nat ->
+  alice:principal -> bob:principal ->
+  gx:bytes -> gy:bytes -> k:bytes ->
+  Lemma
+  (requires 
+    trace_invariant tr /\
+    event_triggered_at tr i bob (Respond2 alice bob gx gy k)
+  )
+  (ensures 
+    is_corrupt tr (principal_label alice) \/ 
+    (exists bob_si. is_corrupt tr (principal_state_label bob bob_si)) \/
+    event_triggered (prefix tr i) alice (Initiate2 alice bob gx gy k)
+  )
+let responder_authentication tr i alice bob gx gy k = ()
+
+(*** Forward Secrecy Properties ***)
+
+val initiator_forward_secrecy: 
+  tr:trace -> alice:principal -> alice_si:state_id -> bob:principal -> gx:bytes -> gy:bytes -> k:bytes ->
+  Lemma
+  (requires
+    trace_invariant tr /\
+    state_was_set tr alice alice_si (InitiatorSendMsg3 bob gx gy k) /\
+    attacker_knows tr k
+  )
+  (ensures
+    is_corrupt tr (principal_label bob) \/ is_corrupt tr (principal_state_label alice alice_si)
+  )
+let initiator_forward_secrecy tr alice alice_si bob gx gy k =
+  attacker_only_knows_publishable_values tr k;
+
+  // We derive the following fact from InitiatorSendMsg3 state invariant
+  // and Respond1 event invariant
+  // (this assert is not needed and only there for pedagogical purposes)
+  assert(
+    (exists x. gx == dh_pk x /\ k == dh x gy /\ is_secret (principal_state_label alice alice_si) tr x) /\
+    (
+      is_corrupt tr (principal_label bob) \/
+      is_corrupt tr (principal_state_label alice alice_si) \/
+      (exists y.
+        (exists bob_si. is_secret (principal_state_label bob bob_si) tr y) /\
+        gy = dh_pk y
+      )
+    )
+  );
+
+  // We can deduce from it the label of `k`, up to some corruption
+  // (this assert is not needed and only there for pedagogical purposes)
+  assert(
+    is_corrupt tr (principal_label bob) \/
+    is_corrupt tr (principal_state_label alice alice_si) \/
+    (exists bob_si. get_label k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
+  );
+
+  // We deduce from the following this assertion,
+  // that will trigger transitivity of `can_flow tr` from `join ...` to `get_label k` to `public`
+  assert(
+    is_corrupt tr (principal_label bob) \/
+    is_corrupt tr (principal_state_label alice alice_si) \/
+    (exists bob_si. join (principal_state_label alice alice_si) (principal_state_label bob bob_si) `can_flow tr` public)
+  );
+
+  // This assert allows to deduce corruption of principal bob from corruption state bob_si of principal bob
+  assert(forall bob_si. principal_label bob `can_flow tr` principal_state_label bob bob_si);
+
+  ()
+
+val responder_forward_secrecy: 
+  tr:trace -> alice:principal -> bob:principal -> bob_si:state_id -> gx:bytes -> gy:bytes -> k:bytes ->
+  Lemma
+  (requires
+    trace_invariant tr /\
+    state_was_set tr bob bob_si (ResponderReceivedMsg3 alice gx gy k) /\
+    attacker_knows tr k
+  )
+  (ensures
+    is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_state_label bob bob_si)
+  )
+let responder_forward_secrecy tr alice bob bob_si gx gy k = 
+  attacker_only_knows_publishable_values tr k;
+
+  // We derive the following fact from ResponderReceivedMsg3 state invariant
+  // and Initiate2 event invariant
+  // (this assert is not needed and only there for pedagogical purposes)
+  assert(
+    (exists y. gy == dh_pk y /\ k == dh y gx /\ is_secret (principal_state_label bob bob_si) tr y) /\
+    (
+      is_corrupt tr (principal_label alice) \/
+      is_corrupt tr (principal_state_label bob bob_si) \/
+      (exists x.
+        (exists alice_si. is_secret (principal_state_label alice alice_si) tr x) /\
+        k == dh x gy
+      )
+    )
+  );
+
+  // We can deduce from it the label of `k`, up to some corruption
+  // (this assert is not needed and only there for pedagogical purposes)
+  assert(
+    is_corrupt tr (principal_label alice) \/
+    is_corrupt tr (principal_state_label bob bob_si) \/
+    (exists alice_si. get_label k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
+  );
+
+  // We deduce from the following this assertion,
+  // that will trigger transitivity of `can_flow tr` from `join ...` to `get_label k` to `public`
+  assert(
+    is_corrupt tr (principal_label alice) \/
+    is_corrupt tr (principal_state_label bob bob_si) \/
+    (exists alice_si. join (principal_state_label alice alice_si) (principal_state_label bob bob_si) `can_flow tr` public)
+  );
+
+  // This assert is needed for the proof
+  assert(exists alice_si. join (principal_state_label alice alice_si) (principal_state_label bob bob_si)
+    `can_flow tr` public \/ 
+    is_corrupt tr (principal_label alice));
+
+  // This assert allows to deduce corruption of principal alice from corruption state alice_si of principal alice
+  assert(forall alice_si. principal_label alice `can_flow tr` principal_state_label alice alice_si);
+
+  ()
diff --git a/examples/iso_dh/Makefile b/examples/iso_dh/Makefile
new file mode 100644
index 0000000..542d594
--- /dev/null
+++ b/examples/iso_dh/Makefile
@@ -0,0 +1,6 @@
+DY_HOME ?= ../..
+include $(DY_HOME)/Makefile
+
+test:
+	cd $(DY_HOME)/obj; OCAMLPATH=$(FSTAR_HOME)/lib ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib DY_Example_DH_Debug.native
+	$(DY_HOME)/obj/DY_Example_DH_Debug.native
diff --git a/examples/iso_dh/README.md b/examples/iso_dh/README.md
new file mode 100644
index 0000000..bf95c46
--- /dev/null
+++ b/examples/iso_dh/README.md
@@ -0,0 +1,54 @@
+# Formal Security Analysis of the ISO-DH Protocol
+
+This folder contains a formal security analysis
+of the Diffie-Hellman key exchange protocol with 
+digital signatures based on the [ISO/IEC 9798-3:2019(E)](https://www.iso.org/standard/67115.html) 
+standard. In this analysis, we prove the following 
+properties of the ISO-DH protocol:
+
+1. Mutual authentication
+2. Forward secrecy of the key ``k`` 
+  (as long as the private DH keys are secret, 
+  the key ``k`` does not leak)
+
+**Protocol Flow**
+
+```
+A -> B: {A, gx}                            msg1
+B -> A: {B, gy, sign({A; gx; gy}, privB)}  msg2
+A -> B: {sign({B; gx; gy}, privA)}         msg3
+```
+
+The model of the protocol is split into two
+parts. The first part is in the ``DY.Example.DH.Protocol.Total``
+module which contains all the code that does
+not depend on the trace, e.g., message definitions,
+cryptographic functions, and message encoding.
+The second part is in the ``DY.Example.DH.Protocol.Stateful`` 
+module, containing the logic that depends on the
+trace, e.g., state definitions, state encoding, and sending messages.
+
+Since the model is split into two parts, the proof is also
+split into the two modules ``DY.Example.DH.Protocol.Total.Proof``
+and ``DY.Example.DH.Protocol.Stateful.Proof``. The first
+module contains helper lemmas about the total functions 
+used in the stateful proof to prove that every
+stateful function fulfills the trace invariants.
+
+The module ``DY.Example.DH.SecurityProperties`` formalizes the
+above-mentioned security properties and proves them with the
+protocol invariants.
+
+To see whether the protocol has been modeled correctly the module
+``DY.Example.DH.Debug`` provides an implementation of an honest
+protocol run. This module can be extracted to OCaml code to
+print an example trace to the console.
+The module ``DY.Example.DH.Debug.Proof`` proves that the
+honest protocol run fulfills the protocol invariants.
+This proof serves as a sanity check for the protocol invariants.
+
+## Check and Run the Model
+To verify the F* code you can call ``make`` from either this 
+directory or the repository's root directory.
+To run the ``DY.Example.DH.Debug`` module you have to
+execute ``make test`` from this directory.
diff --git a/src/core/DY.Core.Label.Derived.fst b/src/core/DY.Core.Label.Derived.fst
index ef91130..b9f6e3e 100644
--- a/src/core/DY.Core.Label.Derived.fst
+++ b/src/core/DY.Core.Label.Derived.fst
@@ -88,3 +88,16 @@ val right_flows_to_meet:
   [SMTPat (l2 `can_flow tr` (l1 `meet` l2))]
 let right_flows_to_meet tr l1 l2 =
   meet_eq tr (meet l1 l2) l1 l2
+
+val can_flow_propagates_is_corrupt:
+  tr:trace -> l1:label -> l2:label ->
+  Lemma
+  (requires
+    is_corrupt tr l2 /\
+    l1 `can_flow tr` l2
+  )
+  (ensures is_corrupt tr l1)
+  [SMTPat (is_corrupt tr l2); SMTPat (l1 `can_flow tr` l2)]
+let can_flow_propagates_is_corrupt tr l1 l2 =
+  flow_to_public_eq tr l1;
+  flow_to_public_eq tr l2