--- a/src/HOL/Auth/Yahalom2.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Thu Jun 26 13:20:50 1997 +0200
@@ -25,7 +25,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX X NB K. EX evs: yahalom lost. \
-\ Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
+\ Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS
yahalom.YM4) 2);
@@ -46,7 +46,7 @@
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
by (etac yahalom.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -57,7 +57,7 @@
(** For reasoning about the encrypted portion of messages **)
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
\ X : analz (sees lost Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
qed "YM4_analz_sees_Spy";
@@ -67,7 +67,7 @@
(*Relates to both YM4 and Oops*)
goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
-\ : set_of_list evs ==> \
+\ : set evs ==> \
\ K : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
@@ -140,7 +140,7 @@
Oops as well as main secrecy property.*)
goal thy
"!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> K ~: range shrK & A ~= B";
by (etac rev_mp 1);
@@ -200,7 +200,7 @@
\ EX A' B' na' nb' X'. ALL A B na nb X. \
\ Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\ : set_of_list evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
+\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
by (etac yahalom.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (Step_tac 1);
@@ -216,10 +216,10 @@
goal thy
"!!evs. [| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says Server A' \
\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
@@ -234,8 +234,8 @@
\ ==> Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set_of_list evs --> \
-\ Says A Spy {|na, nb, Key K|} ~: set_of_list evs --> \
+\ : set evs --> \
+\ Says A Spy {|na, nb, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_sees_tac;
@@ -260,8 +260,8 @@
"!!evs. [| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set_of_list evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set_of_list evs; \
+\ : set evs; \
+\ Says A Spy {|na, nb, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -275,8 +275,8 @@
\ Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set_of_list evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set_of_list evs; \
+\ : set evs; \
+\ Says A Spy {|na, nb, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -297,7 +297,7 @@
\ ==> EX nb. Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (etac rev_mp 1);
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -317,7 +317,7 @@
\ {|Nonce NB, \
\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (etac rev_mp 1);
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -333,13 +333,13 @@
because we do not have to show that NB is secret. *)
goal thy
"!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> EX NA. Says Server A \
\ {|Nonce NB, \
\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
qed "B_trusts_YM4";
@@ -355,7 +355,7 @@
\ B ~: lost --> \
\ (EX NB. Says B Server {|Agent B, Nonce NB, \
\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
(*YM2*)
@@ -366,11 +366,11 @@
goal thy
"!!evs. evs : yahalom lost \
\ ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\ : set_of_list evs --> \
+\ : set evs --> \
\ B ~: lost --> \
\ (EX nb'. Says B Server {|Agent B, nb', \
\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by (etac yahalom.induct 1);
by (ALLGOALS Asm_simp_tac);
(*YM3*)
@@ -384,11 +384,11 @@
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
goal thy
"!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> EX nb'. Says B Server \
\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
addEs sees_Spy_partsEs) 1);
qed "YM3_auth_B_to_A";
@@ -419,7 +419,7 @@
\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \
\ : parts (sees lost Spy evs) --> \
\ B ~: lost --> \
-\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
+\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
by analz_mono_parts_induct_tac;
(*Fake*)
by (Fake_parts_insert_tac 1);
@@ -440,11 +440,10 @@
Other premises guarantee secrecy of K.*)
goal thy
"!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, \
-\ Crypt K (Nonce NB)|} : set_of_list evs; \
-\ (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} \
-\ ~: set_of_list evs); \
+\ Crypt K (Nonce NB)|} : set evs; \
+\ (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
+\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
by (dtac B_trusts_YM4_shrK 1);
by (safe_tac (!claset));