--- a/src/HOL/Auth/WooLam.ML Fri Nov 29 15:31:13 1996 +0100
+++ b/src/HOL/Auth/WooLam.ML Fri Nov 29 17:58:18 1996 +0100
@@ -20,8 +20,8 @@
(*Weak liveness: there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX NB. EX evs: woolam lost. \
-\ Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B)) \
+\ ==> EX NB. EX evs: woolam. \
+\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS
@@ -35,7 +35,7 @@
(**** Inductive proofs about woolam ****)
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : woolam lost ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
by (etac woolam.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
@@ -53,9 +53,7 @@
bind_thm ("WL4_parts_sees_Spy",
WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
- harder to complete, since simplification does less for us.*)
-val parts_Fake_tac = forw_inst_tac [("lost","lost")] WL4_parts_sees_Spy 6;
+val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
@@ -73,7 +71,7 @@
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. evs : woolam lost \
+ "!!evs. evs : woolam \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
by (parts_induct_tac 1);
by (Auto_tac());
@@ -81,14 +79,14 @@
Addsimps [Spy_see_shrK];
goal thy
- "!!evs. evs : woolam lost \
+ "!!evs. evs : woolam \
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
-\ evs : woolam lost |] ==> A:lost";
+\ evs : woolam |] ==> A:lost";
by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
qed "Spy_see_shrK_D";
@@ -98,7 +96,7 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : woolam lost ==> \
+goal thy "!!evs. evs : woolam ==> \
\ length evs <= length evt --> \
\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
@@ -121,9 +119,9 @@
(*If the encrypted message appears then it originated with Alice*)
goal thy
- "!!evs. [| A ~: lost; evs : woolam lost |] \
-\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) \
-\ --> (EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs)";
+ "!!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)";
by (parts_induct_tac 1);
by (Fast_tac 1);
qed_spec_mp "NB_Crypt_imp_Alice_msg";
@@ -132,10 +130,10 @@
Alice, then she originated that certificate. But we DO NOT know that B
ever saw it: the Spy may have rerouted the message to the Server.*)
goal thy
- "!!evs. [| A ~: lost; evs : woolam lost; \
-\ Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} \
+ "!!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 (Nonce NB) (shrK A)) : set_of_list evs";
+\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
addSEs [MPair_parts]
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -146,9 +144,9 @@
(*Server sent WL5 only if it received the right sort of message*)
goal thy
- "!!evs. evs : woolam lost ==> \
-\ Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs \
-\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt NB (shrK A)|} \
+ "!!evs. evs : woolam ==> \
+\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs \
+\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
\ : set_of_list evs)";
by (parts_induct_tac 1);
by (ALLGOALS Fast_tac);
@@ -157,18 +155,18 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: lost; evs : woolam lost |] \
-\ ==> Crypt {|Agent A, NB|} (shrK B) : parts (sees lost Spy evs) \
-\ --> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
+ "!!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";
by (parts_induct_tac 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
(*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 {|Agent A, NB|} (shrK B)) : set_of_list evs; \
-\ B ~: lost; evs : woolam lost |] \
-\ ==> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
+ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
+\ B ~: lost; evs : woolam |] \
+\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "B_got_WL5";
@@ -178,9 +176,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 {|Agent A, Nonce NB|} (shrK B)): set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : woolam lost |] \
-\ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
+ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
+\ A ~: lost; B ~: lost; evs : woolam |] \
+\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
by (fast_tac (!claset addIs [Server_trust_WL4]
addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
qed "B_trust_WL5";
@@ -188,7 +186,7 @@
(*B only issues challenges in response to WL1. Useful??*)
goal thy
- "!!evs. [| B ~= Spy; evs : woolam lost |] \
+ "!!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)";
by (parts_induct_tac 1);
@@ -198,10 +196,10 @@
(**CANNOT be proved because A doesn't know where challenges come from...
goal thy
- "!!evs. [| A ~: lost; B ~= Spy; evs : woolam lost |] \
-\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) & \
+ "!!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 (Nonce NB) (shrK A)) : set_of_list evs";
+\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
by (parts_induct_tac 1);
by (Step_tac 1);
by (best_tac (!claset addSEs partsEs
--- a/src/HOL/Auth/WooLam.thy Fri Nov 29 15:31:13 1996 +0100
+++ b/src/HOL/Auth/WooLam.thy Fri Nov 29 17:58:18 1996 +0100
@@ -16,47 +16,48 @@
WooLam = Shared +
-consts woolam :: "agent set => event list set"
-inductive "woolam lost"
+consts lost :: agent set (*No need for it to be a variable*)
+ woolam :: event list set
+inductive woolam
intrs
(*Initial trace is empty*)
- Nil "[]: woolam lost"
+ Nil "[]: woolam"
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: woolam lost; B ~= Spy;
+ Fake "[| evs: woolam; B ~= Spy;
X: synth (analz (sees lost Spy evs)) |]
- ==> Says Spy B X # evs : woolam lost"
+ ==> Says Spy B X # evs : woolam"
(*Alice initiates a protocol run*)
- WL1 "[| evs: woolam lost; A ~= B |]
- ==> Says A B (Agent A) # evs : woolam lost"
+ WL1 "[| evs: woolam; A ~= B |]
+ ==> Says A B (Agent A) # evs : woolam"
(*Bob responds to Alice's message with a challenge.*)
- WL2 "[| evs: woolam lost; A ~= B;
+ WL2 "[| evs: woolam; A ~= B;
Says A' B (Agent A) : set_of_list evs |]
- ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
+ ==> Says B A (Nonce (newN evs)) # 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 lost; A ~= B;
+ WL3 "[| evs: woolam; A ~= B;
Says B' A (Nonce NB) : set_of_list evs;
Says A B (Agent A) : set_of_list evs |]
- ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost"
+ ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
(*Bob forwards Alice's response to the Server.*)
- WL4 "[| evs: woolam lost; B ~= Server;
+ WL4 "[| evs: woolam; B ~= Server;
Says A' B X : set_of_list evs;
Says A'' B (Agent A) : set_of_list evs |]
- ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost"
+ ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
(*Server decrypts Alice's response for Bob.*)
- WL5 "[| evs: woolam lost; B ~= Server;
- Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|}
+ WL5 "[| evs: woolam; B ~= Server;
+ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
: set_of_list evs |]
- ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
- # evs : woolam lost"
+ ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
+ # evs : woolam"
end