# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1666623486 -3600
# Node ID 943f99825f397168b8663fb4909710067e23186f
# Parent  3ace8ac64f20f4ef6a82abae6bb8cfe8bceb0a54
Replaced some ugly legacy proofs

diff -r 3ace8ac64f20 -r 943f99825f39 src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Sat Oct 22 21:43:26 2022 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Mon Oct 24 15:58:06 2022 +0100
@@ -63,11 +63,11 @@
 
 text \<open>It is impossible to re-use a nonce in both {term NS1} and {term NS2}, provided the nonce
   is secret.  (Honest users generate fresh nonces.)\<close>
-lemma no_nonce_NS1_NS2 [rule_format]:
-      "evs \<in> ns_public
-       \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow>
-           Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
-           Nonce NA \<in> analz (spies evs)"
+lemma no_nonce_NS1_NS2: 
+      "\<lbrakk>evs \<in> ns_public;
+        Crypt (pubEK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs);
+        Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs)\<rbrakk>  
+       \<Longrightarrow> Nonce NA \<in> analz (spies evs)"
   by (induct rule: ns_public.induct) (auto intro: analz_insertI)
 
 
@@ -107,12 +107,13 @@
 
 text \<open>Authentication for {term A}: if she receives message 2 and has used {term NA}
   to start a run, then {term B} has sent message 2.\<close>
-lemma A_trusts_NS2_lemma [rule_format]:
-   "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
-    \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow>
-        Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
-        Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
-  by (erule ns_public.induct) (auto dest: Spy_not_see_NA unique_NA)
+lemma A_trusts_NS2_lemma: 
+    "\<lbrakk>evs \<in> ns_public;            
+      Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs);
+      Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+      A \<notin> bad; B \<notin> bad\<rbrakk>
+     \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
+  by (induct rule: ns_public.induct) (auto dest: Spy_not_see_NA unique_NA)
 
 theorem A_trusts_NS2:
      "\<lbrakk>Says A  B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
@@ -123,12 +124,12 @@
 
 
 text \<open>If the encrypted message appears then it originated with Alice in {term NS1}\<close>
-lemma B_trusts_NS1 [rule_format]:
-     "evs \<in> ns_public
-      \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
-          Nonce NA \<notin> analz (spies evs) \<longrightarrow>
-          Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
-  by (induction evs rule: ns_public.induct) (use analz_insertI in auto)
+lemma B_trusts_NS1:
+     "\<lbrakk>evs \<in> ns_public;                                     
+       Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs);
+       Nonce NA \<notin> analz (spies evs)\<rbrakk>
+      \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+  by (induct evs rule: ns_public.induct) (use analz_insertI in \<open>auto split: if_split_asm\<close>)
 
 
 subsection \<open>Authenticity properties obtained from {term NS2}\<close>
@@ -165,7 +166,7 @@
 
 text \<open>Authentication for {term B}: if he receives message 3 and has used {term NB}
   in message 2, then {term A} has sent message 3.\<close>
-lemma B_trusts_NS3_lemma [rule_format]:
+lemma B_trusts_NS3_lemma:
      "\<lbrakk>evs \<in> ns_public;
        Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs);
        Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
diff -r 3ace8ac64f20 -r 943f99825f39 src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Sat Oct 22 21:43:26 2022 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Mon Oct 24 15:58:06 2022 +0100
@@ -63,11 +63,11 @@
 
 text \<open>It is impossible to re-use a nonce in both {term NS1} and {term NS2}, provided the nonce
   is secret.  (Honest users generate fresh nonces.)\<close>
-lemma no_nonce_NS1_NS2 [rule_format]: 
-      "evs \<in> ns_public 
-       \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
-           Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>  
-           Nonce NA \<in> analz (spies evs)"
+lemma no_nonce_NS1_NS2: 
+      "\<lbrakk>evs \<in> ns_public;
+        Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs);
+        Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs)\<rbrakk>  
+       \<Longrightarrow> Nonce NA \<in> analz (spies evs)"
   by (induct rule: ns_public.induct) (auto intro: analz_insertI)
 
 
@@ -107,12 +107,13 @@
 
 text \<open>Authentication for {term A}: if she receives message 2 and has used {term NA}
   to start a run, then {term B} has sent message 2.\<close>
-lemma A_trusts_NS2_lemma [rule_format]: 
-   "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
-    \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
-        Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
-        Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
-  by (erule ns_public.induct) (auto dest: Spy_not_see_NA unique_NA)
+lemma A_trusts_NS2_lemma: 
+    "\<lbrakk>evs \<in> ns_public;            
+      Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs);
+      Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+      A \<notin> bad; B \<notin> bad\<rbrakk>
+     \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
+  by (induct rule: ns_public.induct) (auto dest: Spy_not_see_NA unique_NA)
 
 theorem A_trusts_NS2: 
      "\<lbrakk>Says A  B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;   
@@ -123,12 +124,12 @@
 
 
 text \<open>If the encrypted message appears then it originated with Alice in {term NS1}\<close>
-lemma B_trusts_NS1 [rule_format]:
-     "evs \<in> ns_public                                         
-      \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
-          Nonce NA \<notin> analz (spies evs) \<longrightarrow>
-          Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
-  by (induction evs rule: ns_public.induct) (use analz_insertI in auto)
+lemma B_trusts_NS1:
+     "\<lbrakk>evs \<in> ns_public;                                     
+       Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs);
+       Nonce NA \<notin> analz (spies evs)\<rbrakk>
+      \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+  by (induct evs rule: ns_public.induct) (use analz_insertI in \<open>auto split: if_split_asm\<close>)
 
 
 subsection \<open>Authenticity properties obtained from {term NS2}\<close>
@@ -166,7 +167,7 @@
 
 text \<open>Authentication for {term B}: if he receives message 3 and has used {term NB}
   in message 2, then {term A} has sent message 3 (to somebody) \<close>
-lemma B_trusts_NS3_lemma [rule_format]:
+lemma B_trusts_NS3_lemma:
      "\<lbrakk>evs \<in> ns_public; 
        Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs); 
        Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;