--- a/src/HOL/Auth/NS_Public.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/NS_Public.thy Tue Sep 23 15:41:33 2003 +0200
@@ -43,8 +43,9 @@
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
declare knows_Spy_partsEs [elim]
-declare analz_subset_parts [THEN subsetD, dest]
-declare Fake_parts_insert [THEN subsetD, dest]
+declare knows_Spy_partsEs [elim]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
(*A "possibility property": there are traces that reach the end*)
@@ -55,9 +56,6 @@
apply possibility
done
-
-(**** Inductive proofs about ns_public ****)
-
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
sends messages containing X! **)
@@ -70,8 +68,7 @@
"evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
-
-(*** Authenticity properties obtained from NS2 ***)
+subsection{*Authenticity properties obtained from NS2*}
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
@@ -143,8 +140,7 @@
done
-
-(*** Authenticity properties obtained from NS2 ***)
+subsection{*Authenticity properties obtained from NS2*}
(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B
[unicity of B makes Lowe's fix work]
@@ -189,8 +185,7 @@
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
by (blast intro: B_trusts_NS3_lemma)
-(*** Overall guarantee for B ***)
-
+subsection{*Overall guarantee for B*}
(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with
NA, then A initiated the run using NA.*)