--- a/src/HOL/Auth/NS_Public.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Thu Jun 26 13:20:50 1997 +0200
@@ -21,7 +21,7 @@
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. A ~= B ==> EX NB. EX evs: ns_public. \
-\ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
+\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
by possibility_tac;
@@ -31,7 +31,7 @@
(**** Inductive proofs about ns_public ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
by (etac ns_public.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -134,7 +134,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
goal thy
- "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; \
+ "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NA ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
@@ -157,12 +157,12 @@
(*Authentication for A: if she receives message 2 and has used NA
to start a run, then B has sent message 2.*)
goal thy
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
+ "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set_of_list evs;\
+\ : set evs;\
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set_of_list evs";
+\ : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
@@ -181,7 +181,7 @@
"!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
\ Nonce NA ~: analz (sees lost Spy evs); \
\ evs : ns_public |] \
-\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
+\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (analz_induct_tac 1);
@@ -237,7 +237,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set_of_list evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NB ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
@@ -262,10 +262,10 @@
in message 2, then A has sent message 3.*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set_of_list evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \
+\ : set evs; \
+\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
+\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK B) NB : parts H*)
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
@@ -294,10 +294,10 @@
NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set_of_list evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \
+\ : set evs; \
+\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
+\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
--- a/src/HOL/Auth/NS_Public.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy Thu Jun 26 13:20:50 1997 +0200
@@ -32,16 +32,15 @@
(*Bob responds to Alice's message with a further nonce*)
NS2 "[| evs: ns_public; A ~= B; Nonce NB ~: used evs;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
- : set_of_list evs |]
+ : set evs |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
# evs : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
- : set_of_list evs;
+ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
- : set_of_list evs |]
+ : set evs |]
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
(**Oops message??**)
--- a/src/HOL/Auth/NS_Public_Bad.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Jun 26 13:20:50 1997 +0200
@@ -25,7 +25,7 @@
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. A ~= B ==> EX NB. EX evs: ns_public. \
-\ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
+\ Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
by possibility_tac;
@@ -35,7 +35,7 @@
(**** Inductive proofs about ns_public ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
by (etac ns_public.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -139,7 +139,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
goal thy
- "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; \
+ "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NA ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
@@ -162,10 +162,10 @@
(*Authentication for A: if she receives message 2 and has used NA
to start a run, then B has sent message 2.*)
goal thy
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
-\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs;\
+ "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
+\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;\
\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs";
+\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
@@ -188,7 +188,7 @@
"!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
\ Nonce NA ~: analz (sees lost Spy evs); \
\ evs : ns_public |] \
-\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
+\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (analz_induct_tac 1);
@@ -240,8 +240,8 @@
(*NB remains secret PROVIDED Alice never responds with round 3*)
goal thy
- "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs;\
-\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs); \
+ "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;\
+\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs); \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NB ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
@@ -270,10 +270,10 @@
in message 2, then A has sent message 3--to somebody....*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \
-\ : set_of_list evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \
+\ : set evs; \
+\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs";
+\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK B) NB : parts H*)
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
@@ -295,7 +295,7 @@
(*Can we strengthen the secrecy theorem? NO*)
goal thy
"!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \
+\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
\ --> Nonce NB ~: analz (sees lost Spy evs)";
by (analz_induct_tac 1);
(*NS1*)
@@ -321,14 +321,14 @@
Level 9
!!evs. [| A ~: lost; B ~: lost; evs : ns_public |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
- : set_of_list evs -->
+ : set evs -->
Nonce NB ~: analz (sees lost Spy evs)
1. !!evs Aa Ba B' NAa NBa evsa.
[| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa;
- Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set_of_list evsa;
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
+ Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set evsa;
Ba : lost;
- Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa;
+ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
Nonce NB ~: analz (sees lost Spy evsa) |]
==> False
*)
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Jun 26 13:20:50 1997 +0200
@@ -35,17 +35,14 @@
(*Bob responds to Alice's message with a further nonce*)
NS2 "[| evs: ns_public; A ~= B; Nonce NB ~: used evs;
- Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
- : set_of_list evs |]
+ Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
# evs : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
- : set_of_list evs;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
- : set_of_list evs |]
+ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
(**Oops message??**)
--- a/src/HOL/Auth/NS_Shared.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Thu Jun 26 13:20:50 1997 +0200
@@ -23,7 +23,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX N K. EX evs: ns_shared lost. \
-\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list evs";
+\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS
ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
@@ -44,7 +44,7 @@
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
by (etac ns_shared.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -52,13 +52,13 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
(*For reasoning about the encrypted portion of message NS3*)
-goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
+goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
\ ==> X : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "NS3_msg_in_parts_sees_Spy";
goal thy
- "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
+ "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
\ ==> K : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
@@ -128,7 +128,7 @@
(*Describes the form of K, X and K' when the Server sends this message.*)
goal thy
"!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : ns_shared lost |] \
\ ==> K ~: range shrK & \
\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \
@@ -148,7 +148,7 @@
\ Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|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);
@@ -161,7 +161,7 @@
Use Says_Server_message_form if applicable.*)
goal thy
"!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
-\ : set_of_list evs; evs : ns_shared lost |] \
+\ : set evs; evs : ns_shared lost |] \
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
\ | X : analz (sees lost Spy evs)";
by (case_tac "A : lost" 1);
@@ -242,7 +242,7 @@
"!!evs. evs : ns_shared lost ==> \
\ EX A' NA' B' X'. ALL A NA B X. \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
+\ : set evs --> A=A' & NA=NA' & B=B' & X=X'";
by (etac ns_shared.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (Step_tac 1);
@@ -260,10 +260,10 @@
goal thy
"!!evs. [| Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says Server A' \
\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -276,8 +276,8 @@
\ ==> Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
-\ : set_of_list evs --> \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
+\ : set evs --> \
+\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac ns_shared.induct 1);
by analz_sees_tac;
@@ -308,8 +308,8 @@
(*Final version: Server's message in the most abstract form*)
goal thy
"!!evs. [| Says Server A \
-\ (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs; \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs); \
+\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
+\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
\ A ~: lost; B ~: lost; evs : ns_shared lost \
\ |] ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -320,8 +320,8 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server A \
-\ (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs; \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs); \
+\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
+\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -344,7 +344,7 @@
\ ==> EX NA. Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|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);
@@ -357,9 +357,9 @@
"!!evs. [| B ~: lost; evs : ns_shared lost |] \
\ ==> Key K ~: analz (sees lost Spy evs) --> \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set_of_list evs --> \
+\ : set evs --> \
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
-\ Says B A (Crypt K (Nonce NB)) : set_of_list evs";
+\ Says B A (Crypt K (Nonce NB)) : set evs";
by (etac ns_shared.induct 1);
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
@@ -390,10 +390,10 @@
goal thy
"!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs); \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set_of_list evs; \
-\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \
+\ : set evs; \
+\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
-\ ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
+\ ==> Says B A (Crypt K (Nonce NB)) : set evs";
by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
qed "A_trusts_NS4";
--- a/src/HOL/Auth/NS_Shared.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Thu Jun 26 13:20:50 1997 +0200
@@ -35,7 +35,7 @@
Server doesn't know who the true sender is, hence the A' in
the sender field.*)
NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; Key KAB ~: used evs;
- Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
+ Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
==> Says Server A
(Crypt (shrK A)
{|Nonce NA, Agent B, Key KAB,
@@ -46,14 +46,14 @@
Can inductively show A ~= Server*)
NS3 "[| evs: ns_shared lost; A ~= B;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set_of_list evs;
- Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
+ : set evs;
+ Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
==> Says A B X # evs : ns_shared lost"
(*Bob's nonce exchange. He does not know who the message came
from, but responds to A because she is mentioned inside.*)
NS4 "[| evs: ns_shared lost; A ~= B; Nonce NB ~: used evs;
- Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
+ Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
==> Says B A (Crypt K (Nonce NB)) # evs
: ns_shared lost"
@@ -63,18 +63,18 @@
Letting the Spy add or subtract 1 lets him send ALL nonces.
Instead we distinguish the messages by sending the nonce twice.*)
NS5 "[| evs: ns_shared lost; A ~= B;
- Says B' A (Crypt K (Nonce NB)) : set_of_list evs;
+ Says B' A (Crypt K (Nonce NB)) : set evs;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set_of_list evs |]
+ : set evs |]
==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
(*This message models possible leaks of session keys.
The two Nonces identify the protocol run: the rule insists upon
the true senders in order to make them accurate.*)
Oops "[| evs: ns_shared lost; A ~= Spy;
- Says B A (Crypt K (Nonce NB)) : set_of_list evs;
+ Says B A (Crypt K (Nonce NB)) : set evs;
Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set_of_list evs |]
+ : set evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
end
--- a/src/HOL/Auth/OtwayRees.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu Jun 26 13:20:50 1997 +0200
@@ -26,7 +26,7 @@
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway lost. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
by possibility_tac;
@@ -45,7 +45,7 @@
qed "otway_mono";
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -55,17 +55,17 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
+goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
\ ==> X : analz (sees lost Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
-goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
\ ==> X : analz (sees lost Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
-goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
+goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
\ ==> K : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
@@ -150,7 +150,7 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \
+\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ evs : otway lost |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
@@ -212,7 +212,7 @@
goal thy
"!!evs. evs : otway lost ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
+\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -229,9 +229,9 @@
goal thy
"!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -247,7 +247,7 @@
\ : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set_of_list evs";
+\ : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
qed_spec_mp "Crypt_imp_OR1";
@@ -300,12 +300,12 @@
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set_of_list evs --> \
+\ : set evs --> \
\ (EX NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
@@ -335,16 +335,16 @@
Spy_not_see_encrypted_key*)
goal thy
"!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ A ~: lost; A ~= Spy; evs : otway lost |] \
\ ==> EX NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
addEs sees_Spy_partsEs) 1);
qed "A_trusts_OR4";
@@ -358,8 +358,8 @@
"!!evs. [| A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -382,8 +382,8 @@
goal thy
"!!evs. [| Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -395,8 +395,8 @@
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -417,7 +417,7 @@
\ (EX X. Says B Server \
\ {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
@@ -458,11 +458,11 @@
\ --> (ALL X'. Says B Server \
\ {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
-\ : set_of_list evs \
+\ : set evs \
\ --> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
@@ -486,15 +486,15 @@
goal thy
"!!evs. [| B ~: lost; B ~= Spy; evs : otway lost; \
\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\ : set_of_list evs |] \
+\ : set evs |] \
\ ==> Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
addSEs sees_Spy_partsEs) 1);
qed "B_trusts_OR3";
@@ -507,10 +507,10 @@
"!!evs. [| B ~: lost; evs : otway lost |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
\ (EX X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\ : set_of_list evs)";
+\ : set evs)";
by (etac otway.induct 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
@@ -524,14 +524,14 @@
strictly necessary for authentication.*)
goal thy
"!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost |] \
\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
-\ : set_of_list evs";
+\ : set evs";
by (blast_tac (!claset addSDs [A_trusts_OR4]
addSEs [OR3_imp_OR2]) 1);
qed "A_auths_B";
--- a/src/HOL/Auth/OtwayRees.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Thu Jun 26 13:20:50 1997 +0200
@@ -37,7 +37,7 @@
the sender is, hence the A' in the sender field.
Note that NB is encrypted.*)
OR2 "[| evs: otway lost; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
+ Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
@@ -52,7 +52,7 @@
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says Server B
{|Nonce NA,
Crypt (shrK A) {|Nonce NA, Key KAB|},
@@ -65,16 +65,16 @@
Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
- : set_of_list evs;
+ : set evs;
Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says B A {|Nonce NA, X|} # evs : otway lost"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
Oops "[| evs: otway lost; B ~= Spy;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
end
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Jun 26 13:20:50 1997 +0200
@@ -23,7 +23,7 @@
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway lost. \
\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
-\ : set_of_list evs";
+\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
by possibility_tac;
@@ -42,7 +42,7 @@
qed "otway_mono";
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -52,13 +52,13 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
\ X : analz (sees lost Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
-\ : set_of_list evs ==> K : parts (sees lost Spy evs)";
+\ : set evs ==> K : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
@@ -139,7 +139,7 @@
"!!evs. [| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : otway lost |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
@@ -202,7 +202,7 @@
\ EX A' B' NA' NB'. ALL A B NA NB. \
\ Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs \
\ --> A=A' & B=B' & NA=NA' & NB=NB'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -222,11 +222,11 @@
"!!evs. [| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says Server B' \
\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \
\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : otway lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
@@ -244,7 +244,7 @@
\ --> (EX NB. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -257,12 +257,12 @@
Freshness may be inferred from nonce NA.*)
goal thy
"!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
-\ : set_of_list evs; \
+\ : set evs; \
\ A ~: lost; evs : otway lost |] \
\ ==> EX NB. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
addEs sees_Spy_partsEs) 1);
qed "A_trusts_OR4";
@@ -277,8 +277,8 @@
\ ==> Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
+\ : set evs --> \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -302,8 +302,8 @@
"!!evs. [| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \
+\ : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -316,8 +316,8 @@
\ Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \
+\ : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -337,7 +337,7 @@
\ --> (EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -351,11 +351,11 @@
goal thy
"!!evs. [| B ~: lost; evs : otway lost; \
\ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs |] \
+\ : set evs |] \
\ ==> EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
addEs sees_Spy_partsEs) 1);
qed "B_trusts_OR3";
--- a/src/HOL/Auth/OtwayRees_AN.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Jun 26 13:20:50 1997 +0200
@@ -39,7 +39,7 @@
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
OR2 "[| evs: otway lost; B ~= Server;
- Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
+ Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
# evs : otway lost"
@@ -47,7 +47,7 @@
session key to Bob with a packet for forwarding to Alice.*)
OR3 "[| evs: otway lost; B ~= Server; A ~= B; Key KAB ~: used evs;
Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- : set_of_list evs |]
+ : set evs |]
==> Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
@@ -57,9 +57,9 @@
those in the message he previously sent the Server.*)
OR4 "[| evs: otway lost; A ~= B;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- : set_of_list evs;
+ : set evs;
Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says B A X # evs : otway lost"
(*This message models possible leaks of session keys. The nonces
@@ -68,7 +68,7 @@
Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
end
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Jun 26 13:20:50 1997 +0200
@@ -29,7 +29,7 @@
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
by possibility_tac;
@@ -39,7 +39,7 @@
(**** Inductive proofs about otway ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -49,17 +49,17 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
+goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
\ X : analz (sees lost Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
-goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
\ X : analz (sees lost Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
-goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
+goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
\ ==> K : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
@@ -140,7 +140,7 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \
+\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ evs : otway |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
@@ -201,7 +201,7 @@
goal thy
"!!evs. evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
+\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -218,9 +218,9 @@
goal thy
"!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -231,8 +231,8 @@
"!!evs. [| A ~: lost; B ~: lost; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -255,8 +255,8 @@
goal thy
"!!evs. [| Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -276,7 +276,7 @@
\ : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set_of_list evs";
+\ : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -292,12 +292,12 @@
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set_of_list evs --> \
+\ : set evs --> \
\ (EX B NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
@@ -317,11 +317,11 @@
{|Nonce NAa, Agent Aa, Agent A,
Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
- : set_of_list evsa;
+ : set evsa;
Says A B
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
- : set_of_list evsa
+ : set evsa
*)
writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
--- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Jun 26 13:20:50 1997 +0200
@@ -36,7 +36,7 @@
the sender is, hence the A' in the sender field.
We modify the published protocol by NOT encrypting NB.*)
OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
+ Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X, Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
@@ -51,7 +51,7 @@
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says Server B
{|Nonce NA,
Crypt (shrK A) {|Nonce NA, Key KAB|},
@@ -62,16 +62,16 @@
those in the message he previously sent the Server.*)
OR4 "[| evs: otway; A ~= B;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
- : set_of_list evs;
+ : set evs;
Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says B A {|Nonce NA, X|} # evs : otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
Oops "[| evs: otway; B ~= Spy;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
end
--- a/src/HOL/Auth/Public.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Public.ML Thu Jun 26 13:20:50 1997 +0200
@@ -119,7 +119,7 @@
setloop split_tac [expand_if]))));
qed "UN_parts_sees_Says";
-goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
+goal thy "Says A B X : set evs --> X : sees lost Spy evs";
by (list.induct_tac "evs" 1);
by (Auto_tac ());
qed_spec_mp "Says_imp_sees_Spy";
--- a/src/HOL/Auth/Recur.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Thu Jun 26 13:20:50 1997 +0200
@@ -25,7 +25,7 @@
\ ==> EX K NA. EX evs: recur lost. \
\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
\ Agent Server|} \
-\ : set_of_list evs";
+\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS
(respond.One RSN (4,recur.RA3))) 2);
@@ -39,7 +39,7 @@
\ ==> EX K. EX NA. EX evs: recur lost. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} \
-\ : set_of_list evs";
+\ : set evs";
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -59,7 +59,7 @@
\ ==> EX K. EX NA. EX evs: recur lost. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} \
-\ : set_of_list evs";
+\ : set evs";
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -87,7 +87,7 @@
qed "recur_mono";
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs";
by (etac recur.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -126,7 +126,7 @@
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
-goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set_of_list evs \
+goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
\ ==> RA : analz (sees lost Spy evs)";
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "RA4_analz_sees_Spy";
@@ -382,7 +382,7 @@
goal thy
"!!evs. evs : recur lost \
\ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
-\ ~: set_of_list evs";
+\ ~: set evs";
by (etac recur.induct 1);
by (etac (respond.induct) 5);
by (Auto_tac());
@@ -530,7 +530,7 @@
\ : parts (sees lost Spy evs); \
\ A ~: lost; evs : recur lost |] \
\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \
-\ : set_of_list evs";
+\ : set evs";
by (etac rev_mp 1);
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -547,7 +547,7 @@
goal thy
"!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs); \
\ A ~: lost; A ~= Spy; evs : recur lost |] \
-\ ==> EX C RC. Says Server C RC : set_of_list evs & \
+\ ==> EX C RC. Says Server C RC : set evs & \
\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
by parts_induct_tac;
--- a/src/HOL/Auth/Recur.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Recur.thy Thu Jun 26 13:20:50 1997 +0200
@@ -75,14 +75,14 @@
NOTE: existing proofs don't need PA and are complicated by its
presence! See parts_Fake_tac.*)
RA2 "[| evs: recur lost; B ~= C; B ~= Server; Nonce NB ~: used evs;
- Says A' B PA : set_of_list evs;
+ Says A' B PA : set evs;
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
# evs : recur lost"
(*The Server receives Bob's message and prepares a response.*)
RA3 "[| evs: recur lost; B ~= Server;
- Says B' Server PB : set_of_list evs;
+ Says B' Server PB : set evs;
(PB,RB,K) : respond evs |]
==> Says Server B RB # evs : recur lost"
@@ -91,11 +91,11 @@
RA4 "[| evs: recur lost; A ~= B;
Says B C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|}
- : set_of_list evs;
+ : set evs;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
RA|}
- : set_of_list evs |]
+ : set evs |]
==> Says B A RA # evs : recur lost"
(**No "oops" message can readily be expressed, since each session key is
--- a/src/HOL/Auth/Shared.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Thu Jun 26 13:20:50 1997 +0200
@@ -138,7 +138,7 @@
setloop split_tac [expand_if]))));
qed "UN_parts_sees_Says";
-goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
+goal thy "Says A B X : set evs --> X : sees lost Spy evs";
by (list.induct_tac "evs" 1);
by (Auto_tac ());
qed_spec_mp "Says_imp_sees_Spy";
--- a/src/HOL/Auth/WooLam.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML Thu Jun 26 13:20:50 1997 +0200
@@ -22,7 +22,7 @@
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX NB. EX evs: woolam. \
\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
-\ : set_of_list evs";
+\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS
woolam.WL4 RS woolam.WL5) 2);
@@ -35,7 +35,7 @@
(**** Inductive proofs about woolam ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
by (etac woolam.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -45,7 +45,7 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B X : set_of_list evs \
+goal thy "!!evs. Says A' B X : set evs \
\ ==> X : analz (sees lost Spy evs)";
by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
qed "WL4_analz_sees_Spy";
@@ -97,7 +97,7 @@
goal thy
"!!evs. [| A ~: lost; evs : woolam |] \
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) \
-\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
+\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -109,8 +109,8 @@
goal thy
"!!evs. [| A ~: lost; evs : woolam; \
\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
-\ : set_of_list evs |] \
-\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
+\ : set evs |] \
+\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
addSEs [MPair_parts]
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -122,9 +122,9 @@
(*Server sent WL5 only if it received the right sort of message*)
goal thy
"!!evs. evs : woolam ==> \
-\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs \
+\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs \
\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
-\ : set_of_list evs)";
+\ : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
@@ -135,7 +135,7 @@
goal thy
"!!evs. [| B ~: lost; evs : woolam |] \
\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \
-\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
+\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -143,9 +143,9 @@
(*Partial guarantee for B: if it gets a message of correct form then the Server
sent the same message.*)
goal thy
- "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
+ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
\ B ~: lost; evs : woolam |] \
-\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
+\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "B_got_WL5";
@@ -155,9 +155,9 @@
But A may have sent the nonce to some other agent and it could have reached
the Server via the Spy.*)
goal thy
- "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
+ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
\ A ~: lost; B ~: lost; evs : woolam |] \
-\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
+\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (blast_tac (!claset addIs [Server_trusts_WL4]
addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
qed "B_trusts_WL5";
@@ -166,8 +166,8 @@
(*B only issues challenges in response to WL1. Useful??*)
goal thy
"!!evs. [| B ~= Spy; evs : woolam |] \
-\ ==> Says B A (Nonce NB) : set_of_list evs \
-\ --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
+\ ==> Says B A (Nonce NB) : set evs \
+\ --> (EX A'. Says A' B (Agent A) : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
@@ -178,8 +178,8 @@
goal thy
"!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) & \
-\ Says B A (Nonce NB) : set_of_list evs \
-\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
+\ Says B A (Nonce NB) : set evs \
+\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (Step_tac 1);
--- a/src/HOL/Auth/WooLam.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy Thu Jun 26 13:20:50 1997 +0200
@@ -36,27 +36,27 @@
(*Bob responds to Alice's message with a challenge.*)
WL2 "[| evs: woolam; A ~= B;
- Says A' B (Agent A) : set_of_list evs |]
+ Says A' B (Agent A) : set evs |]
==> Says B A (Nonce NB) # evs : woolam"
(*Alice responds to Bob's challenge by encrypting NB with her key.
B is *not* properly determined -- Alice essentially broadcasts
her reply.*)
WL3 "[| evs: woolam; A ~= B;
- Says A B (Agent A) : set_of_list evs;
- Says B' A (Nonce NB) : set_of_list evs |]
+ Says A B (Agent A) : set evs;
+ Says B' A (Nonce NB) : set evs |]
==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
(*Bob forwards Alice's response to the Server.*)
WL4 "[| evs: woolam; B ~= Server;
- Says A' B X : set_of_list evs;
- Says A'' B (Agent A) : set_of_list evs |]
+ Says A' B X : set evs;
+ Says A'' B (Agent A) : set evs |]
==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
(*Server decrypts Alice's response for Bob.*)
WL5 "[| evs: woolam; B ~= Server;
Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
- : set_of_list evs |]
+ : set evs |]
==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
# evs : woolam"
--- a/src/HOL/Auth/Yahalom.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML Thu Jun 26 13:20:50 1997 +0200
@@ -24,7 +24,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);
@@ -45,7 +45,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";
@@ -56,7 +56,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 {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|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";
@@ -66,7 +66,7 @@
(*Relates to both YM4 and Oops*)
goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, 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 {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> K ~: range shrK";
by (etac rev_mp 1);
@@ -199,7 +199,7 @@
\ EX A' B' na' nb' X'. ALL A B na nb X. \
\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, 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 \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says Server A' \
\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
@@ -233,8 +233,8 @@
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : 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;
@@ -259,8 +259,8 @@
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : 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);
@@ -274,8 +274,8 @@
\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : 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);
@@ -309,7 +309,7 @@
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (etac rev_mp 1);
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -327,7 +327,7 @@
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (etac rev_mp 1);
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -346,7 +346,7 @@
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set_of_list evs)";
+\ : set evs)";
by analz_mono_parts_induct_tac;
(*YM3 & Fake*)
by (Blast_tac 2);
@@ -368,7 +368,7 @@
goalw thy [KeyWithNonce_def]
"!!evs. Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
-\ : set_of_list evs ==> KeyWithNonce K NB evs";
+\ : set evs ==> KeyWithNonce K NB evs";
by (Blast_tac 1);
qed "KeyWithNonceI";
@@ -394,7 +394,7 @@
goalw thy [KeyWithNonce_def]
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ NB ~= NB'; evs : yahalom lost |] \
\ ==> ~ KeyWithNonce K NB evs";
by (blast_tac (!claset addDs [unique_session_keys]) 1);
@@ -453,7 +453,7 @@
goal thy
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ NB ~= NB'; KAB ~: range shrK; evs : yahalom lost |] \
\ ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) = \
\ (Nonce NB : analz (sees lost Spy evs))";
@@ -495,9 +495,9 @@
not_lost_tac to remove the assumption B' ~: lost.*)
goal thy
"!!evs.[| Says C D {|X, Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
-\ : set_of_list evs; B ~: lost; \
+\ : set evs; B ~: lost; \
\ Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ NB ~: analz (sees lost Spy evs); evs : yahalom lost |] \
\ ==> NA' = NA & A' = A & B' = B";
by (not_lost_tac "B'" 1);
@@ -528,11 +528,11 @@
(*The Server sends YM3 only in response to YM2.*)
goal thy
"!!evs. [| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
+\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
\ evs : yahalom lost |] \
\ ==> EX B'. Says B' Server \
\ {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
-\ : set_of_list evs";
+\ : set evs";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
by (ALLGOALS Asm_simp_tac);
@@ -546,8 +546,8 @@
"!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ : set_of_list evs --> \
-\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) --> \
+\ : set evs --> \
+\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) --> \
\ Nonce NB ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_sees_tac;
@@ -606,16 +606,16 @@
goal thy
"!!evs. [| Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} : set_of_list evs; \
-\ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
+\ Crypt K (Nonce NB)|} : set evs; \
+\ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
dtac B_trusts_YM4_shrK 1);
@@ -638,7 +638,7 @@
\ B ~: lost --> \
\ Says B Server {|Agent B, \
\ Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ : set_of_list evs";
+\ : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
@@ -647,11 +647,11 @@
goal thy
"!!evs. evs : yahalom lost \
\ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\ : set_of_list evs --> \
+\ : set evs --> \
\ B ~: lost --> \
\ Says B Server {|Agent B, \
\ Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ : set_of_list evs";
+\ : set evs";
by (etac yahalom.induct 1);
by (ALLGOALS Asm_simp_tac);
(*YM4*)
@@ -664,10 +664,10 @@
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
goal thy
"!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ : 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";
@@ -698,7 +698,7 @@
\ Crypt (shrK B) {|Agent A, Key K|} \
\ : 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);
@@ -720,13 +720,13 @@
goal thy
"!!evs. [| Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ : set_of_list evs; \
+\ : set evs; \
\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} : set_of_list evs; \
+\ Crypt K (Nonce NB)|} : set evs; \
\ (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} \
-\ ~: set_of_list evs); \
+\ ~: set evs); \
\ A ~: lost; B ~: lost; Spy: 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 (dtac B_trusts_YM4 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
--- a/src/HOL/Auth/Yahalom.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy Thu Jun 26 13:20:50 1997 +0200
@@ -32,7 +32,7 @@
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
+ Says A' B {|Agent A, Nonce NA|} : set evs |]
==> Says B Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
# evs : yahalom lost"
@@ -42,7 +42,7 @@
YM3 "[| evs: yahalom lost; A ~= Server; Key KAB ~: used evs;
Says B' Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says Server A
{|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
Crypt (shrK B) {|Agent A, Key KAB|}|}
@@ -52,8 +52,8 @@
uses the new session key to send Bob his Nonce.*)
YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
- X|} : set_of_list evs;
- Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
+ X|} : set evs;
+ Says A B {|Agent A, Nonce NA|} : set evs |]
==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
(*This message models possible leaks of session keys. The Nonces
@@ -62,7 +62,7 @@
Oops "[| evs: yahalom lost; A ~= Spy;
Says Server A {|Crypt (shrK A)
{|Agent B, Key K, Nonce NA, Nonce NB|},
- X|} : set_of_list evs |]
+ X|} : set evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
@@ -71,6 +71,6 @@
"KeyWithNonce K NB evs ==
EX A B na X.
Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
- : set_of_list evs"
+ : set evs"
end
--- 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));
--- a/src/HOL/Auth/Yahalom2.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Thu Jun 26 13:20:50 1997 +0200
@@ -35,7 +35,7 @@
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
+ Says A' B {|Agent A, Nonce NA|} : set evs |]
==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
# evs : yahalom lost"
@@ -46,7 +46,7 @@
YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs;
Says B' Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says Server A
{|Nonce NB,
Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
@@ -58,8 +58,8 @@
YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|}
- : set_of_list evs;
- Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
+ : set evs;
+ Says A B {|Agent A, Nonce NA|} : set evs |]
==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
(*This message models possible leaks of session keys. The nonces
@@ -68,7 +68,7 @@
Oops "[| evs: yahalom lost; A ~= Spy;
Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} : set_of_list evs |]
+ X|} : set evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
end
--- a/src/HOL/List.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/List.ML Thu Jun 26 13:20:50 1997 +0200
@@ -112,7 +112,7 @@
(** map **)
goal thy
- "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
+ "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
@@ -170,38 +170,38 @@
qed "mem_filter";
Addsimps[mem_filter];
-(** set_of_list **)
+(** set **)
-goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
+goal thy "set (xs@ys) = (set xs Un set ys)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "set_of_list_append";
Addsimps[set_of_list_append];
-goal thy "(x mem xs) = (x: set_of_list xs)";
+goal thy "(x mem xs) = (x: set xs)";
by (induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
by (Blast_tac 1);
qed "set_of_list_mem_eq";
-goal thy "set_of_list l <= set_of_list (x#l)";
+goal thy "set l <= set (x#l)";
by (Simp_tac 1);
by (Blast_tac 1);
qed "set_of_list_subset_Cons";
-goal thy "(set_of_list xs = {}) = (xs = [])";
+goal thy "(set xs = {}) = (xs = [])";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "set_of_list_empty";
Addsimps [set_of_list_empty];
-goal thy "set_of_list(rev xs) = set_of_list(xs)";
+goal thy "set(rev xs) = set(xs)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "set_of_list_rev";
Addsimps [set_of_list_rev];
-goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
+goal thy "set(map f xs) = f``(set xs)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "set_of_list_map";
@@ -483,7 +483,7 @@
(** takeWhile & dropWhile **)
goal thy
- "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
+ "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
@@ -492,7 +492,7 @@
Addsimps [takeWhile_append1];
goal thy
- "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
+ "(!x:set xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
@@ -500,7 +500,7 @@
Addsimps [takeWhile_append2];
goal thy
- "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
+ "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
@@ -509,14 +509,14 @@
Addsimps [dropWhile_append1];
goal thy
- "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
+ "(!x:set xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
bind_thm("dropWhile_append2", ballI RS (result() RS mp));
Addsimps [dropWhile_append2];
-goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
+goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
--- a/src/HOL/List.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/List.thy Thu Jun 26 13:20:50 1997 +0200
@@ -16,7 +16,7 @@
concat :: 'a list list => 'a list
foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
hd :: 'a list => 'a
- set_of_list :: 'a list => 'a set
+ set :: 'a list => 'a set
list_all :: ('a => bool) => ('a list => bool)
map :: ('a=>'b) => ('a list => 'b list)
mem :: ['a, 'a list] => bool (infixl 55)
@@ -70,9 +70,9 @@
primrec "op mem" list
"x mem [] = False"
"x mem (y#ys) = (if y=x then True else x mem ys)"
-primrec set_of_list list
- "set_of_list [] = {}"
- "set_of_list (x#xs) = insert x (set_of_list xs)"
+primrec set list
+ "set [] = {}"
+ "set (x#xs) = insert x (set xs)"
primrec list_all list
list_all_Nil "list_all P [] = True"
list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
--- a/src/HOL/ex/InSort.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/ex/InSort.ML Thu Jun 26 13:20:50 1997 +0200
@@ -18,7 +18,7 @@
by (ALLGOALS Asm_simp_tac);
qed "insort_permutes";
-goal thy "set_of_list(ins f x xs) = insert x (set_of_list xs)";
+goal thy "set(ins f x xs) = insert x (set xs)";
by (asm_simp_tac (!simpset addsimps [set_of_list_via_mset]
setloop (split_tac [expand_if])) 1);
by (Fast_tac 1);
--- a/src/HOL/ex/Qsort.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/ex/Qsort.ML Thu Jun 26 13:20:50 1997 +0200
@@ -29,13 +29,13 @@
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "qsort_permutes";
-goal Qsort.thy "set_of_list(qsort le xs) = set_of_list xs";
+goal Qsort.thy "set(qsort le xs) = set xs";
by(simp_tac (!simpset addsimps [set_of_list_via_mset,qsort_permutes]) 1);
qed "set_of_list_qsort";
Addsimps [set_of_list_qsort];
goal List.thy
- "(!x:set_of_list[x:xs.P(x)].Q(x)) = (!x:set_of_list xs. P(x)-->Q(x))";
+ "(!x:set[x:xs.P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
by (list.induct_tac "xs" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed"Ball_set_of_list_filter";
@@ -43,7 +43,7 @@
goal Qsort.thy
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \
-\ (!x:set_of_list xs. !y:set_of_list ys. le x y))";
+\ (!x:set xs. !y:set ys. le x y))";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "sorted_append";
--- a/src/HOL/ex/Sorting.ML Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/ex/Sorting.ML Thu Jun 26 13:20:50 1997 +0200
@@ -19,7 +19,7 @@
Addsimps [mset_append, mset_compl_add];
-goal Sorting.thy "set_of_list xs = {x.mset xs x ~= 0}";
+goal Sorting.thy "set xs = {x.mset xs x ~= 0}";
by (list.induct_tac "xs" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
by (Fast_tac 1);
--- a/src/HOL/ex/Sorting.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/ex/Sorting.thy Thu Jun 26 13:20:50 1997 +0200
@@ -21,7 +21,7 @@
primrec sorted list
"sorted le [] = True"
- "sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)"
+ "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
primrec mset list
"mset [] y = 0"