diff --git a/Encoding_Time.thy b/Encoding_Time.thy
new file mode 100644
index 0000000000000000000000000000000000000000..488a1296321c485fbd11f0d534875f57a9371c62
--- /dev/null
+++ b/Encoding_Time.thy
@@ -0,0 +1,32 @@
+(*  Title:  OneWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      The encoding and decoding rules for timestamps in protocol messages.
+*)
+
+theory Encoding_Time
+imports Traces_Timed HOL.Rat "~~/src/HOL/Library/Countable"
+begin
+
+subsection\<open>Our encoding and decoding functions behave nicely:
+              Output of decoding equals input of encoding.\<close>
+
+consts encode_time :: "rat \<Rightarrow> nat"
+       decode_time :: "nat \<Rightarrow> rat"
+
+specification(encode_time)
+    encode_rat_injection [simp]: "inj encode_time" 
+  apply auto
+  done
+
+specification(decode_time)
+    encode_decode_time [simp]: "decode_time (encode_time t) = t" 
+  using encode_rat_injection inv_f_eq
+  apply metis 
+  done
+
+
+end
\ No newline at end of file
diff --git a/EntryPoint_SecureTime.thy b/EntryPoint_SecureTime.thy
new file mode 100644
index 0000000000000000000000000000000000000000..d2cddeebc7687ddc55a42aabc6aa1a9f100eddd9
--- /dev/null
+++ b/EntryPoint_SecureTime.thy
@@ -0,0 +1,18 @@
+(*  Title:  EntryPoint_SecureTime
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      Collection of theories for new secure time protocol model definitions.
+*)
+
+theory EntryPoint_SecureTime
+  imports 
+    Encoding_Time
+    Foundations_HMAC
+    "~~/src/HOL/Auth/Public"
+
+begin
+
+end
\ No newline at end of file
diff --git a/Foundations_HMAC.thy b/Foundations_HMAC.thy
new file mode 100644
index 0000000000000000000000000000000000000000..134352c654b57a418575b79b9e4061c6591af654
--- /dev/null
+++ b/Foundations_HMAC.thy
@@ -0,0 +1,73 @@
+(*  Title:  Foundations_HMAC
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      Some essential proofs about the security properties of HMAC tags.
+*)
+
+theory Foundations_HMAC
+  imports Encoding_Time "~~/src/HOL/Auth/Public"
+begin
+
+
+section\<open>Protocol-independent reasoning about initial key secrecy\<close>
+
+(*This lemma was difficult enough to at one point be an axiom. 
+    There has to be a similar lemma somewhere*)
+lemma priSK_not_initially_lost: "A \<notin> bad \<Longrightarrow> Key (priSK A) \<notin> analz (knows_t Spy [])"
+  using Key_image_eq analz_into_parts
+  apply fastforce
+  done
+
+(*The following lemmas beg the same question as the one above:
+    Why is the proof apparently not self-evident from the library theories?*)
+lemma priEK_not_initially_lost: "A \<notin> bad \<Longrightarrow> Key (priEK A) \<notin> analz (knows_t Spy [])"
+  using Key_image_eq analz_into_parts
+  apply fastforce
+  done
+
+lemma shrK_not_initially_lost: "A \<notin> bad \<Longrightarrow> Key (shrK A) \<notin> analz (knows_t Spy [])"
+  using Key_image_eq analz_into_parts
+  apply fastforce
+  done
+
+
+section\<open>(Protocol-independent) Reasoning about HMAC-based authentication properties\<close>
+
+abbreviation is_hmac_protected :: "key \<Rightarrow> msg \<Rightarrow> msg \<Rightarrow> bool"
+             ("_ HashAuthenticates _ inside _") where
+             "is_hmac_protected K P M \<equiv> (M = \<lbrace>Hash \<lbrace>Key K, P\<rbrace>, P\<rbrace>)"
+
+lemma spy_cannot_fake_hash_set: "\<lbrakk>Key (priSK A) \<notin> analz knowledge; 
+                                  Hash\<lbrace>Key (priSK A), X\<rbrace> \<notin> analz knowledge\<rbrakk>
+                             \<Longrightarrow> Hash\<lbrace>Key (priSK A), X\<rbrace> \<notin> synth (analz knowledge)"
+  apply auto
+  done
+
+lemma spy_cannot_fake_hmac_set: "\<lbrakk>Key (priSK A) \<notin> analz knowledge;
+                             Hash\<lbrace>Key (priSK A), X\<rbrace> \<notin> analz knowledge\<rbrakk>
+                             \<Longrightarrow> Hash[Key (priSK A)] X \<notin> synth (analz knowledge)"
+  apply auto
+  done
+
+lemma spy_cannot_fake_ping_trace: 
+      "\<And> m. \<lbrakk> Key (priSK A) \<notin> analz (knows Spy evs); 
+              X \<notin> analz (knows Spy evs);
+              Hash\<lbrace>Key (priSK A), m\<rbrace> \<notin> analz (knows Spy evs);
+              X = Hash[Key (priSK A)] m\<rbrakk>
+             \<Longrightarrow> X \<notin> synth (analz (knows Spy evs))"
+  apply auto
+  done
+
+theorem spy_cannot_break_hmac_protection_set: 
+      "\<lbrakk>K HashAuthenticates P inside M;
+        Key K \<notin> analz (knowledge); 
+        Hash\<lbrace>Key K, P\<rbrace> \<notin> analz (knowledge);
+        M \<notin> analz (knowledge) \<rbrakk>
+       \<Longrightarrow> M \<notin> synth (analz (knowledge))"
+  apply auto
+  done
+
+end
\ No newline at end of file
diff --git a/OneWayNTS_Guarantees.thy b/OneWayNTS_Guarantees.thy
new file mode 100644
index 0000000000000000000000000000000000000000..0716ff009de9bad3f0a64bb674863828ef28299a
--- /dev/null
+++ b/OneWayNTS_Guarantees.thy
@@ -0,0 +1,698 @@
+(*  Title:  OneWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      The security proofs on the model for the one-way variant of NTS.
+*)
+
+theory OneWayNTS_Guarantees
+  imports OneWayNTS_Protocol
+
+begin
+
+section\<open>Reasoning about First Message Type: "Commit"\<close>
+
+subsection \<open>Regularity Properties: Relevant key (priSK) is not lost\<close>
+
+lemma priSK_not_lost:
+      "tr \<in> onewayNTS \<Longrightarrow> Key (priSK Br) \<notin> analz (knows_t Spy tr)"
+  apply (erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        using priSK_not_initially_lost 
+                        apply auto[1]
+  txt\<open>Case: Fake\<close>       apply auto[1]
+                        using Fake_analz_eq 
+                        apply blast
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Init\<close>       apply auto[1]
+  txt\<open>Case: Commit\<close>     apply auto[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+subsection\<open>Crypto Properties: 
+           Asymmetric signatures cannot be broken without key\<close>
+
+abbreviation is_sign_protected :: "key \<Rightarrow> msg \<Rightarrow> msg \<Rightarrow> bool"
+             ("_ SignatureAuthenticates _ inside _") where
+             "is_sign_protected K P M \<equiv> (M = \<lbrace>(Crypt K P), P\<rbrace>)"
+
+subsection \<open>Relevant message type is protected by asymmetric signature\<close>
+
+txt\<open>A Signature (commit type) is only ever introduced 
+    when a full commit message is introduced.\<close>
+lemma if_commit_signature_then_commit:
+      "\<lbrakk> 
+                M = create_commit ck n1 t1;
+                tr \<in> onewayNTS\<rbrakk>
+               \<Longrightarrow>   (Crypt (priSK Br)\<lbrace>Hash (Nonce ck), Nonce n1, Number (encode_time t1)\<rbrace>
+                      \<in> analz (knows_t Spy tr)
+                     \<longrightarrow> M \<in> analz (knows_t Spy tr))"
+  apply (erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp[1] 
+                        apply (metis Crypt_notin_image_Key analz_image_Key image_Un)
+  txt\<open>Case: Fake\<close> 
+                        apply (metis Crypt_synth_eq Fake_analz_eq analz_t_mono_contra(1) 
+                                   knows_t_Spy_Says priSK_not_lost synth.Inj)
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply simp[1]
+  txt\<open>Case: Commit\<close>     apply simp[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+subsection\<open>Main result(s): 
+           Authenticity properties of "Commit" type messages\<close>
+
+theorem message_authentication_global_perspective_commit: 
+        "\<lbrakk>X \<in> analz (knows_t Spy tr);  
+          \<exists> ck n1 t1. 
+          X = create_commit ck n1 t1; 
+          tr \<in> onewayNTS\<rbrakk> 
+         \<Longrightarrow> \<exists> tsay. (tsay, Says Br Alice X) \<in> set tr"
+  apply(erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp
+                        using Un_assoc analz_image_Key image_Un image_iff 
+                              inf_sup_aci(7)  msg.distinct(33) sup.commute
+                        apply (smt msg.distinct(27) msg.inject(6))
+  txt\<open>Case: Fake\<close>       using priSK_not_lost if_commit_signature_then_commit
+                        apply simp[1] 
+                        apply (metis (full_types) Fake_analz_eq synth_simps(4) 
+                                      synth_simps(5))
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply simp[1]
+  txt\<open>Case: Commit\<close>     using priSK_not_lost apply auto[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+theorem message_authentication_client_perspective_commit: 
+        "\<lbrakk>(trcv, Gets Alice X) \<in> set tr;  
+          \<exists> ck n1 t1. 
+          X = create_commit ck n1 t1; 
+          tr \<in> onewayNTS\<rbrakk> 
+         \<Longrightarrow> \<exists> tsay. (tsay, Says Br Alice X) \<in> set tr"
+  apply(erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1]
+  txt\<open>Case: Fake\<close>       apply simp[1]
+                        apply blast
+  txt\<open>Case: Receive\<close>    apply simp[1]
+                        apply (metis Says_imp_knows_t_Spy analz.simps 
+                                    create_commit.simps 
+                                    message_authentication_global_perspective_commit)
+  txt\<open>Case: Init\<close>       apply simp[1]
+  txt\<open>Case: Commit\<close>     using priSK_not_lost 
+                        apply auto[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+lemma chain_key_not_lost_initially:
+      "Nonce ck \<notin> {nts1w_COMMIT, nts1w_PING, nts1w_CONFIRM} 
+       \<Longrightarrow> Nonce ck \<notin> analz (knows_t Spy [])"
+  apply auto
+  apply (metis Nonce_Key_image_eq analz_image_Key image_Un)
+  done
+
+
+section\<open>Reasoning about Second Message Type: "Confirm"\<close>
+
+lemma notes_implies_noteq:
+      "\<lbrakk>(tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr; tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> Nonce ck \<noteq> Nonce n1"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  apply auto
+  done
+
+lemma notes_implies_used:
+      "\<lbrakk>(tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr; 
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow>   Nonce ck \<in> used_t tr 
+           \<and> Nonce n1 \<in> used_t tr"
+  using Notes_imp_used_t apply blast
+  done
+
+lemma nonce_and_keynonce_cannot_collide_induct:
+      "\<lbrakk>(tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr; 
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> (tinit2, Notes Br \<lbrace>Nonce any, Nonce ck1\<rbrace>) \<notin> set tr"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  using notes_implies_used 
+  apply auto
+  done
+
+lemma keynonces_cannot_collide_induct:
+      "\<lbrakk>(tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr; 
+        Nonce n1 \<noteq> Nonce n2 \<or> tinit1 \<noteq> tinit2;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> (tinit2, Notes Br \<lbrace>Nonce ck1, Nonce n2\<rbrace>) \<notin> set tr"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  using notes_implies_used 
+  apply auto
+  done
+
+lemma nonces_cannot_collide_induct:
+      "\<lbrakk>(tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr; 
+        Nonce ck1 \<noteq> Nonce ck2 \<or> tinit1 \<noteq> tinit2;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> (tinit2, Notes Br \<lbrace>Nonce ck2, Nonce n1\<rbrace>) \<notin> set tr"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  using notes_implies_used 
+  apply auto
+  done
+
+lemma nonce_and_keynonce_cannot_collide:
+      "\<lbrakk>(tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr;
+        (tinit2, Notes Br \<lbrace>Nonce ck2, Nonce n2\<rbrace>) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow>  Nonce ck1 \<noteq> Nonce n2
+          \<and> Nonce ck2 \<noteq> Nonce n1
+          \<and> Nonce ck1 \<noteq> Nonce n1
+          \<and> Nonce ck2 \<noteq> Nonce n2"
+  using nonce_and_keynonce_cannot_collide_induct notes_implies_noteq
+  apply auto
+  done
+
+lemma keynonces_cannot_collide:
+      "\<lbrakk>(tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr;
+        (tinit2, Notes Br \<lbrace>Nonce ck2, Nonce n2\<rbrace>) \<in> set tr;
+        Nonce n1 \<noteq> Nonce n2 \<or> tinit1 \<noteq> tinit2 \<or> Nonce ck1 \<noteq> Nonce ck2;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow>  Nonce ck1 \<noteq> Nonce ck2 \<and> Nonce n1 \<noteq> Nonce n2"
+  apply (rule conjI)
+  using keynonces_cannot_collide_induct
+   apply auto[1]
+  using nonces_cannot_collide_induct
+   apply auto[1]
+  done
+
+(* The problematic (obvious to humans, apparently difficult inside the specified model) 
+   part of reasoning is this:
+   IF two events are in a trace tr
+   THEN there must be a "sub-trace" tr* SUCH THAT 
+        - one event is already in tr*
+        - tr* fulfills all requirements to inductively insert the other event *)
+lemma init_nonces_not_collide:
+      "\<lbrakk>(tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr;
+        (tinit2, Notes Br \<lbrace>Nonce ck2, Nonce n2\<rbrace>) \<in> set tr;
+        (tinit1, \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<noteq> (tinit2, \<lbrace>Nonce ck2, Nonce n2\<rbrace>);
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow>  (Nonce ck1 \<noteq> Nonce ck2
+           \<and> Nonce n1  \<noteq> Nonce n2
+           \<and> Nonce ck1 \<noteq> Nonce n2
+           \<and> Nonce ck2 \<noteq> Nonce n1
+           \<and> Nonce ck1 \<noteq> Nonce n1
+           \<and> Nonce ck2 \<noteq> Nonce n2)"
+  apply (rule conjI)
+  using keynonces_cannot_collide nonce_and_keynonce_cannot_collide notes_implies_noteq
+  apply auto[1]
+  apply blast
+  apply blast
+  using nonce_and_keynonce_cannot_collide_induct nonces_cannot_collide_induct 
+  apply blast
+  done
+
+lemma commit_implies_init_induct:
+      "\<lbrakk>(tcom, Says Br Alice (create_commit ck1 n1 tval1)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> \<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1]
+  txt\<open>Case: Fake\<close>       using  Br_honest Spy_in_bad event.inject(1) list.set_intros(2) 
+                               prod.inject set_ConsD
+                        apply metis
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Init\<close>       apply auto[1]
+  txt\<open>Case: Commit\<close>     apply simp[1]
+                        apply blast
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]   
+  txt\<open>Case: Discipline\<close> apply auto[1] 
+  done
+
+lemma commit_implies_init:
+      "\<lbrakk>(tcom, Says Br Alice (create_commit ck1 n1 tval1)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> \<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr"
+  using commit_implies_init_induct
+  apply blast
+  done
+
+(* Needed to assert that ck is also != n1 and != all the Message Type IDs *)
+lemma chain_key_not_parts_disjoint_commit:
+      "\<lbrakk>Nonce ck \<notin> analz (knows_t Spy tr);
+        (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+        Nonce ckx \<noteq> Nonce ck;
+        Nonce n1x \<noteq> Nonce ck;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> Nonce ck \<notin> 
+           analz (knows_t Spy ((t1, Says Br Alice (create_commit ckx n1x t1)) # tr))"
+  using notes_implies_noteq
+  apply auto
+  done
+
+lemma chain_key_not_parts_own_commit:
+      "\<lbrakk>Nonce ck \<notin> analz (knows_t Spy tr);
+        (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> Nonce ck \<notin> 
+           analz (knows_t Spy ((t1, Says Br Alice (create_commit ck n1 t1)) # tr))"
+  using notes_implies_noteq
+  apply auto
+  done
+
+lemma chain_key_not_parts_commit:
+      "\<lbrakk>Nonce ck \<notin> analz (knows_t Spy tr);
+        (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+        Nonce ck \<noteq> Nonce n1x;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> Nonce ck \<notin> 
+           analz (knows_t Spy ((t1, Says Br Alice (create_commit ckx n1x t1)) # tr))"
+  apply auto
+  done
+
+lemma chain_key_not_leaked_commit: 
+      "\<lbrakk> tr \<in> onewayNTS;
+        (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+        Nonce ck \<notin> analz (knows_t Spy tr)\<rbrakk>
+    \<Longrightarrow> Nonce ck \<notin> analz (knows_t Spy ( 
+                    (tsend, Says Br Alice (create_commit ck n1 tsend)) # tr))"
+  using chain_key_not_parts_own_commit 
+  apply blast
+  done
+
+lemma analz_add_commit[simp]:
+      "analz (insert (create_commit ck n1 t1) msgs)
+       = (analz {create_commit ck n1 t1}) \<union> (analz msgs)"
+  apply auto
+  done
+
+lemma chain_key_not_parts_disjoint_confirm:
+      "\<lbrakk>Nonce ck \<notin> analz (knows_t Spy tr);
+        (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+        Nonce ckx \<noteq> Nonce ck;
+        Nonce n1x \<noteq> Nonce ck;
+        tr \<in> onewayNTS\<rbrakk>
+        \<Longrightarrow> Nonce ck \<notin> 
+            analz (knows_t Spy ((ts, Says Br Alice (create_confirm ckx n1x)) # tr))"
+  apply auto
+  done
+
+lemma confirm_implies_commit_induct:
+      "\<lbrakk>(tcnfrm, Says Br Alice (create_confirm ck1 n1)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> \<exists> tcmmt tval1. (tcmmt, Says Br Alice (create_commit ck1 n1 tval1)) \<in> set tr"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1]
+  txt\<open>Case: Fake\<close>       using  Br_honest Spy_in_bad event.inject(1) list.set_intros(2) 
+                               prod.inject set_ConsD
+                        apply metis
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Init\<close>       apply auto[1]
+  txt\<open>Case: Commit\<close>     apply simp[1]
+                        apply blast
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]   
+  txt\<open>Case: Discipline\<close> apply auto[1] 
+  done
+
+lemma confirm_implies_init:
+      "\<lbrakk>(tcnfrm, Says Br Alice (create_confirm ck1 n1)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> \<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr"
+  using commit_implies_init_induct confirm_implies_commit_induct 
+  apply blast
+  done
+
+lemma nonce_and_keynonce_cannot_collide_confirm_induct:
+      "\<lbrakk>(tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr;
+        Nonce nx \<noteq> Nonce n1;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> (tcnfrm, Says Br Alice (create_confirm any ck1)) \<notin> set tr
+           \<and> (tcnfrmx, Says Br Alice (create_confirm ck1 nx)) \<notin> set tr"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1] 
+  txt\<open>Case: Fake\<close>       apply simp[1]
+                        using Br_honest 
+                        apply fastforce
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply simp[1]
+                        using Says_imp_used_t 
+                        apply blast
+  txt\<open>Case: Commit\<close>     apply auto[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    using commit_implies_init_induct init_nonces_not_collide 
+                              notes_implies_noteq
+                        apply simp  
+                        apply blast  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+lemma confirm_either_matches_existing_init_fully_or_not_at_all:
+      "\<lbrakk>\<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr \<and>
+        (tconf, Says Br Alice (create_confirm ckx nx)) \<in> set tr;
+        Nonce ckx \<noteq> Nonce ck1 \<or> Nonce nx \<noteq> Nonce n1;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow>  (Nonce ckx \<noteq> Nonce ck1 \<and> Nonce nx \<noteq> Nonce n1)"
+  apply auto (* Generates 2 subgoals *)
+    using confirm_implies_init keynonces_cannot_collide apply fastforce
+    using nonce_and_keynonce_cannot_collide_confirm_induct apply auto
+    done
+
+lemma confirm_either_matches_existing_confirm_fully_or_not_at_all:
+      "\<lbrakk>\<exists> tconf1. (tconf1, Says Br Alice (create_confirm ck1 n1)) \<in> set tr \<and>
+        (tconf2, Says Br Alice (create_confirm ck2 n2)) \<in> set tr;
+        Nonce ck2 \<noteq> Nonce ck1 \<or> Nonce n2 \<noteq> Nonce n1;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow>  (Nonce ck2 \<noteq> Nonce ck1 \<and> Nonce n2 \<noteq> Nonce n1)"
+  apply auto (* Generates 2 subgoals *)
+    apply (metis confirm_implies_init create_confirm.elims keynonces_cannot_collide msg.inject(3))
+    apply (metis confirm_implies_init create_confirm.elims keynonces_cannot_collide msg.inject(3))
+  done
+
+lemma chain_key_not_parts_disjoint_confirm_v2:
+      "\<lbrakk>Nonce ck1 \<notin> analz (knows_t Spy tr);
+        (tinit1, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr;
+        \<exists> tinit. (tinit2, Notes Br \<lbrace>Nonce ck2, Nonce n2\<rbrace>) \<in> set tr;
+        Nonce ck2 \<noteq> Nonce ck1;
+        tr \<in> onewayNTS\<rbrakk>
+        \<Longrightarrow> Nonce ck1 \<notin> 
+            analz (knows_t Spy ((ts, Says Br Alice (create_confirm ck2 n2)) # tr))"
+  using nonce_and_keynonce_cannot_collide
+  apply auto
+  done
+
+theorem chain_key_not_lost_unless_disclosed:
+      "\<lbrakk>\<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> (Nonce ck \<in> analz (knows_t Spy tr) 
+           \<longrightarrow>  (\<exists> tdsc. (tdsc, Says Br Alice (create_confirm ck n1)) \<in> set tr))"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        using not_parts_not_analz chain_key_not_lost_initially 
+                        apply auto[1] 
+  txt\<open>Case: Fake\<close>       apply simp
+                        apply (smt Fake_analz_eq synth_simps(1))
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply simp[1]
+                        using not_parts_not_analz 
+                        apply blast
+  txt\<open>Case: Commit\<close>     apply auto[1]
+                        using nonce_and_keynonce_cannot_collide_induct 
+                        apply blast
+  txt\<open>Case: Ping\<close>       apply auto[1]
+                        using Says_imp_knows_t_Spy analz.Snd 
+                        apply blast
+  txt\<open>Case: Confirm\<close>    using init_nonces_not_collide
+                              chain_key_not_parts_disjoint_confirm_v2
+                        apply simp 
+                        apply (metis commit_implies_init_induct create_commit.elims)   
+  txt\<open>Case: Discipline\<close> apply auto[1]                     
+  done
+
+theorem chain_key_not_lost_unless_disclosed_v2:
+      "\<lbrakk>(create_confirm ck n1) \<notin> knows_t Spy tr;
+        \<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> (Nonce ck \<notin> analz (knows_t Spy tr))"
+  using Says_imp_knows_t_Spy chain_key_not_lost_unless_disclosed
+  apply blast
+  done
+
+lemma confirm_implies_previous_commit:
+      "\<lbrakk>(tconfirm, Says Br Alice (create_confirm ck n1)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> \<exists> tcommit tval. ((tcommit, Says Br Alice (create_commit ck n1 tval)) \<in> set tr 
+           \<and> tconfirm \<ge> tval)"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>     
+                        apply auto[1] 
+  txt\<open>Case: Fake\<close>       apply simp 
+                        using Br_honest 
+                        apply fastforce
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply auto[1]
+  txt\<open>Case: Commit\<close>     apply auto[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]           
+  txt\<open>Case: Discipline\<close> apply auto[1]           
+  done
+
+lemma commit_is_unique:
+      "\<lbrakk>\<exists> tcommit. (tcommit, Says Br Alice (create_commit ck n1 tvalid)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> \<forall> tother tvalid2. ((tother, Says Br Alice (create_commit ck n1 tvalid2)) \<in> set tr
+                             \<longrightarrow> (tvalid = tvalid2))"
+  apply (erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1] 
+  txt\<open>Case: Fake\<close>       apply simp 
+                        using Br_honest Spy_in_bad
+                        apply (metis)
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply auto[1] 
+  txt\<open>Case: Commit\<close>     apply auto[1] 
+                        apply (metis encode_decode_time)  
+                        apply (metis encode_decode_time) 
+  txt\<open>Case: Ping\<close>       apply auto[1]
+  txt\<open>Case: Confirm\<close>    apply auto[1]    
+  txt\<open>Case: Discipline\<close> apply auto[1]                  
+  done
+
+lemma confirm_after_tvalid:
+      "\<lbrakk>\<exists> tcommit. (tcommit, Says Br Alice (create_commit ck n1 tvalid)) \<in> set tr \<and>
+        (tconfirm, Says Br Alice (create_confirm ck n1)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> tconfirm \<ge> tvalid"
+  using commit_is_unique confirm_implies_previous_commit 
+  apply blast
+  done
+
+lemma not_confirm_before_tvalid:
+      "\<lbrakk>\<exists> tcommit. (tcommit, Says Br Alice (create_commit ck n1 tvalid)) \<in> set tr;
+        maxtime tr < tvalid;
+        tr \<in> onewayNTS\<rbrakk> 
+       \<Longrightarrow> (tconfirm, Says Br Alice (create_confirm ck n1)) \<notin> set tr"
+  using confirm_after_tvalid eq_refl leD le_less_trans maxtime_aux
+  apply (metis)
+  done
+
+
+section\<open>Reasoning about third (most intricate) message type: "Ping"\<close>
+
+subsection\<open>(Protocol-independent) Reasoning:
+              HMAC-based authentication properties\<close>
+
+abbreviation is_hmac_protected_nonce :: "nat \<Rightarrow> msg \<Rightarrow> msg \<Rightarrow> bool"
+             ("_ NonceHashAuthenticates _ inside _") where
+             "is_hmac_protected_nonce N P M \<equiv> (M = \<lbrace>Hash \<lbrace>Nonce N, P\<rbrace>, P\<rbrace>)"
+
+lemma spy_cannot_fake_nonce_hash_set: "\<lbrakk>Nonce N \<notin> analz knowledge; 
+                                  Hash\<lbrace>Nonce N, X\<rbrace> \<notin> analz knowledge\<rbrakk>
+                             \<Longrightarrow> Hash\<lbrace>Nonce N, X\<rbrace> \<notin> synth (analz knowledge)"
+  apply auto
+  done
+
+lemma spy_cannot_fake_nonce_hmac_set: "\<lbrakk>Nonce N \<notin> analz knowledge;
+                             Hash\<lbrace>Nonce N, X\<rbrace> \<notin> analz knowledge\<rbrakk>
+                             \<Longrightarrow> Hash[Nonce N] X \<notin> synth (analz knowledge)"
+  apply auto
+  done
+
+lemma create_ping_is_nonce_hash_authenticated:
+      "ck NonceHashAuthenticates
+       \<lbrace>Nonce n1, Number (encode_time t1)\<rbrace>
+       inside (create_ping ck n1 t1)"
+  apply auto
+  done
+
+lemma hmac_protects_unless_key_leaked:
+      "\<lbrakk>Nonce N \<notin> analz knowledge;
+       N NonceHashAuthenticates P inside M;
+       M \<notin> analz knowledge;
+       Hash \<lbrace>Nonce N, P\<rbrace> \<notin> analz knowledge\<rbrakk>
+       \<Longrightarrow> M \<notin> synth (analz knowledge)"
+  apply auto
+  done
+
+subsection\<open>Reasoning about structure and regularity of "Ping" messages\<close>
+
+lemma ping_implies_init:
+      "\<lbrakk>\<exists> tping. (tping, Says Br Alice (create_ping ck1 n1 tping)) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> \<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr"
+ apply (erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1]
+  txt\<open>Case: Fake\<close>       using Br_honest Spy_in_bad event.inject(1) list.set_intros(2) 
+                              prod.inject set_ConsD
+                        apply metis
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Init\<close>       apply auto[1] 
+  txt\<open>Case: Commit\<close>     apply simp[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+                        apply (simp add: commit_implies_init_induct)
+  txt\<open>Case: Confirm\<close>    apply auto[1]    
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+lemma ping_tag_cannot_be_faked:
+      "\<lbrakk>Nonce ck \<notin> analz (knows_t Spy tr);
+        \<forall> t1. Hash\<lbrace>Nonce ck, \<lbrace>Nonce n1, Number (encode_time t1)\<rbrace>\<rbrace> 
+              \<notin> analz (knows_t Spy tr)
+        \<and> (create_ping ck n1 t1) \<notin> (knows_t Spy tr);
+        tr \<in> onewayNTS\<rbrakk>
+        \<Longrightarrow> \<forall> t1. Hash\<lbrace>Nonce ck, \<lbrace>Nonce n1, Number (encode_time t1)\<rbrace>\<rbrace>  
+                  \<notin> synth (analz (knows_t Spy tr))"
+  using create_commit.elims if_commit_signature_then_commit msg.distinct(19)
+  apply simp
+  using msg.distinct(37) msg.distinct(41) msg.distinct(9) msg.inject(6) priSK_not_lost 
+        synth.simps synth_simps(5)
+  apply blast
+  done
+
+txt\<open>An HMAC tag (ping type) is not introduced 
+    unless a full ping message is introduced.\<close>
+lemma if_ping_tag_then_ping:
+      "\<lbrakk>((tnotes, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr \<or>
+        Nonce ck1 \<notin> used_t tr) \<and>
+        (create_confirm ck1 n1) \<notin> (knows_t Spy tr) \<and>
+        (create_ping ck1 n1 t1) \<notin> (knows_t Spy tr);
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> Hash \<lbrace>Nonce ck1, \<lbrace>Nonce n1, Number (encode_time t1)\<rbrace>\<rbrace> 
+                 \<notin> analz (knows_t Spy tr)"
+  apply (erule rev_mp, erule onewayNTS.induct)
+(* Trouble arises for the Fake case *)
+  txt\<open>Case: Nil\<close>        using not_parts_not_analz 
+                        apply auto[1]
+  txt\<open>Case: Fake\<close>       using ping_implies_init ping_tag_cannot_be_faked 
+                              chain_key_not_lost_unless_disclosed
+                        apply auto[1]
+                        apply (metis Fake_analz_eq create_confirm.elims
+                                     chain_key_not_lost_unless_disclosed_v2 
+                                     spy_cannot_fake_nonce_hash_set synth.Inj)
+                        apply (metis Fake_analz_eq Hash_synth_analz usedI
+                                     not_parts_not_analz synth.Inj synth_simps(1))
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Init\<close>       apply auto[1] 
+  txt\<open>Case: Commit\<close>     apply auto[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]  
+  txt\<open>Case: Confirm\<close>    apply auto[1]  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+lemma Br_says_ping_correct_time:
+      "\<lbrakk>(tsays, Says Br Alice (create_ping ck1 n1 t1)) \<in> set tr; 
+        tr \<in> onewayNTS\<rbrakk>
+       \<Longrightarrow> tsays = t1"
+ apply(erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1] 
+  txt\<open>Case: Fake\<close>       apply auto[1] 
+                        using Br_honest 
+                        apply auto[1]               
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply simp[1]
+  txt\<open>Case: Commit\<close>     apply simp[1]
+  txt\<open>Case: Ping\<close>       apply auto[1]
+                        apply (metis encode_decode_time)
+  txt\<open>Case: Confirm\<close>    apply simp  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+theorem ping_cannot_be_faked: 
+        "\<lbrakk>(tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr;
+          (create_confirm ck1 n1) \<notin> knows_t Spy tr;
+          (create_ping ck1 n1 t1) \<notin> knows_t Spy tr;          
+          tr \<in> onewayNTS\<rbrakk> 
+         \<Longrightarrow> (create_ping ck1 n1 t1) \<notin> synth (analz (knows_t Spy tr))"
+  apply (simp add: chain_key_not_lost_unless_disclosed_v2 if_ping_tag_then_ping)
+  using chain_key_not_lost_unless_disclosed_v2 if_ping_tag_then_ping 
+  apply fastforce
+  done
+
+theorem message_authentication_global_perspective_ping: 
+        "\<lbrakk>  (create_ping ck1 n1 t1) \<in> (knows_t Spy tr) \<and>
+          (\<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr) \<and>
+          (create_confirm ck1 n1) \<notin> knows_t Spy tr;           
+          tr \<in> onewayNTS\<rbrakk> 
+         \<Longrightarrow> (t1, Says Br Alice(create_ping ck1 n1 t1)) \<in> set tr"
+  apply(erule rev_mp, erule onewayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1]
+  txt\<open>Case: Fake\<close>       using ping_cannot_be_faked Br_says_ping_correct_time 
+                        apply simp 
+                        apply blast                    
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Init\<close>       apply auto[1] 
+                        apply (metis HPair_def analz.Fst analz.Inj analz.Snd 
+                                     not_parts_not_analz usedI)
+  txt\<open>Case: Commit\<close>     apply simp[1]
+  txt\<open>Case: Ping\<close>       apply auto[1] 
+                        apply (metis Br_says_ping_correct_time create_commit.elims 
+                                     create_ping.elims list.set_intros(1) 
+                                     onewayNTS.Ping)
+  txt\<open>Case: Confirm\<close>    apply simp  
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+lemma gets_implies_known:
+      "\<lbrakk>\<exists> trcv.(trcv, Gets Alice X) \<in> set tr;
+        tr \<in> onewayNTS\<rbrakk>
+        \<Longrightarrow> X \<in> knows_t Spy tr"
+  apply(erule rev_mp, erule onewayNTS.induct)
+  using Says_imp_knows_t_Spy
+  apply auto
+  done
+
+lemma message_authentication_client_perspective_ping_assms: 
+        "\<lbrakk>\<exists> trcv_commit tinit.
+          (trcv_ping, Gets Alice (create_ping ck1 n1 t1)) \<in> set tr \<and>
+          (trcv_commit, Gets Alice (create_commit ck1 n1 tvalid)) \<in> set tr \<and>
+          trcv_ping < tvalid \<and>
+          maxtime tr < tvalid;
+          tr \<in> onewayNTS\<rbrakk> 
+         \<Longrightarrow>  (create_ping ck1 n1 t1) \<in> (knows_t Spy tr) \<and>
+              (\<exists> tinit. (tinit, Notes Br \<lbrace>Nonce ck1, Nonce n1\<rbrace>) \<in> set tr) \<and>
+                      (create_confirm ck1 n1) \<notin> knows_t Spy tr"
+  apply (rule conjI)
+  using gets_implies_known apply metis
+  apply (rule conjI)
+  using message_authentication_client_perspective_commit commit_implies_init 
+  apply blast
+  using message_authentication_client_perspective_commit not_confirm_before_tvalid
+  apply meson 
+  using analz.Fst analz.Inj chain_key_not_lost_unless_disclosed commit_implies_init_induct 
+        create_confirm.elims
+  apply metis
+  done
+
+theorem message_authentication_client_perspective_ping: 
+        "\<lbrakk>\<exists> trcv_commit tinit.
+          (trcv_ping, Gets Alice (create_ping ck1 n1 t1)) \<in> set tr \<and>
+          (trcv_commit, Gets Alice (create_commit ck1 n1 tvalid)) \<in> set tr \<and>
+          trcv_ping < tvalid \<and>
+          maxtime tr < tvalid;
+          tr \<in> onewayNTS\<rbrakk> 
+         \<Longrightarrow> (t1, Says Br Alice(create_ping ck1 n1 t1)) \<in> set tr"
+  using message_authentication_client_perspective_ping_assms
+        message_authentication_global_perspective_ping 
+  apply auto 
+  done
+
+subsection\<open>Timeliness Properties\<close>
+
+theorem message_authentication_client_perspective_sync: 
+        "\<lbrakk>(trcv_ping, Gets Alice (create_ping ck1 n1 t1)) \<in> set tr \<and>
+          trcv_ping < tvalid;
+          trcv_ping > t1;
+          tvalid > t1;
+          tr \<in> onewayNTS\<rbrakk> 
+         \<Longrightarrow> abs(Offset - (t1 - (clocktime Alice trcv_ping))) \<le> abs(tvalid - t1)" 
+  using clocktime_def apply auto 
+  done
+
+txt\<open>Regrettably, there are no nicer  
+    sync properties for one-way communication.\<close>
+
+end
\ No newline at end of file
diff --git a/OneWayNTS_Protocol.thy b/OneWayNTS_Protocol.thy
new file mode 100644
index 0000000000000000000000000000000000000000..ce11f85bb0c24c906fc21fd32c64eb4b9a0f7f62
--- /dev/null
+++ b/OneWayNTS_Protocol.thy
@@ -0,0 +1,176 @@
+(*  Title:   OneWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      The protocol model for the one-way variant of NTS.
+*)
+
+theory OneWayNTS_Protocol
+  imports EntryPoint_SecureTime
+
+begin
+
+
+section\<open>Setup of the environment for One-Way NTS\<close>
+
+consts
+  Offset    :: time   (* time offset between Alice and Br *)
+  Br        :: agent  (* honest broadcaster *)
+  Alice     :: agent  (* honest time client *)
+
+  DisclosureDelay ::  time (* time delay between commitment to 
+                              and disclusure of a key*)
+
+specification(DisclosureDelay)
+  DiscDel_positive [simp]:    "DisclosureDelay > 0"
+  apply (simp add: gt_ex)
+  done
+
+specification(clocktime Alice Br Offset)
+  Br_clock_perfect [simp]:    "clocktime Br t = t" 
+  Alice_clock_linear [simp]:  "clocktime Alice t = clocktime Br t - Offset"
+  Br_honest [simp]:           "Br \<notin> bad"
+  Alice_Br_different:         "Alice \<noteq> Br"
+  apply fastforce
+  done
+
+fun recent_offset :: "agent \<Rightarrow> trace_t \<Rightarrow> time"
+  where "recent_offset A [] = 0"
+  | "recent_offset A (ev # tr) = (if \<exists>X t. ev = (t, Notes A (Number (encode_time X))) 
+                                then 0 
+                                else recent_offset A tr)"
+
+fun clocktime_trace :: "agent \<Rightarrow> trace_t \<Rightarrow> time \<Rightarrow> time"
+  where "clocktime_trace A tr t = clocktime A t - recent_offset A tr"
+
+section\<open>Definition of and basic reasoning about employed message formats\<close>
+
+fun create_commit :: "key \<Rightarrow> nat \<Rightarrow> time \<Rightarrow> msg"
+  where "create_commit chain_key n1 tv
+         = \<lbrace>
+             (Crypt (priSK Br) \<lbrace>Hash (Nonce chain_key), Nonce n1, Number (encode_time tv)\<rbrace>),
+Hash (Nonce chain_key), Nonce n1, Number (encode_time tv)
+           \<rbrace>"
+
+abbreviation is_valid_commit :: "msg \<Rightarrow> bool"
+  where "is_valid_commit m \<equiv>
+         \<exists> h1 n1 t1 sign.
+           m = \<lbrace>sign, h1, n1, t1\<rbrace>
+         \<and> \<lbrace>h1, n1, t1\<rbrace> \<in> analz {sign, Key (pubSK Br)}"
+
+lemma is_valid_create_commit:
+  "is_valid_commit (create_commit ck n t)"
+  apply simp
+  done
+
+fun create_ping :: "key \<Rightarrow> nat \<Rightarrow> time \<Rightarrow> msg"
+  where "create_ping chain_key n1 t1
+         =  Hash[Nonce chain_key] \<lbrace>Nonce n1, Number (encode_time t1)\<rbrace>"
+
+abbreviation is_valid_ping :: "msg \<Rightarrow> nat \<Rightarrow> bool"
+  where "is_valid_ping m n \<equiv>
+         \<exists> h t1.
+           m = \<lbrace>h, Nonce n, t1\<rbrace>"
+
+lemma is_valid_create_ping:
+  "is_valid_ping (create_ping ck n t) n"
+  apply simp
+  done
+
+fun create_confirm :: "key \<Rightarrow> nat \<Rightarrow> msg"
+  where "create_confirm chain_key n1 
+         = \<lbrace>Nonce chain_key, Nonce n1\<rbrace>"
+
+abbreviation is_valid_confirm :: "msg \<Rightarrow> nat \<Rightarrow> bool"
+  where "is_valid_confirm m n \<equiv>
+         \<exists> ck.
+           m = \<lbrace>Nonce ck, Nonce n\<rbrace>"
+
+lemma is_valid_create_confirm:
+  "is_valid_confirm (create_confirm ck n) n"
+  apply simp
+  done
+
+section\<open>Specification of the actual protocol as inductive set of traces\<close>
+
+inductive_set
+ onewayNTS :: "(trace_t) set"
+ where
+
+  (* Global, protocol-independent Rules*)
+
+   Nil [intro] : "[] \<in> onewayNTS"
+
+ | Fake:
+  "\<lbrakk>tr \<in> onewayNTS;  
+    t \<ge>  maxtime tr; 
+    X \<in> synth (analz (knows_t Spy tr))\<rbrakk>
+  \<Longrightarrow> (t, Says Spy B X) # tr \<in> onewayNTS"
+
+ | Receive:
+  "\<lbrakk>tr \<in> onewayNTS; 
+    (tsend, Says A B X) \<in> set tr; 
+    trecv \<ge> maxtime tr \<rbrakk>
+   \<Longrightarrow> (trecv, Gets C X) # tr \<in> onewayNTS"
+
+ (* Protocol rules for one-way sync *)
+
+(* The "Init" step ensures that the Nonces are going into the "used_t" set *)
+| Init:
+   "\<lbrakk>tr \<in> onewayNTS; 
+     tinit \<ge> maxtime tr;
+     Nonce n1 \<notin> used_t tr; 
+     Nonce ck \<notin> used_t tr; 
+     Nonce ck \<noteq> Nonce n1\<rbrakk> 
+    \<Longrightarrow> (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) # tr \<in> onewayNTS" 
+
+| Commit:
+   "\<lbrakk> tr \<in> onewayNTS; 
+      tsend \<ge> maxtime tr; 
+      tvalid = tsend + DisclosureDelay;
+      (tinit, Notes Br \<lbrace>Nonce ck, Nonce n1\<rbrace>) \<in> set tr;
+      \<forall> tother tvalid2. 
+        (tother, Says Br Alice (create_commit ck n1 tvalid2)) \<notin> set tr\<rbrakk>
+    \<Longrightarrow> (tsend, Says Br Alice (create_commit ck n1 tvalid)) # tr \<in> onewayNTS"
+
+| Ping:
+  "\<lbrakk> tr \<in> onewayNTS; 
+     tvalid > tsend; 
+     tsend \<ge> maxtime tr;
+     (tcom, Says Br Alice (create_commit chain_key n1 tvalid)) \<in> set tr \<rbrakk>
+    \<Longrightarrow> (tsend, Says Br Alice (create_ping chain_key n1 tsend)) # tr \<in> onewayNTS"
+
+| Confirm:
+   "\<lbrakk> tr \<in> onewayNTS; 
+      tcnfrm \<ge> maxtime tr;
+      tcnfrm \<ge> tvalid;
+      (tcom, Says Br Alice (create_commit chain_key n1 tvalid)) \<in> set tr \<rbrakk>
+    \<Longrightarrow> (tcnfrm, Says Br Alice (create_confirm chain_key n1)) # tr \<in> onewayNTS"
+
+| Discipline:
+   "\<lbrakk> (trcv_ping, Gets Alice (create_ping ck1 n1 t1)) \<in> set tr;
+      (trcv_commit, Gets Alice (create_commit ck1 n1 tvalid)) \<in> set tr;
+      trcv_ping < tvalid;
+      tdiscp \<ge> maxtime tr;
+      tr \<in> onewayNTS\<rbrakk> 
+     \<Longrightarrow> (tdiscp, Notes Alice(Number (encode_time 
+                      (t1 - (clocktime_trace Alice tr trcv_ping))))) 
+          # tr \<in> onewayNTS"
+
+lemma maxtime_aux:
+      "\<lbrakk>(t1, Says A B X) \<in> set tr; t2 \<ge> maxtime tr\<rbrakk> \<Longrightarrow> t2 \<ge> t1"
+  using maxtime_geq_elem occursAtTime_t.simps 
+  apply blast
+  done
+
+lemma maxtime_aux2:
+      "\<lbrakk>tr \<in> onewayNTS;
+        tr = (tlatest, ev) # tr2\<rbrakk>
+       \<Longrightarrow> maxtime tr = tlatest"
+  apply(erule rev_mp, erule onewayNTS.induct)
+         apply auto
+  done
+
+end
\ No newline at end of file
diff --git a/OneWayNTS_Viability.thy b/OneWayNTS_Viability.thy
new file mode 100644
index 0000000000000000000000000000000000000000..b447815f87195141e0561316b5fd3a7ffd70edd1
--- /dev/null
+++ b/OneWayNTS_Viability.thy
@@ -0,0 +1,226 @@
+(*  Title:   OneWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      The viability and executability proofs for the model of one-way NTS.
+*)
+
+theory OneWayNTS_Viability
+  imports OneWayNTS_Protocol
+
+begin
+
+
+section\<open>Viability of Two-Way NTS: Participants only say what they can synthesize\<close>
+
+lemma Br_knows_priSK[simp]:
+  "tr \<in> onewayNTS \<Longrightarrow> Key (priSK Br) \<in> knows_t Br tr"
+  apply (meson contra_subsetD initState_subset_knows priK_in_initState)
+  done
+
+lemma commit_viable: 
+      "\<lbrakk>tr \<in> onewayNTS; 
+        commit = create_commit ck n1 tvalid;
+        Nonce n1 \<in> knows_t Br tr;
+        Nonce ck \<in> knows_t Br tr
+        \<rbrakk>
+       \<Longrightarrow> commit \<in> synth (analz (knows_t Br tr))"
+  apply auto
+  done
+
+lemma ping_viable: 
+      "\<lbrakk>tr \<in> onewayNTS; 
+        ping = create_ping ck n1 tstmp;
+        Nonce n1 \<in> knows_t Br tr;
+        Nonce ck \<in> knows_t Br tr
+        \<rbrakk>
+       \<Longrightarrow> ping \<in> synth (analz (knows_t Br tr))"
+  using HPair_def 
+  apply auto
+  done
+
+lemma confirm_viable:
+      "\<lbrakk>tr \<in> onewayNTS;
+        confirm = create_confirm ck n1;
+        Nonce n1 \<in> knows_t Br tr;
+        Nonce ck \<in> knows_t Br tr
+       \<rbrakk> 
+       \<Longrightarrow> confirm \<in> synth (analz (knows_t Br tr))"
+  apply auto
+  done
+
+
+section\<open>Executability of Two-Way NTS with limited amount time context\<close>
+
+consts 
+  N1 :: nat
+  CK :: nat
+
+specification(N1 CK)
+  nonce_key_different: "N1 \<noteq> CK"
+  apply auto
+  done
+
+consts
+  T_INIT :: time
+  T_SND1 :: time
+  T_RCV1 :: time
+  T_SND2 :: time
+  T_RCV2 :: time
+  T_SND3 :: time
+  T_RCV3 :: time
+  T_DISP :: time
+
+specification (T_INIT T_SND1 T_RCV1 T_SND2 T_RCV2 T_SND3 T_RCV3 T_DISP)
+  order0: "T_INIT \<ge> 0"
+  order1: "T_SND1 \<ge> T_INIT"
+  order2: "T_RCV1 \<ge> T_SND1"
+  order3: "T_SND2 \<ge> T_RCV1"
+  order4: "T_RCV2 \<ge> T_SND2"
+  order5: "T_SND1 + DisclosureDelay > T_RCV2"
+  order6: "T_SND3 \<ge> T_SND1 + DisclosureDelay"
+  order7: "T_RCV3 \<ge> T_SND3"
+  order8: "T_DISP \<ge> T_RCV3"
+  apply auto 
+  apply (metis DiscDel_positive add.left_neutral order_refl)
+  done
+
+lemma onewayNTS_validrun_0:
+      "[(T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS.Nil onewayNTS.Init nonce_key_different order0
+  apply auto
+  done
+
+lemma onewayNTS_validrun_1:
+      "[(T_SND1, Says Br Alice (create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS_validrun_0 onewayNTS.Commit list.set_intros
+  apply auto
+  using event.simps(7) list.distinct(1) maxtime_aux2 order1 
+  apply fastforce
+  done
+
+lemma onewayNTS_validrun_1_rcv:
+      "[(T_RCV1, Gets Alice(create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_SND1, Says Br Alice (create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS_validrun_1 onewayNTS.Receive list.set_intros
+  apply auto
+  using maxtime_aux2 order2 
+  apply fastforce
+  done
+
+lemma onewayNTS_validrun_2:
+      "[(T_SND2, Says Br Alice (create_ping CK N1 T_SND2)),
+        (T_RCV1, Gets Alice(create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_SND1, Says Br Alice (create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS_validrun_1_rcv onewayNTS.Ping list.set_intros
+  apply auto
+  using maxtime_aux2 event.simps list.distinct(1) order3 order5
+  apply (smt le_less_trans list.set_intros(1) list.set_intros(2) order4)
+  done
+
+lemma onewayNTS_validrun_2_rcv:
+      "[(T_RCV2, Gets Alice (create_ping CK N1 T_SND2)),
+        (T_SND2, Says Br Alice (create_ping CK N1 T_SND2)),
+        (T_RCV1, Gets Alice(create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_SND1, Says Br Alice (create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS_validrun_2 onewayNTS.Receive list.set_intros
+  apply auto
+  apply (smt list.set_intros(1) maxtime_aux2 order4)
+  done
+
+lemma onewayNTS_validrun_3:
+      "[(T_SND3, Says Br Alice (create_confirm CK N1)),
+        (T_RCV2, Gets Alice (create_ping CK N1 T_SND2)),
+        (T_SND2, Says Br Alice (create_ping CK N1 T_SND2)),
+        (T_RCV1, Gets Alice(create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_SND1, Says Br Alice (create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS_validrun_2_rcv onewayNTS.Confirm list.set_intros
+  apply auto
+  using less_imp_le less_le_trans list.set_intros(1) maxtime_aux2 order5 
+             order6 set_subset_Cons subsetD
+  apply smt
+  done
+
+lemma onewayNTS_validrun_3_rcv:
+      "[(T_RCV3, Gets Alice (create_confirm CK N1)),
+        (T_SND3, Says Br Alice (create_confirm CK N1)),
+        (T_RCV2, Gets Alice (create_ping CK N1 T_SND2)),
+        (T_SND2, Says Br Alice (create_ping CK N1 T_SND2)),
+        (T_RCV1, Gets Alice(create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_SND1, Says Br Alice (create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS_validrun_3 onewayNTS.Receive list.set_intros
+  apply auto
+  using list.set_intros(1) maxtime_aux2 order7
+  apply smt
+  done
+
+lemma onewayNTS_validrun_4:
+      "\<exists> X.
+       [(T_RCV3, Notes Alice X),
+        (T_RCV3, Gets Alice (create_confirm CK N1)),
+        (T_SND3, Says Br Alice (create_confirm CK N1)),
+        (T_RCV2, Gets Alice (create_ping CK N1 T_SND2)),
+        (T_SND2, Says Br Alice (create_ping CK N1 T_SND2)),
+        (T_RCV1, Gets Alice(create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_SND1, Says Br Alice (create_commit CK N1 (T_SND1 + DisclosureDelay))),
+        (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  using onewayNTS_validrun_3_rcv onewayNTS.Discipline list.set_intros
+  apply auto
+  using list.set_intros(1) maxtime_aux2 order8 order7 
+        le_less set_subset_Cons subsetD order5
+         add_diff_cancel_left' diff_add_cancel  order_trans set_subset_Cons
+         insert_subset list.simps(15) order_refl order_trans
+proof -
+assume a1: "[(T_RCV3, Gets Alice \<lbrace>Nonce CK, Nonce N1\<rbrace>), (T_SND3, Says Br Alice \<lbrace>Nonce CK, Nonce N1\<rbrace>), (T_RCV2, Gets Alice Hash[Nonce CK] \<lbrace>Nonce N1, Number (encode_time T_SND2)\<rbrace>), (T_SND2, Says Br Alice Hash[Nonce CK] \<lbrace>Nonce N1, Number (encode_time T_SND2)\<rbrace>), (T_RCV1, Gets Alice \<lbrace>Crypt (priSK Br) \<lbrace>Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>, Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>), (T_SND1, Says Br Alice \<lbrace>Crypt (priSK Br) \<lbrace>Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>, Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>), (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+  assume a2: "\<And>trcv_ping ck1 n1 t1 tr trcv_commit tvalid tdiscp. \<lbrakk>(trcv_ping, Gets Alice Hash[Nonce ck1] \<lbrace>Nonce n1, Number (encode_time t1)\<rbrace>) \<in> set tr; (trcv_commit, Gets Alice \<lbrace>Crypt (priSK Br) \<lbrace>Hash (Nonce ck1), Nonce n1, Number (encode_time tvalid)\<rbrace>, Hash (Nonce ck1), Nonce n1, Number (encode_time tvalid)\<rbrace>) \<in> set tr; trcv_ping < tvalid; maxtime tr \<le> tdiscp; tr \<in> onewayNTS\<rbrakk> \<Longrightarrow> (tdiscp, Notes Alice (Number (encode_time (t1 - (trcv_ping - Offset - recent_offset Alice tr))))) # tr \<in> onewayNTS"
+  have f3: "\<forall>p ps pa. set ps \<subseteq> set ((pa::rat \<times> event) # p # ps)"
+    by (meson order_trans set_subset_Cons)
+  have f4: "\<forall>r n ra rb ps P na rc rd. (r, Gets Alice \<lbrace>Crypt (priSK Br) \<lbrace>Hash (Nonce na), Nonce n, Number (encode_time rc)\<rbrace>, Hash (Nonce na), Nonce n, Number (encode_time rc)\<rbrace>) \<notin> P \<or> \<not> maxtime ps \<le> rd \<or> \<not> rb < rc \<or> (rd, Notes Alice (Number (encode_time (ra - (rb - Offset - recent_offset Alice ps))))) # ps \<in> onewayNTS \<or> (rb, Gets Alice Hash[Nonce na] \<lbrace>Nonce n, Number (encode_time ra)\<rbrace>) \<notin> set ps \<or> ps \<notin> onewayNTS \<or> \<not> P \<subseteq> set ps"
+    using a2 by blast
+  have "\<forall>p pa ps pb. (pa::rat \<times> event) \<in> set (pb # p # pa # ps)"
+    by simp
+  then show "\<exists>m. [(T_RCV3, Notes Alice m), (T_RCV3, Gets Alice \<lbrace>Nonce CK, Nonce N1\<rbrace>), (T_SND3, Says Br Alice \<lbrace>Nonce CK, Nonce N1\<rbrace>), (T_RCV2, Gets Alice Hash[Nonce CK] \<lbrace>Nonce N1, Number (encode_time T_SND2)\<rbrace>), (T_SND2, Says Br Alice Hash[Nonce CK] \<lbrace>Nonce N1, Number (encode_time T_SND2)\<rbrace>), (T_RCV1, Gets Alice \<lbrace>Crypt (priSK Br) \<lbrace>Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>, Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>), (T_SND1, Says Br Alice \<lbrace>Crypt (priSK Br) \<lbrace>Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>, Hash (Nonce CK), Nonce N1, Number (encode_time (T_SND1 + DisclosureDelay))\<rbrace>), (T_INIT, Notes Br \<lbrace>Nonce CK, Nonce N1\<rbrace>)] \<in> onewayNTS"
+    using f4 f3 a1 by (metis (no_types) maxtime_aux2 order5 order_refl)
+qed
+
+lemma onewayNTS_Discipline:
+      "\<lbrakk>(tdiscp, Notes Alice X) \<in> set tr;
+        tr \<in> onewayNTS;
+        Alice \<notin> bad\<rbrakk>
+        \<Longrightarrow> \<exists> tsnd2 trcv2 ck n1 tr2. 
+            (trcv2, Gets Alice (create_ping ck n1 tsnd2)) \<in> set tr
+            \<and> X = Number (encode_time (tsnd2 - (clocktime_trace Alice tr2 trcv2)))"
+  apply(erule rev_mp, erule onewayNTS.induct)
+  using Alice_Br_different 
+  apply auto
+  done
+
+lemma onewayNTS_validrun_4_corr1:
+      "\<exists> tnotes tr offset.
+       tr \<in> onewayNTS
+       \<and> (tnotes, Notes Alice (offset)) \<in> set tr"
+  using onewayNTS_validrun_4
+  apply auto
+  apply (meson list.set_intros(1))
+  done
+
+lemma onewayNTS_validrun_4_corr2:
+      "Alice \<notin>bad
+       \<Longrightarrow> \<exists> tnotes tr offs tsnd2 trcv2 tr2.
+       tr \<in> onewayNTS
+       \<and> (tnotes, Notes Alice (Number (encode_time (tsnd2 - (clocktime_trace Alice tr2 trcv2))))) 
+         \<in> set tr"
+  using onewayNTS_validrun_4_corr1 onewayNTS_Discipline
+  apply auto
+  apply blast
+  done
+
+end
\ No newline at end of file
diff --git a/Traces_Timed.thy b/Traces_Timed.thy
new file mode 100644
index 0000000000000000000000000000000000000000..c2528520f39692bc8664058a4078a638c5621265
--- /dev/null
+++ b/Traces_Timed.thy
@@ -0,0 +1,568 @@
+(*  Title:  OneWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      Extensions of "event" and "event list" types (and all related operators 
+      and concepts) to timed contexts, for the purpose of analysing security 
+      properties of cryptographically protected time synchronisation protocols.
+
+    Acknowledgment: Parts of this theory are inspired by the "ProtoVeriPhy" work 
+                    by Benedikt Schmidt and Patrick Schaller from ETH Zurich. 
+                    
+                    Portions of their "Event.thy" files have been taken and 
+                    adapted for the present theory where appropriate.
+                    
+                    Note, however, that this is not a reproduction of that work.
+                    There are fundamental differences, due to the present theory 
+                    being realized via theories from the "Auth" folder of the 
+                    official Isabelle releases.
+*)
+
+theory Traces_Timed
+imports "~~/src/HOL/Auth/Event" HOL.Real
+begin
+
+section\<open>Foundations\<close>
+
+  type_synonym
+    time      =   rat
+    
+  type_synonym
+    event_t   =   "(time * event)"
+
+  consts eventTime :: "event \<Rightarrow> event_t"
+  
+  type_synonym
+    trace     =   "event list"
+    
+  type_synonym
+    trace_t   =   "event_t list"
+
+
+  lemma set_cons_eq_union_set:
+      "\<forall> ev evs. (set (ev # evs) = (set [ev]) \<union> (set evs))"
+  apply simp
+  done
+  
+  consts 
+    clocktime ::  "[agent, time] \<Rightarrow> time"
+
+
+section\<open>"occursAt..." Functions\<close>
+txt\<open>Functions are defined that extract the agent or the time
+    at which a given (timed) event occurs.\<close>
+
+primrec occursAtAgent :: "event \<Rightarrow> agent"
+  where
+        "occursAtAgent (Says A B X) = A"
+      | "occursAtAgent (Gets B X)   = B"
+      | "occursAtAgent (Notes A X)  = A"
+    
+  primrec occursAtAgent_t :: "event_t \<Rightarrow> agent"
+    where "occursAtAgent_t (t, ev) = occursAtAgent ev"
+  
+primrec occursAtTime_t :: "event_t \<Rightarrow> time"
+  where "occursAtTime_t (t, ev) = t"     
+    
+
+section\<open>The "maxtime" Operator\<close>
+txt\<open>A function is defined that returns the time at which
+   the latest event occurs in a given (timed) trace.\<close>     
+      
+  primrec maxtime :: "trace_t \<Rightarrow> time"
+  where
+      maxtime_empty:  "maxtime []     = (0 :: time)"
+    | maxtime_cons:   "maxtime (x#xs) = max (occursAtTime_t x) (maxtime xs)"
+    
+  lemma maxtime_non_negative [intro, simp]:
+    "maxtime tr >= 0"
+  apply (induct tr)
+  apply (auto)
+  done
+  
+  lemma maxtime_mono [simp]:
+    "maxtime tr = t \<Longrightarrow> maxtime (ev # tr) \<ge> t"
+  apply (auto)
+    done
+
+lemma maxtime_incr [simp]:
+    "maxtime (ev#tr) \<ge> occursAtTime_t ev"
+  apply simp
+  done
+  
+lemma maxtime_geq_elem:
+    assumes "maxtime tr \<le> t" 
+    (*assumes "maxtime tr \<le> t"*) 
+    and     "occursAtTime_t ev = te"
+    and     "ev \<in> set tr"
+    shows   "te \<le> t"
+    using assms
+    apply (induct tr)
+    apply simp
+    apply auto
+    done
+
+lemma there_is_later:
+      "\<forall> tr. \<exists> te. te \<ge> (maxtime tr)"
+  apply auto
+  done
+
+lemma there_is_strictly_later_time:
+      "\<forall> (t1::time). \<exists> t2. t2 > t1"
+  apply (simp add: linordered_field_no_ub)
+  done
+
+lemma there_is_later_time:
+      "\<forall> (t1::time). \<exists> t2. t2 \<ge> t1"
+  apply auto
+  done
+
+lemma there_is_strictly_later_times:
+      "\<forall> (t1::time) (t2::time). \<exists> t3. t3 > t1 \<and> t3 > t2"
+  using linordered_field_no_ub
+  apply (meson gt_ex less_le_trans not_less order.strict_trans)
+  done
+
+lemma there_is_later_times:
+      "\<forall> (t1::time) (t2::time). \<exists> t3. t3 \<ge> t1 \<and> t3 \<ge> t2"
+  using there_is_strictly_later_times
+  apply (meson linear)
+  done
+
+lemma there_is_strictly_later:
+      "\<forall> tr. \<exists> tl. tl > (maxtime tr)"
+  using gt_ex
+  apply auto
+  done
+
+lemma there_is_inbetween:
+      "tlater > (t::time) \<Longrightarrow> (\<exists> tb. tb \<ge> t \<and> tlater > tb)"
+  using gt_ex
+  apply auto
+  done
+
+lemma there_is_inbetween_2:
+      "tlater > (t::time) \<Longrightarrow> (\<exists> tb1 tb2. tb1 \<ge> t \<and> tlater > tb1 
+                                        \<and> tb2 \<ge> tb1 \<and> tlater > tb2)"
+  using there_is_inbetween gt_ex
+  apply auto
+  done
+                                
+
+section\<open>The "untime" Operator Family\<close>
+txt\<open>Functions are defined which eliminate the time coordinates from a given event (trace) 
+    and yield the untimed variant.\<close>
+
+  fun untimeEvent :: "event_t \<Rightarrow> event"
+  where 
+      "untimeEvent (t, Says A B X) = (Says A B X)"
+    | "untimeEvent (t, Gets B X)   = (Gets B X)"
+    | "untimeEvent (t, Notes B X)  = (Notes B X)"
+
+primrec untimeTrace_induct :: "trace_t \<Rightarrow> trace"
+  where
+      untimeTrace_induct_Nil  : "untimeTrace_induct [] = []"
+    | untimeTrace_induct_Cons : "untimeTrace_induct (ev # evs) = untimeEvent ev # untimeTrace_induct evs"
+
+lemma occursAtAgent_t_eq_occursAtAgent_untimeEvent:
+      "occursAtAgent_t ev = occursAtAgent (untimeEvent ev)"
+  using occursAtAgent_t.simps untimeEvent.elims
+  apply (metis)
+  done
+
+  
+section\<open>The "used_t" Operator\<close>
+txt\<open>The "used" operator is modified to accommodate timed traces.
+    Reasoning about the timed and untimed variant of "used" is performed.\<close>
+      
+  abbreviation (input)
+    used_t      :: "trace_t \<Rightarrow> msg set"
+    where          "used_t tr == used (untimeTrace_induct tr)"
+      
+  lemma used_mono:
+    "X \<in> used evs \<Longrightarrow> X \<in> used (ev#evs)"
+  apply (induct ev)
+  apply (auto)
+    done
+
+lemma used_t_mono:
+      "X \<in> used_t evs \<Longrightarrow> X \<in> used_t (ev # evs)"   
+    apply (simp add: used_mono)
+    done
+
+lemma used_ignores_list_order:
+      "used (eva # [evb]) = used (evb # [eva])"
+  apply (case_tac eva)
+    apply (case_tac evb)
+      apply simp_all
+      apply blast
+      apply blast
+    apply (case_tac evb)
+      apply simp_all
+    apply (case_tac evb)
+      apply simp_all
+      apply blast
+      apply blast
+    done
+
+lemma used_t_ignores_list_order:
+      "used_t (eva # [evb]) = used_t (evb # [eva])"
+  apply (simp add: used_ignores_list_order)
+  done
+
+lemma used_subset:
+      "set evsa \<subseteq> set evsb \<Longrightarrow> (x \<in> used evsa \<Longrightarrow> x \<in> used evsb)"
+  apply (induct evsa)
+  apply (meson subsetCE used_nil_subset)
+  apply (case_tac a)
+    apply simp
+    using Says_imp_analz_Spy Set.set_insert UnCI parts_analz parts_insert usedI
+    apply (metis)
+     apply simp
+     apply (induct evsb)
+     apply simp
+      apply (case_tac aa)
+        apply blast
+       apply blast
+      using UnCI UnE insert_subset list.simps(15) set_ConsD subset_iff used_Notes used_mono
+      apply (smt)
+      done
+
+  lemma used_t_subset:
+      "set evsa \<subseteq> set evsb \<Longrightarrow> (x \<in> used_t evsa \<Longrightarrow> x \<in> used_t evsb)"
+  apply (induct evsa)
+  using used_nil_subset 
+  apply force
+  apply (case_tac a)
+  apply (case_tac b)
+    apply simp_all
+    apply (induct evsb)
+    apply simp_all
+   apply (metis UnCI order_refl untimeEvent.simps(1) used_Says used_mono)
+  apply (induct evsb)
+  apply simp_all
+  apply (metis UnCI order_refl untimeEvent.simps(3) used_Notes used_mono)
+  done
+
+  lemma used_same_set:
+    "set evsa = set evsb \<Longrightarrow> used evsa = used evsb"
+    using subsetI subset_antisym used_subset
+    apply (metis)
+    done
+
+  lemma used_t_same_set:
+      "set evsa = set evsb \<Longrightarrow> used_t evsa = used_t evsb"
+  using  subsetI subset_antisym used_t_subset
+  apply (metis)
+  done
+
+
+section\<open>The Family of "view" Operators\<close>
+txt\<open>Functions are defined which limit a given event trace
+    to the part that is acually apparent to a given agent.\<close>
+
+  fun perspective_t :: "event_t \<Rightarrow> event_t"
+      where
+          "perspective_t (t, Says A B X) = ((clocktime A t), Says A B X)"
+        | "perspective_t (t, Gets B X)   = ((clocktime B t), Gets B X)"
+        | "perspective_t (t, Notes B X)  = ((clocktime B t), Notes B X)"
+
+  lemma untime_perspective_t_eq_untime :
+      "untimeEvent (perspective_t (t, ev)) = untimeEvent (t, ev)"
+    apply (cases ev)
+    apply simp_all
+    done
+
+primrec view :: "agent \<Rightarrow> trace \<Rightarrow> trace"
+  where   view_induct_Nil  :   "view A [] = []"
+        | view_induct_Cons :   "view A (ev # evs) =  (  if  occursAtAgent ev = A 
+                                                        then  ev # (view A evs)
+                                                        else  view A evs
+                                                      )"
+
+primrec view_t :: "agent \<Rightarrow> trace_t \<Rightarrow> trace_t"
+  where   view_t_induct_Nil  :   "view_t A [] = []"
+        | view_t_induct_Cons :   "view_t A (ev # evs) =  ( if  occursAtAgent_t ev = A 
+                                                              then (perspective_t ev) # (view_t A evs)
+                                                              else  view_t A evs
+                                                            )"
+
+  fun view_t_untimed :: "agent \<Rightarrow> trace_t \<Rightarrow> event list"
+    where "view_t_untimed A tr = view A (untimeTrace_induct tr)"
+
+
+lemma untimeTrace_view_eq_view_t_untimed:
+      "(untimeTrace_induct (view_t A tr)) = view A (untimeTrace_induct tr)"
+  apply (induct tr)
+   apply simp
+  using untime_perspective_t_eq_untime occursAtAgent_t_eq_occursAtAgent_untimeEvent 
+  apply auto
+  done 
+  
+  
+  lemma view_occurs_at:
+    "ev \<in> set (view A tr) \<Longrightarrow> occursAtAgent ev = A"
+    apply (induct tr)
+     apply simp
+    apply (case_tac a)
+    apply simp_all
+    using occursAtAgent.simps(1) set_ConsD
+      apply smt
+    using occursAtAgent.simps(2) set_ConsD
+    apply smt
+    using occursAtAgent.simps(3) set_ConsD
+    apply smt
+    done
+  
+  lemma view_t_occurs_at_t:
+    "ev \<in> set (view_t A tr) \<Longrightarrow> occursAtAgent_t ev = A"
+    apply (induct tr)
+     apply simp
+    apply (case_tac a)
+    apply (case_tac b)
+      apply simp_all
+    using occursAtAgent_t.simps(1) set_ConsD occursAtAgent_t_eq_occursAtAgent_untimeEvent untimeEvent.simps(1) untime_perspective_t_eq_untime
+      apply (metis (mono_tags, lifting) occursAtAgent.simps(1) )
+     apply (metis (mono_tags, lifting) occursAtAgent.simps(2) occursAtAgent_t_eq_occursAtAgent_untimeEvent set_ConsD untimeEvent.simps(2) untime_perspective_t_eq_untime)
+    apply (metis (mono_tags, lifting) occursAtAgent.simps(3) occursAtAgent_t_eq_occursAtAgent_untimeEvent set_ConsD untimeEvent.simps(3) untime_perspective_t_eq_untime)
+    done  
+  
+  lemma view_subset:
+    "set (view_t_untimed A tr) \<subseteq> set (untimeTrace_induct tr)"
+    apply (induct tr)
+    apply simp
+    apply auto
+  done
+  
+  lemma used_view_subset:
+    "used (view A tr) \<subseteq> used tr"
+  apply (induct tr)
+  apply (auto simp add: used.simps split: event.split)
+  done
+  
+lemma Notes_t_Notes:
+      "(t, Notes A X) \<in> set evs \<Longrightarrow> Notes A X \<in> set (untimeTrace_induct evs)" 
+  apply (induct evs)
+  apply simp_all
+  apply auto
+  done
+  
+  
+lemma Notes_imp_used_t [rule_format]: 
+      "(t, Notes A X) \<in> set evs \<Longrightarrow> X \<in> used_t evs"
+  using Notes_imp_used Notes_t_Notes 
+  apply blast
+  done
+
+lemma Says_imp_used_t [rule_format]: 
+      "(t, Says A B X) \<in> set evs --> X \<in> used_t evs"
+apply (induct_tac evs)
+apply (auto split: event.split)
+apply (simp add: used_mono Notes_t_Notes)
+done
+
+
+section\<open>The "knows_t" Operator\<close>
+txt\<open>A functions is defined which, for a given timed event trace
+    returns the knowledge of a given agent.\<close>
+
+abbreviation (input)
+  knows_t :: "agent \<Rightarrow> trace_t \<Rightarrow> msg set"
+  where      "knows_t A tr == knows A (untimeTrace_induct tr)"
+
+lemma knows_t_initState:
+      "knows_t A [] = initState A"
+  apply auto
+  done
+
+lemma in_set_untimed_implies_in_set_timed:
+  "ev \<in> set (untimeTrace_induct tr)
+  \<Longrightarrow> EX t.
+         (t, ev) \<in> set tr"
+  apply (induct tr)
+   apply simp
+  using untimeEvent.elims insert_iff list.set(2) untimeTrace_induct.simps(2)
+  apply smt
+  done
+  
+abbreviation (input)
+  spies_t  :: "event_t list => msg set" 
+  where       "spies_t == knows_t Spy"
+
+lemma knows_t_Spy_Says [simp]:
+      "knows_t Spy ((t, Says A B X) # evs) = insert X (knows_t Spy evs)"
+by simp
+
+lemma knows_t_Spy_Notes [simp]:
+      "knows_t Spy ((t, Notes A X) # evs) =  
+          (if A:bad then insert X (knows_t Spy evs) else knows_t Spy evs)"
+by simp
+
+lemma knows_t_Spy_Gets [simp]: 
+      "knows_t Spy ((t, Gets A X) # evs) = knows_t Spy evs"
+by simp
+
+lemma knows_t_Spy_subset_knows_t_Spy_Says:
+      "knows_t Spy evs \<subseteq> knows_t Spy ((t, Says A B X) # evs)"
+by (simp add: subset_insertI)
+
+lemma knows_t_Spy_subset_knows_t_Spy_Notes:
+      "knows_t Spy evs \<subseteq> knows_t Spy ((t, Notes A X) # evs)"
+by force
+
+lemma knows_t_Spy_subset_knows_t_Spy_Gets:
+      "knows_t Spy evs \<subseteq> knows_t Spy ((t, Gets A X) # evs)"
+by (simp add: subset_insertI)
+
+txt\<open>Spy sees what is sent on the traffic\<close>
+lemma Says_imp_knows_t_Spy [rule_format]:
+      "(t, Says A B X) \<in> set evs --> X \<in> knows_t Spy evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split: event.split)
+using knows_subset_knows_Cons 
+apply fastforce
+done
+
+lemma Notes_imp_knows_t_Spy [rule_format]:
+      "(t, Notes A X) \<in> set evs --> A: bad --> X \<in> knows_t Spy evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split: event.split)
+using knows_subset_knows_Cons 
+apply fastforce
+done
+
+txt\<open>Elimination rules: derive contradictions from old Says events containing
+    items known to be fresh\<close>
+lemmas Says_imp_parts_t_knows_t_Spy = 
+       Says_imp_knows_t_Spy [THEN parts.Inj, elim_format] 
+
+lemmas knows_t_Spy_parts_tEs =
+       Says_imp_parts_t_knows_t_Spy parts.Body [elim_format]
+
+txt\<open>Compatibility for the old "spies" function\<close>
+lemmas spies_t_parts_tEs = knows_t_Spy_parts_tEs
+lemmas Says_imp_spies_t = Says_imp_knows_t_Spy
+lemmas parts_t_insert_spies_t = parts_insert_knows_A [of _ Spy]
+
+
+subsection\<open>Knowledge of Agents\<close>
+
+lemma knows_t_subset_knows_t_Says: 
+      "knows_t A evs \<subseteq> knows_t A ((t, Says A' B X) # evs)"
+apply (simp add: subset_insertI)
+apply (simp add: knows_subset_knows_Cons)
+done
+
+lemma knows_t_subset_knows_t_Notes: 
+      "knows_t A evs \<subseteq> knows_t A ((t, Notes A' X) # evs)"
+apply (simp add: subset_insertI)
+apply (simp add: knows_subset_knows_Cons)
+done
+
+lemma knows_t_subset_knows_t_Gets: 
+      "knows_t A evs \<subseteq> knows_t A ((t, Gets A' X) # evs)"
+apply (simp add: subset_insertI)
+apply (simp add: knows_subset_knows_Cons)
+done
+
+txt\<open>Agents know what they say\<close>
+lemma Says_imp_knows_t [rule_format]: 
+      "(t, Says A B X) \<in> set evs --> X \<in> knows_t A evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split: event.split)
+apply (metis Says_imp_knows contra_subsetD knows_subset_knows_Cons list.set_intros(1) 
+             untimeEvent.simps(1))
+done
+
+txt\<open>Agents know what they note\<close>
+lemma Notes_imp_knows_t [rule_format]: 
+      "(t, Notes A X) \<in> set evs --> X \<in> knows_t A evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split: event.split)
+using Notes_imp_knows Notes_t_Notes 
+apply auto
+done
+
+txt\<open>Agents know what they receive\<close>
+lemma Gets_imp_knows_t_agents [rule_format]:
+      "A \<noteq> Spy --> (t, Gets A X) \<in> set evs --> X \<in> knows_t A evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split: event.split)
+using Gets_imp_knows_agents knows_subset_knows_Cons 
+apply fastforce
+  done
+
+txt\<open>What agents DIFFERENT FROM Spy know 
+    was either said, or noted, or got, or known initially\<close>
+lemma knows_t_imp_Says_Gets_Notes_initState [rule_format]:
+      "[| X \<in> knows_t A evs; A \<noteq> Spy |] 
+       ==> EX t B.  
+             (t, Says A B X) \<in> set evs 
+           | (t, Gets A X) \<in> set evs 
+           | (t, Notes A X) \<in> set evs 
+           | X \<in> initState A"
+  apply (erule rev_mp)
+  apply (induct_tac "evs")
+  apply simp
+  using in_set_untimed_implies_in_set_timed knows_imp_Says_Gets_Notes_initState
+  apply (smt Gets_imp_knows_agents Notes_imp_knows Says_imp_knows list.set_intros(1) list.simps(9) set_ConsD set_subset_Cons subset_iff untimeTrace_induct.simps(2))
+  done
+
+txt\<open>What the Spy knows -- for the time being --
+    was either said or noted, or known initially\<close>
+lemma knows_t_Spy_imp_Says_Notes_initState [rule_format]:
+      "[| X \<in> knows_t Spy evs |] 
+          ==> EX t A B.  
+            (t, Says A B X) \<in> set evs 
+          | (t, Notes A X) \<in> set evs 
+          | X \<in> initState Spy"
+ using in_set_untimed_implies_in_set_timed
+  apply (meson knows_Spy_imp_Says_Notes_initState)
+  done
+
+lemma initState_into_used_t: 
+      "X \<in> parts (initState B) ==> X \<in> used_t evs"
+  using initState_into_used
+  apply blast
+  done
+
+lemma used_t_Says [simp]: 
+      "used_t ((t, Says A B X) # evs) = parts{X} \<union> used_t evs"
+by simp
+
+lemma used_t_Notes [simp]: 
+      "used_t ((t, Notes A X) # evs) = parts{X} \<union> used_t evs"
+apply (auto)
+done
+
+lemma used_t_Gets [simp]: 
+      "used_t ((t, Gets A X) # evs) = used_t evs"
+by simp
+
+lemma used_t_nil_subset: 
+      "used_t [] \<subseteq> used_t evs"
+  apply simp
+  using initState_into_used_t
+  apply (simp add: used_nil_subset)
+  done
+
+lemmas analz_t_mono_contra =
+       knows_t_Spy_subset_knows_t_Spy_Says [THEN analz_mono, THEN contra_subsetD]
+       knows_t_Spy_subset_knows_t_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
+       knows_t_Spy_subset_knows_t_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
+
+       
+lemma knows_t_subset_knows_t_Cons: 
+      "knows_t A evs \<subseteq> knows_t A (e # evs)"
+  apply (cases e)
+  apply(auto simp: knows_Cons)
+  using knows_Cons knows_subset_knows_Cons 
+  apply (fastforce)
+  using event.simps(10) event.simps(11) event.simps(12) insert_iff untimeEvent.elims
+  apply (smt)
+  done
+
+
+end
\ No newline at end of file
diff --git a/TwoWayNTS_Guarantees.thy b/TwoWayNTS_Guarantees.thy
new file mode 100644
index 0000000000000000000000000000000000000000..c858e734c2c99699d6d88e0568a09dd1452b5019
--- /dev/null
+++ b/TwoWayNTS_Guarantees.thy
@@ -0,0 +1,332 @@
+(*  Title:  TwoWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      The security proofs on the model for the two-way variant of NTS.
+*)
+
+theory TwoWayNTS_Guarantees
+  imports TwoWayNTS_Protocol
+
+begin
+
+
+txt\<open>Security properties of Two-Way NTS\<close>
+
+
+section\<open>Regularity Properties\<close>
+
+txt\<open>Server key remains secret throughout the protocol.\<close>
+lemma shrK_Br_not_lost: "tr \<in> twowayNTS
+                       \<Longrightarrow> Key (shrK Br) \<notin> analz (knows_t Spy tr)"
+  apply (erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        using shrK_not_initially_lost apply auto[1]
+  txt\<open>Case: Fake\<close>       using synth_analz_insert_eq apply auto[1]
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Request\<close>    apply auto[1]
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+txt\<open>Client key remain secret throughout the protocol.\<close>
+lemma shrK_Alice_not_lost: 
+      "\<lbrakk>Alice \<notin> bad; 
+        tr \<in> twowayNTS\<rbrakk>
+       \<Longrightarrow> Key (shrK Alice) \<notin> analz (knows_t Spy tr)"
+  apply (erule twowayNTS.induct)
+  txt\<open>Case Nil\<close>         using shrK_not_initially_lost apply auto[1]
+  txt\<open>Case Fake\<close>        using synth_analz_insert_eq apply auto[1]
+  txt\<open>Case Receive\<close>     apply auto[1]
+  txt\<open>Case Request\<close>     using shrK_Br_not_lost apply auto[1]
+  txt\<open>Case Response\<close>    apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+txt\<open>An HMAC tag (request type) is only not introduced 
+    unless a full request message is introduced.\<close>
+lemma if_request_tag_then_request:
+      "\<lbrakk>Alice \<notin> bad;  
+                M = create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                                   (shrK Alice) n1 t1;
+                tr \<in> twowayNTS\<rbrakk>
+               \<Longrightarrow>   (request_tag (Crypt (shrK Br) (Key (shrK Alice))) 
+                                  (shrK Alice) n1 t1 
+                      \<in> analz (knows_t Spy tr)
+                     \<longrightarrow> M \<in> analz (knows_t Spy tr))"
+  apply (erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp[1] 
+                        apply (metis Hash_notin_image_Key analz_image_Key image_Un)
+  txt\<open>Case: Fake\<close>       using analz_t_mono_contra(1) apply auto[1] 
+                        using shrK_Br_not_lost Fake_analz_eq Hash_synth_analz 
+                            shrK_Alice_not_lost synth_simps(2) apply (metis )
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Request\<close>    apply simp[1] using shrK_Br_not_lost apply (blast)
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+txt\<open>An HMAC tag (response type) is not introduced 
+    unless a full response message is introduced.\<close>
+lemma if_response_tag_then_response:
+      "\<lbrakk>Alice \<notin> bad;      
+        M = create_response (shrK Alice) n1 n2 t2 t3;
+        tr \<in> twowayNTS\<rbrakk>
+       \<Longrightarrow> (response_tag (shrK Alice) n1 n2 t2 t3 \<in> analz (knows_t Spy tr) 
+           \<longrightarrow> M \<in> analz (knows_t Spy tr))"
+  apply (erule rev_mp)
+  apply (erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp apply (metis Hash_notin_image_Key analz_image_Key image_Un)
+  txt\<open>Case: Fake\<close>       using Fake_analz_eq Hash_synth_analz analz_insertI 
+                              shrK_Alice_not_lost synth_simps(2) 
+                        apply (simp, metis )
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Request\<close>    using shrK_Br_not_lost shrK_Alice_not_lost 
+                        apply auto[1]
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+
+section\<open>Structure Properties\<close>
+
+txt\<open>Whenever the client says anything, it is a proper and
+    well-formed request message.\<close>
+lemma Alice_says_request: 
+      "\<lbrakk>(tsend, Says Alice Br X) \<in> set tr; 
+        Alice \<notin> bad; 
+        tr \<in> twowayNTS\<rbrakk>
+       \<Longrightarrow> \<exists> n1 oldtr. X =  create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                                     (shrK Alice) n1 (clocktime_trace Alice oldtr tsend)"
+  apply(erule rev_mp, erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp[1] 
+  txt\<open>Case: Fake\<close>       apply auto[1]
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Request\<close>    apply auto[1] 
+  txt\<open>Case: Response\<close>   apply (simp add: Alice_Br_different)
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+txt\<open>Whenever the server says anything, it is a proper and
+    well-formed response message.\<close>
+lemma Br_says_response: "\<lbrakk>(tsend, Says Br Alice X) \<in> set tr; 
+                          Alice \<notin> bad; tr \<in> twowayNTS\<rbrakk>
+                         \<Longrightarrow> \<exists> n1 n2 t1 requestkey. 
+                               X = create_response requestkey n1 n2 t1 (clocktime Br tsend)"
+  apply(erule rev_mp, erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp[1] 
+  txt\<open>Case: Fake\<close>       apply auto[1] using Br_honest 
+                        apply auto[1]
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Request\<close>    apply (simp add: Alice_Br_different) 
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+
+section\<open>Authenticity Properties\<close>
+
+subsection\<open>Authenticity - Global Perspective\<close>
+
+txt\<open>If a message on the wire is a well-formed request message,
+    then the client has said it.\<close>
+theorem message_authentication_global_perspective_request: 
+        "\<lbrakk>X \<in> analz (knows_t Spy tr); Alice \<notin> bad;  
+          \<exists> n1 t1. X = create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                             (shrK Alice) 
+                             n1 
+                             ( t1); 
+          tr \<in> twowayNTS\<rbrakk> 
+         \<Longrightarrow> \<exists> tsay. (tsay, Says Alice Br X) \<in> set tr"
+  apply(erule rev_mp, erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1] 
+                        apply (metis HPair_def analz_image_Key imageE image_Un msg.distinct(33))
+  txt\<open>Case: Fake\<close>       apply simp
+                        using spy_cannot_break_hmac_protection_set create_request_hmac_protected
+                              if_request_tag_then_request shrK_Alice_not_lost HPair_def                      
+                        apply (metis Fake_analz_eq One_nat_def request_tag.simps synth.Inj)
+  txt\<open>Case: Receive\<close>    apply simp[1]
+  txt\<open>Case: Request\<close>    using shrK_Br_not_lost 
+                        apply auto[1]
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+txt\<open>If a message on the wire is a well-formed response message,
+    then the server has said it.\<close>
+theorem message_authentication_global_perspective_response: 
+        "\<lbrakk>X \<in> analz (knows_t Spy tr); Alice \<notin> bad; 
+          \<exists> n1 n2 t2 t3. X = create_response (shrK Alice) n1 n2 t2 t3; 
+          tr \<in> twowayNTS\<rbrakk> 
+         \<Longrightarrow> \<exists> n1 n2 n2 tsay. (tsay, Says Br Alice X) \<in> set tr"
+  apply(erule rev_mp, erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1] 
+                        apply (metis HPair_def analz_image_Key imageE image_Un 
+                                     msg.distinct(33))
+  txt\<open>Case: Fake\<close>       apply simp
+                        using spy_cannot_break_hmac_protection_set 
+                            create_response_hmac_protected
+                            if_response_tag_then_response shrK_Alice_not_lost 
+                            Fake_analz_eq HPair_def synth.Inj response_tag.simps
+                        apply (metis )
+  txt\<open>Case: Receive\<close>    apply auto[1]
+  txt\<open>Case: Request\<close>    using shrK_Br_not_lost 
+                        apply auto[1]
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+
+subsection\<open>Authenticity - Participant Perspectives\<close>
+
+txt\<open>If the server gets a message that satisfies the proper format for a request message 
+    and uses the correct keys, then the client has said it (previously).\<close>
+theorem message_authentication_server_perspective_request:
+        "\<lbrakk>(tget, Gets Br X) \<in> set tr; Alice \<notin> bad; 
+           \<exists> n1 t1. X = create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                              (shrK Alice) n1 (t1);
+           tr \<in> twowayNTS\<rbrakk> 
+         \<Longrightarrow> \<exists> tsay n1 oldtr. (tsay, Says Alice Br X) \<in> set tr \<and> tsay \<le> tget
+             \<and> X = create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                              (shrK Alice) n1 (clocktime_trace Alice oldtr tsay)"
+  apply(erule rev_mp, erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp[1]
+  txt\<open>Case: Fake\<close>       apply auto[1]
+  txt\<open>Case: Receive\<close>    using message_authentication_global_perspective_request
+                              Says_imp_knows_t_Spy maxtime_geq_elem 
+                        apply auto[1]
+                        using analz.Inj create_request.simps Alice_says_request msg.inject
+                              Alice_clock_linear Br_clock_perfect HPair_eq analz.Inj                               
+                        apply (smt create_request.simps clocktime_trace.simps)
+  txt\<open>Case: Request\<close>    apply auto[1]
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+txt\<open>If the client gets a message that satisfies the proper format for a response message 
+    and uses the correct keys, then the server has said it (previously).\<close>
+theorem message_authentication_client_perspective_response:
+        "\<lbrakk>(tget, Gets Alice X) \<in> set tr; 
+           Alice \<notin> bad; 
+           \<exists> n1 n2 t2 t3. X = create_response (shrK Alice) n1 n2 t2 t3; 
+           tr \<in> twowayNTS\<rbrakk> 
+         \<Longrightarrow> \<exists> tsay n1 n2 t2. (tsay, Says Br Alice  X) \<in> set tr 
+                     \<and> tsay \<le> tget
+                     \<and> X = create_response (shrK Alice) n1 n2 t2 (clocktime Br tsay)"
+  apply(erule rev_mp, erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply simp
+  txt\<open>Case: Fake\<close>       apply auto[1]
+  txt\<open>Case: Receive\<close>    using message_authentication_global_perspective_response 
+                              Says_imp_knows_t_Spy maxtime_geq_elem 
+                        apply auto[1]
+                        using Br_says_response Br_clock_perfect HPair_eq analz.Inj
+                        apply (smt  create_response.simps msg.inject(2) msg.inject(6))
+  txt\<open>Case: Request\<close>    apply auto[1]
+  txt\<open>Case: Response\<close>   apply auto[1]
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+
+section\<open>Timeliness Properties\<close>
+
+subsection\<open>Timeliness - Event Ordering and Time Windows\<close>
+
+txt\<open>If a correlating pair of a request and a response message have been said,
+    then the request was said before the response.\<close>
+lemma message_order_request_before_matching_response:
+      "\<lbrakk>\<exists> request response n1.
+          (treq, Says Alice Br request) \<in> set tr
+          \<and> (tresp, Says Br Alice response) \<in> set tr
+          \<and> valid_sync_pair request response;
+        Alice \<notin> bad;
+        tr \<in> twowayNTS \<rbrakk>
+       \<Longrightarrow> treq \<le> tresp"
+  apply(erule rev_mp, erule twowayNTS.induct)
+  txt\<open>Case: Nil\<close>        apply auto[1]
+  txt\<open>Case: Fake\<close>       using shrK_Br_not_lost apply force
+  txt\<open>Case: Receive\<close>    apply fastforce
+  txt\<open>Case: Request\<close>    apply auto[1]
+                          txt \<open>Goal 1\<close>  apply (metis HPair_def MPair_used_D Says_imp_used_t)
+                          txt \<open>Goal 2\<close>  apply blast
+  txt\<open>Case: Response\<close>   using Alice_Br_different event.inject(1) maxtime_geq_elem 
+                            occursAtTime_t.simps prod.inject set_ConsD 
+                        apply (metis)
+  txt\<open>Case: Discipline\<close> apply auto[1]
+  done
+
+txt\<open>If the client gets a response message for which it has said the correlating request,
+    then the response was said after the request and before it was received.\<close>
+lemma client_perspective_server_response_timewindow_clocktime_trace:
+        "\<lbrakk>(t4, Gets Alice response) \<in> set tr;
+          \<exists> n1 n2 t2 t3 request.
+              response = create_response (shrK Alice) n1 n2 t2 t3
+            \<and> request = create_request (Crypt (shrK Br) (Key (shrK Alice)))
+                                 (shrK Alice) n1 (clocktime_trace Alice oldtr t1)
+            \<and> (t1, Says Alice Br request) \<in> set tr;
+          Alice \<notin> bad;
+          tr \<in> twowayNTS\<rbrakk> 
+         \<Longrightarrow> \<exists> tresp n1 n2 t3. 
+                (t3, Says Br Alice response) \<in> set tr
+              \<and> t3 \<le> t4 \<and> t1 \<le> t3"
+  using message_authentication_client_perspective_response
+        message_order_request_before_matching_response 
+  apply auto
+  using Alice_clock_linear Br_clock_perfect 
+  apply blast
+  done
+
+subsection\<open>Timeliness - Auxiliary\<close>
+
+txt\<open>If a point-in-time lies between two others, then the distance from the inner point  to the 
+    middle of the two outer points is no more than half the distance between the outer points.\<close>
+lemma arithmetic_1:
+      "\<lbrakk>x \<le> y; y \<le> z; 
+        clocktime Alice x = clocktime Alice x\<rbrakk> 
+       \<Longrightarrow> (x+z)/2 - y \<le> (z-x)/2
+        \<and>  y -(x+z)/2 \<le> (z-x)/2"
+  apply (simp add: add_divide_distrib)
+  done
+
+txt\<open>The previous lemma still holds if a constant value is added to both outer points in the
+    evaluation of distances.\<close>
+lemma clocktime_approx_clocktime_trace:
+      "\<lbrakk>t1 \<le> t3; t3 \<le> t4\<rbrakk>
+       \<Longrightarrow> abs(Offset + (recent_offset Alice tr) 
+              - (t3 - ((clocktime_trace Alice tr t1) + (clocktime_trace Alice tr t4))/2)) 
+           \<le> (t4 - t1)/2"
+  apply auto
+  using abs_le_iff add.commute add_divide_eq_iff arithmetic_1 diff_add_cancel 
+        diff_diff_eq2 minus_diff_eq mult.commute rel_simps(76)
+        le_divide_eq_numeral1(1)  clocktime_trace.simps comm_semiring_class.distrib
+  apply simp
+  using abs_le_iff add.commute add_divide_eq_iff arithmetic_1 diff_add_cancel 
+        diff_diff_eq2 minus_diff_eq mult.commute rel_simps(76)  clocktime_trace.simps
+        le_divide_eq_numeral1(1) comm_semiring_class.distrib
+  apply (smt comm_semiring_class.distrib)
+  done
+
+subsection\<open>Timeliness - Synchronization\<close>
+
+txt\<open>If the client receives a proper response, then the offset it calculates as the difference
+    between t3 (server reception of request) is at most (t4 - t1) away from its true offset.\<close>
+theorem client_perspective_offset_calculation:
+        "\<lbrakk>(t4, Gets Alice response) \<in> set tr;
+          \<exists> request.
+              response = create_response (shrK Alice) n1 n2 t2 t3
+            \<and> request = create_request (Crypt (shrK Br) (Key (shrK Alice)))
+                                       (shrK Alice) n1 (clocktime_trace Alice oldtr t1)
+            \<and> (t1, Says Alice Br request) \<in> set tr;
+          Alice \<notin> bad;
+          tr \<in> twowayNTS\<rbrakk> 
+         \<Longrightarrow> abs(Offset + (recent_offset Alice oldtr) - 
+                 (t3 - ((clocktime_trace Alice oldtr t1) + (clocktime_trace Alice oldtr t4))/2)) 
+             \<le>  (t4 - t1)/2"
+  using clocktime_approx_clocktime_trace Br_says_response HPair_def 
+        client_perspective_server_response_timewindow_clocktime_trace           
+  apply auto 
+  apply (smt encode_decode_time msg.inject(2) msg.inject(6))
+  done
+
+
+end
\ No newline at end of file
diff --git a/TwoWayNTS_Protocol.thy b/TwoWayNTS_Protocol.thy
new file mode 100644
index 0000000000000000000000000000000000000000..e15d9d49d567e256f852253002b40c38945afae3
--- /dev/null
+++ b/TwoWayNTS_Protocol.thy
@@ -0,0 +1,166 @@
+(*  Title:   TwoWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      The protocol model for the two-way variant of NTS.
+*)
+
+theory TwoWayNTS_Protocol
+  imports EntryPoint_SecureTime
+
+begin
+
+
+section\<open>Setup of the environment for Two-Way NTS\<close>
+
+consts
+  Offset    :: time   (* time offset between Alice and Br *)
+  Br        :: agent  (* honest broadcaster *)
+  Alice     :: agent  (* honest time client *)
+
+
+specification(clocktime Alice Br Offset)
+  Br_clock_perfect [simp]:    "clocktime Br t = t"
+  Alice_clock_linear [simp]:  "clocktime Alice t 
+                               = clocktime Br t - Offset"
+  Br_honest [simp]:           "Br \<notin> bad"
+  Alice_Br_different:         "Alice \<noteq> Br"
+  apply fastforce
+  done
+
+fun recent_offset :: "agent \<Rightarrow> trace_t \<Rightarrow> time"
+  where "recent_offset A [] = 0"
+  | "recent_offset A (ev # tr) = (if \<exists>X t. ev = (t, Notes A (Number (encode_time X))) 
+                                then 0 
+                                else recent_offset A tr)"
+
+fun clocktime_trace :: "agent \<Rightarrow> trace_t \<Rightarrow> time \<Rightarrow> time"
+  where "clocktime_trace A tr t = clocktime A t - recent_offset A tr"
+
+
+section\<open>Definition of and basic reasoning about employed message formats\<close>
+
+abbreviation  nts2w_REQUEST ::  msg where "nts2w_REQUEST  \<equiv> Nonce 1"
+abbreviation  nts2w_RESPONSE :: msg where "nts2w_RESPONSE \<equiv> Nonce 2"
+
+fun create_request :: "msg \<Rightarrow> key \<Rightarrow> nat \<Rightarrow> time \<Rightarrow> msg"
+  where "create_request requestkiv requestkey n1 t1 
+         = Hash[Key requestkey]
+               \<lbrace>nts2w_REQUEST, requestkiv,  Nonce n1, (Number (encode_time t1))\<rbrace>"
+
+fun request_tag :: "msg \<Rightarrow> key \<Rightarrow> nat \<Rightarrow> time \<Rightarrow> msg"
+  where "request_tag requestkiv requestkey n1 t1
+         = Hash \<lbrace>Key requestkey,
+                  \<lbrace>nts2w_REQUEST, requestkiv,  Nonce n1, (Number (encode_time t1))\<rbrace> \<rbrace>"
+
+abbreviation is_valid_request :: "msg \<Rightarrow> bool"
+  where "is_valid_request m \<equiv> 
+         (\<exists> requestkiv requestkey n1 t1.
+            m = Hash[Key requestkey] 
+                    \<lbrace>nts2w_REQUEST,requestkiv, Nonce n1, (Number (encode_time t1))\<rbrace>
+                \<and> requestkiv = (Crypt (shrK Br) (Key requestkey))
+         )"
+
+lemma create_request_hmac_protected:
+      "requestkey HashAuthenticates \<lbrace>nts2w_REQUEST, requestkiv, Nonce n1, Number (encode_time t1)\<rbrace> 
+                  inside (create_request requestkiv requestkey n1 t1)"
+  apply auto
+  done
+
+fun create_response :: "key \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> time \<Rightarrow> time \<Rightarrow> msg"
+  where "create_response responsekey n1 n2 t2 t3 
+          = Hash[Key responsekey] 
+                \<lbrace>nts2w_RESPONSE, Nonce n1, Nonce n2, (Number (encode_time t2)), (Number (encode_time t3))\<rbrace>"
+
+fun response_tag :: "key \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> time \<Rightarrow> time \<Rightarrow> msg"
+  where "response_tag responsekey n1 n2 t2 t3 
+          = Hash\<lbrace>Key responsekey,
+                \<lbrace>nts2w_RESPONSE, Nonce n1, Nonce n2, (Number (encode_time t2)), (Number (encode_time t3))\<rbrace> \<rbrace>"
+
+abbreviation is_valid_response :: "msg \<Rightarrow> bool"
+  where "is_valid_response m 
+          \<equiv> (\<exists> responsekey n1 n2 t2 t3.
+                m = Hash[responsekey] 
+                        \<lbrace>nts2w_RESPONSE, Nonce n1, Nonce n2, (Number (encode_time t2)), (Number (encode_time t3))\<rbrace>
+             )"
+
+lemma is_valid_create_response:
+  "is_valid_response (create_response key n1 n2 t2 t3)"
+  apply auto
+  done
+
+lemma create_response_hmac_protected:
+      "responsekey 
+        HashAuthenticates \<lbrace>nts2w_RESPONSE, Nonce n1, Nonce n2, (Number (encode_time t2)), (Number (encode_time t3))\<rbrace>
+        inside (create_response responsekey n1 n2 t2 t3)"
+  apply auto
+  done
+
+abbreviation concerns_nonce :: "nat \<Rightarrow> msg \<Rightarrow> bool"
+  where "concerns_nonce n1 m \<equiv>    (\<exists> kiv key t1.
+                                      m = create_request kiv key n1 t1) 
+                                \<or> (\<exists> key n2 t2 t3.
+                                      m = create_response key n1 n2 t2 t3)"
+
+abbreviation valid_sync_pair :: "msg \<Rightarrow> msg \<Rightarrow> bool"
+  where "valid_sync_pair m1 m2 
+          \<equiv> (\<exists> key n1 n2 t1 t2 t3.(
+                m1 = create_request  (Crypt (shrK Br) (Key key)) key n1 t1
+              \<and> m2 = create_response key n1 n2 t2 t3))"
+
+section\<open>Specification of the actual protocol as inductive set of traces\<close>
+
+inductive_set
+ twowayNTS :: "(trace_t) set"
+ where
+
+  (* Global, protocol-independent Rules*)
+
+   Nil [intro] : "[] \<in> twowayNTS"
+
+ | Fake:
+  "\<lbrakk> tr \<in> twowayNTS;  t \<ge>  maxtime tr; X \<in> synth (analz (knows_t Spy tr))\<rbrakk>
+  \<Longrightarrow> (t, Says Spy B X) # tr \<in> twowayNTS"
+
+ | Receive:
+  "\<lbrakk> tr \<in> twowayNTS; (tsend, Says A B X) \<in> set tr; trecv \<ge> maxtime tr \<rbrakk>
+   \<Longrightarrow> (trecv, Gets C X) # tr \<in> twowayNTS"
+
+ (* Protocol rules for one-way sync *)
+
+ | Request:                                                                          
+   "\<lbrakk> tr \<in> twowayNTS; tsend \<ge> maxtime tr; Nonce n1 \<notin> used_t tr;
+      request = create_request (Crypt (shrK Br) (Key (shrK Alice)))
+                               (shrK Alice)
+                               n1 
+                               (clocktime_trace Alice tr tsend)
+    \<rbrakk>
+    \<Longrightarrow> (tsend, Says Alice Br request) # tr \<in> twowayNTS"
+
+| Response:
+   "\<lbrakk>tr \<in> twowayNTS; 
+     t3 \<ge> maxtime tr; 
+     Nonce n2 \<notin> used_t tr;
+     (t2, Gets Br request) \<in> set tr;
+     is_valid_request request;
+     request = create_request (Crypt (shrK Br) (Key requestkey)) requestkey n1 t1;
+     response = (create_response requestkey n1 n2 t2 t3)         
+    \<rbrakk>
+    \<Longrightarrow> (t3, Says Br Alice response) # tr \<in> twowayNTS"
+
+| Discipline:
+"\<lbrakk>tr \<in> twowayNTS;
+  tdisc \<ge> maxtime tr;
+  (t4, Gets Alice response) \<in> set tr;
+  response = create_response (shrK Alice) n1 n2 t2 t3;
+  request = create_request (Crypt (shrK Br) (Key (shrK Alice)))
+                           (shrK Alice) n1 (clocktime_trace Alice oldtr t1);
+  (t1, Says Alice Br request) \<in> set tr\<rbrakk> 
+         \<Longrightarrow> (tdisc, Notes Alice 
+                  (Number (encode_time (t3 - ((clocktime_trace Alice oldtr t1) 
+                           + (clocktime_trace Alice oldtr t4))/2)))) 
+            # tr \<in> twowayNTS"
+
+end
\ No newline at end of file
diff --git a/TwoWayNTS_Viability.thy b/TwoWayNTS_Viability.thy
new file mode 100644
index 0000000000000000000000000000000000000000..0e2d878d0e86ab35bce7ade1787870805783af81
--- /dev/null
+++ b/TwoWayNTS_Viability.thy
@@ -0,0 +1,194 @@
+(*  Title:  TwoWayNTS_Protocol
+
+    Author: Kristof Teichel
+
+    Copyright (C) 2019 Physikalisch-Technische Bundesanstalt Braunschweig 
+
+      The viability and executability proofs for the model of two-way NTS.
+*)
+
+theory TwoWayNTS_Viability
+  imports TwoWayNTS_Protocol
+
+begin
+
+section\<open>Viability of Two-Way NTS: 
+        Participants only say what they can synthesize\<close>
+
+txt\<open>Every piece of information required for the generation of a request message 
+    is available to the client at the time of generation.\<close>
+lemma request_viable: 
+      "\<lbrakk>tr \<in> twowayNTS; 
+        tsend \<ge> maxtime tr; 
+        Nonce n1 \<notin> used_t tr;
+        request = create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                                 (shrK Alice) n1 (clocktime Alice tsend);
+        Nonce n1 \<in> knows_t Alice tr;
+        Key (shrK Br) \<in> knows_t Alice tr;
+        nts2w_REQUEST \<in> knows_t Alice tr;
+        nts2w_RESPONSE \<in> knows_t Alice tr\<rbrakk>
+       \<Longrightarrow> request \<in> synth (analz (knows_t Alice tr))"
+  apply auto 
+  apply (smt HPair_eq_MPair analz.Inj numeral_1_eq_Suc_0 shrK_in_knows synth.Inj synth.Number 
+         synth_simps(3) synth_simps(4) synth_simps(5))
+  done
+
+txt\<open>On reception of a proper request message, the server can extract 
+    the utilized nonce and client key from it.\<close>
+lemma response_aux: 
+   "\<lbrakk>tr \<in> twowayNTS; 
+     tresp \<ge> maxtime tr; 
+     Nonce n2 \<notin> used_t tr;
+     (t2, Gets Br request) \<in> set tr;
+     is_valid_request request;
+     request = create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                              (shrK Alice) n1 t1\<rbrakk>
+    \<Longrightarrow> Nonce n1 \<in> analz (knows_t Br tr) \<and> Key (shrK Alice) \<in> analz (knows_t Br tr)"
+  using Br_honest Gets_imp_knows_t_agents HPair_def 
+  apply auto 
+    txt\<open>Goal 1\<close> apply (metis Br_honest Gets_imp_knows_t_agents MPair_analz Spy_in_bad 
+                             analz.Inj analz.Snd)
+    txt\<open>Goal 2\<close> using Br_honest Gets_imp_knows_t_agents HPair_def analz.Fst analz.Snd 
+                      analz_increasing analz_shrK_Decrypt shrK_in_knows 
+                      shrK_not_initially_lost subset_iff 
+                apply smt
+  done
+
+txt\<open>All information required for generation of a response message correlating to 
+    a given request is available to the server after reception of said request.\<close>
+lemma response_viable: 
+    "\<lbrakk>tr \<in> twowayNTS; 
+      tresp \<ge> maxtime tr; 
+      Nonce n2 \<notin> used_t tr;
+      (t2, Gets Br request) \<in> set tr;
+      is_valid_request request;
+      request = create_request (Crypt (shrK Br) (Key (shrK Alice))) 
+                               (shrK Alice) n1 t1;
+      response = (create_response (shrK Alice) n1 n2 t2 t3);     
+      Nonce n2 \<in> knows_t Br tr;
+      nts2w_REQUEST \<in> knows_t Br tr;
+      nts2w_RESPONSE \<in> knows_t Br tr \<rbrakk> 
+     \<Longrightarrow> response \<in> synth (analz (knows_t Br tr))"
+  apply auto
+  using HPair_eq_MPair shrK_in_knows synth.Inj synth.Number 
+        Gets_imp_knows_t_agents response_aux HPair_def
+  apply auto
+  apply metis apply metis apply metis
+done
+
+
+section\<open>Executability of Two-Way NTS with limited amount time context\<close>
+
+txt\<open>There exists a protocol trace where a proper request is said by the client.\<close>
+lemma twowayNTS_validrun_1: "\<exists> tr request  t1 n1 oldtr. 
+                                tr \<in> twowayNTS
+                              \<and> (t1, Says Alice Br request) \<in> set tr
+                              \<and> is_valid_request request
+                              \<and> request = create_request 
+                                            (Crypt (shrK Br) (Key (shrK Alice))) 
+                                            (shrK Alice) n1 
+                                            (clocktime_trace Alice oldtr t1)"
+  using twowayNTS.Nil twowayNTS.Request Nonce_notin_used_empty list.set_intros(1) 
+        create_request.simps maxtime_mono untimeTrace_induct_Nil One_nat_def
+  apply metis
+  done
+
+txt\<open>There exists a protocol trace in which a proper request is 
+    said by the client and received by the server.\<close>
+lemma twowayNTS_validrun_2: "\<exists>  t2 tr request t1 n1 oldtr. 
+                                tr \<in> twowayNTS
+                              \<and> (t1, Says Alice Br request) \<in> set tr
+                              \<and> is_valid_request request
+                              \<and> request = create_request 
+                                            (Crypt (shrK Br) (Key (shrK Alice))) 
+                                            (shrK Alice) n1 
+                                            (clocktime_trace Alice oldtr t1)
+                              \<and> (t2, Gets Br request) \<in> set tr
+                              \<and> (shrK Alice) = shrK Alice"
+  using twowayNTS_validrun_1 le_cases there_is_later twowayNTS.Receive 
+        maxtime_mono list.set_intros(1) list.set_intros(2) 
+  apply auto
+  using One_nat_def 
+  apply (smt list.set_intros(1) list.set_intros(2) maxtime_mono)
+  done
+
+txt\<open>There exists a protocol trace in which a proper response is said as a 
+    reaction to an existing proper request from the client.\<close>
+lemma twowayNTS_validrun_3: "\<exists> n1 n2 tr t1 t2 t3 request response oldtr.
+                               tr \<in> twowayNTS
+                             \<and> (t1, Says Alice Br request) \<in> set tr
+                             \<and> is_valid_request request
+                             \<and> request = create_request 
+                                           (Crypt (shrK Br) (Key (shrK Alice)))
+                                           (shrK Alice) n1 
+                                           (clocktime_trace Alice oldtr t1)
+                             \<and> (t3, Says Br Alice response) \<in> set tr
+                             \<and> is_valid_response response
+                             \<and> response = create_response (shrK Alice) n1 n2 t2 t3"
+  using twowayNTS_validrun_2 twowayNTS.Response
+        Nonce_supply1 there_is_later
+  apply auto
+  using list.set_intros(1)
+  apply (metis list.set_intros(2) maxtime_mono numeral_2_eq_2)
+  done
+
+txt\<open>There exists a protocol trace in which a proper response is received by the
+    client which correlates to a proper request previously said by the client.\<close>
+lemma twowayNTS_validrun_4: "\<exists> n1 n2 tr t1 t2 t3 t4 request response oldtr.
+                               tr \<in> twowayNTS
+                             \<and> request = create_request 
+                                           (Crypt (shrK Br) (Key (shrK Alice))) 
+                                           (shrK Alice) n1 
+                                           (clocktime_trace Alice oldtr t1)
+                             \<and> is_valid_request request
+                             \<and> (t1, Says Alice Br request) \<in> set tr
+                             \<and> response = create_response (shrK Alice) n1 n2 t2 t3
+                             \<and> is_valid_response response
+                             \<and> (t4, Gets Alice response) \<in> set tr"
+  using twowayNTS_validrun_3 twowayNTS.Receive there_is_later
+  apply auto 
+  using list.set_intros(1) maxtime_mono numeral_2_eq_2 twowayNTS.Receive
+        there_is_later list.set_intros(2)
+  apply metis
+  done
+
+txt\<open>There exists a protocol trace in which the client notes a measured offset as 
+    the result of an exchange of a proper request and a proper response.\<close>
+lemma twowayNTS_validrun_5: "\<exists> tdiscip offset tr.
+                               tr \<in> twowayNTS
+                             \<and> (tdiscip, Notes Alice 
+                                          (Number (encode_time offset))) \<in> set tr"
+  using twowayNTS_validrun_4 twowayNTS.Discipline 
+  apply meson
+  using there_is_later list.set_intros(1) list.set_intros(2) create_response.simps 
+        diff_add_eq_diff_diff_swap encode_decode_time insert_iff list.set(2) 
+        maxtime_mono twowayNTS.Receive
+  apply auto
+proof -
+fix tr :: "(rat \<times> event) list" and t1 :: rat and t2 :: rat and t3 :: rat and t4 :: rat and oldtr :: "(rat \<times> event) list" and t1a :: rat and n1b :: nat and n2a :: nat and t2a :: rat and t3a :: rat
+  assume a1: "\<And>tr tdisc t4 response n1 n2 t2 t3 request oldtr t1. \<lbrakk>tr \<in> twowayNTS; maxtime tr \<le> tdisc; (t4, Gets Alice Hash[Key (shrK Alice)] \<lbrace>nts2w_RESPONSE, Nonce n1, Nonce n2, Number (encode_time t2), Number (encode_time t3)\<rbrace>) \<in> set tr; response = Hash[Key (shrK Alice)] \<lbrace>nts2w_RESPONSE, Nonce n1, Nonce n2, Number (encode_time t2), Number (encode_time t3)\<rbrace>; request = Hash[Key (shrK Alice)] \<lbrace>Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n1, Number (encode_time (t1 - Offset - recent_offset Alice oldtr))\<rbrace>; (t1, Says Alice Br Hash[Key (shrK Alice)] \<lbrace>Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n1, Number (encode_time (t1 - Offset - recent_offset Alice oldtr))\<rbrace>) \<in> set tr\<rbrakk> \<Longrightarrow> (tdisc, Notes Alice (Number (encode_time (t3 - (t1 + (t4 - 2 * recent_offset Alice oldtr) - 2 * Offset) / 2)))) # tr \<in> twowayNTS"
+assume a2: "tr \<in> twowayNTS"
+  assume a3: "(t1, Says Alice Br Hash[Key (shrK Alice)] \<lbrace>Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n1b, Number (encode_time t1a)\<rbrace>) \<in> set tr"
+  assume a4: "(t4, Gets Alice Hash[Key (shrK Alice)] \<lbrace>nts2w_RESPONSE, Nonce n1b, Nonce n2a, Number (encode_time t2a), Number (encode_time t3a)\<rbrace>) \<in> set tr"
+  assume a5: "encode_time (t1 - Offset - recent_offset Alice oldtr) = encode_time t1a"
+  assume a6: "encode_time t2 = encode_time t2a"
+  assume a7: "encode_time t3 = encode_time t3a"
+have f8: "\<forall>r n ra ps rb m rc na ma rd psa. (rd, Notes Alice (Number (encode_time (rc - (rb + (ra - 2 * recent_offset Alice psa) - 2 * Offset) / 2)))) # ps \<in> twowayNTS \<or> (rb, Says Alice Br \<lbrace>Hash \<lbrace>Key (shrK Alice), Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace>, Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace>) \<notin> set ps \<or> \<lbrace>Hash \<lbrace>Key (shrK Alice), Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace>, Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace> \<noteq> m \<or> \<lbrace>Hash \<lbrace>Key (shrK Alice), nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace>, nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace> \<noteq> ma \<or> (ra, Gets Alice \<lbrace>Hash \<lbrace>Key (shrK Alice), nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace>, nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace>) \<notin> set ps \<or> \<not> maxtime ps \<le> rd \<or> ps \<notin> twowayNTS"
+  using a1 HPair_def by force
+  have f9: "(t1, Says Alice Br \<lbrace>Hash \<lbrace>Key (shrK Alice), nts2w_REQUEST, Crypt (shrK Br) (Key (shrK Alice)), Nonce n1b, Number (encode_time t1a)\<rbrace>, nts2w_REQUEST, Crypt (shrK Br) (Key (shrK Alice)), Nonce n1b, Number (encode_time t1a)\<rbrace>) \<in> set tr"
+    using a3 by (simp add: HPair_def)
+  have f10: "(t4, Gets Alice \<lbrace>Hash \<lbrace>Key (shrK Alice), Nonce (Suc 1), Nonce n1b, Nonce n2a, Number (encode_time t2), Number (encode_time t3)\<rbrace>, Nonce (Suc 1), Nonce n1b, Nonce n2a, Number (encode_time t2), Number (encode_time t3)\<rbrace>) \<in> set tr"
+    using a7 a6 a4 by (simp add: HPair_def numeral_2_eq_2)
+  have "\<forall>r n ra ps rb rc na rd psa. (rd, Notes Alice (Number (encode_time (rc - (rb - (2 * Offset - (ra - 2 * recent_offset Alice psa))) / 2)))) # ps \<in> twowayNTS \<or> (rb, Says Alice Br \<lbrace>Hash \<lbrace>Key (shrK Alice), Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace>, Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace>) \<notin> set ps \<or> (ra, Gets Alice \<lbrace>Hash \<lbrace>Key (shrK Alice), nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace>, nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace>) \<notin> set ps \<or> \<not> maxtime ps \<le> rd \<or> ps \<notin> twowayNTS"
+    using f8  diff_diff_eq2 apply auto 
+    by (smt diff_diff_eq2) 
+  then have "\<forall>r n ra ps rb rc na rd psa. (rd, Notes Alice (Number (encode_time (rc - (rb - (Offset + Offset - (ra - 2 * recent_offset Alice psa))) / 2)))) # ps \<in> twowayNTS \<or> (rb, Says Alice Br \<lbrace>Hash \<lbrace>Key (shrK Alice), Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace>, Nonce (Suc 0), Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time (rb - Offset - recent_offset Alice psa))\<rbrace>) \<notin> set ps \<or> (ra, Gets Alice \<lbrace>Hash \<lbrace>Key (shrK Alice), nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace>, nts2w_RESPONSE, Nonce n, Nonce na, Number (encode_time r), Number (encode_time rc)\<rbrace>) \<notin> set ps \<or> \<not> maxtime ps \<le> rd \<or> ps \<notin> twowayNTS"
+    by auto
+  then have "\<forall>r ra rb n rc na ps. (t1, Says Alice Br \<lbrace>Hash \<lbrace>Key (shrK Alice), nts2w_REQUEST, Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time t1a)\<rbrace>, nts2w_REQUEST, Crypt (shrK Br) (Key (shrK Alice)), Nonce n, Number (encode_time t1a)\<rbrace>) \<notin> set ps \<or> (rb, Gets Alice \<lbrace>Hash \<lbrace>Key (shrK Alice), Nonce (Suc 1), Nonce n, Nonce na, Number (encode_time ra), Number (encode_time rc)\<rbrace>, Nonce (Suc 1), Nonce n, Nonce na, Number (encode_time ra), Number (encode_time rc)\<rbrace>) \<notin> set ps \<or> (r, Notes Alice (Number (encode_time (rc - (t1 - (Offset - (rb - (Offset + 2 * recent_offset Alice oldtr)))) / 2)))) # ps \<in> twowayNTS \<or> \<not> maxtime ps \<le> r \<or> ps \<notin> twowayNTS"
+    using a5 by (simp add: diff_diff_eq2 numeral_2_eq_2)
+  then show ?thesis
+    using f10 f9 a2 by (meson list.set_intros(1) maxtime_mono mult_2_right)
+qed
+
+
+end
\ No newline at end of file