--- a/src/HOL/Auth/Message.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Message.ML Fri Jan 17 12:49:31 1997 +0100
@@ -18,16 +18,6 @@
Simp_tac i;
-
-(*GOALS.ML??*)
-fun prlim n = (goals_limit:=n; pr());
-
-(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
-goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
-by (fast_tac (!claset addEs [equalityE]) 1);
-val subset_range_iff = result();
-
-
open Message;
AddIffs (msg.inject);
@@ -44,49 +34,6 @@
Addsimps [invKey, invKey_eq];
-(**** Freeness laws for HPair ****)
-
-goalw thy [HPair_def] "Agent A ~= HPair X Y";
-by (Simp_tac 1);
-qed "Agent_neq_HPair";
-
-goalw thy [HPair_def] "Nonce N ~= HPair X Y";
-by (Simp_tac 1);
-qed "Nonce_neq_HPair";
-
-goalw thy [HPair_def] "Key K ~= HPair X Y";
-by (Simp_tac 1);
-qed "Key_neq_HPair";
-
-goalw thy [HPair_def] "Hash Z ~= HPair X Y";
-by (Simp_tac 1);
-qed "Hash_neq_HPair";
-
-goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
-by (Simp_tac 1);
-qed "Crypt_neq_HPair";
-
-val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair,
- Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
-
-AddIffs HPair_neqs;
-AddIffs (HPair_neqs RL [not_sym]);
-
-goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
-by (Simp_tac 1);
-qed "HPair_eq";
-
-goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
-by (Simp_tac 1);
-qed "MPair_eq_HPair";
-
-goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
-by (Auto_tac());
-qed "HPair_eq_MPair";
-
-AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
-
-
(**** keysFor operator ****)
goalw thy [keysFor_def] "keysFor {} = {}";
@@ -133,7 +80,7 @@
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key,
- keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
+ keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
by (Fast_tac 1);
@@ -282,8 +229,8 @@
fun parts_tac i =
EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
- etac parts.induct i,
- REPEAT (fast_tac (!claset addss (!simpset)) i)];
+ etac parts.induct i,
+ REPEAT (fast_tac (!claset addss (!simpset)) i)];
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
by (parts_tac 1);
@@ -410,8 +357,8 @@
fun analz_tac i =
EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
- etac analz.induct i,
- REPEAT (fast_tac (!claset addss (!simpset)) i)];
+ etac analz.induct i,
+ REPEAT (fast_tac (!claset addss (!simpset)) i)];
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
by (analz_tac 1);
@@ -488,7 +435,7 @@
qed "analz_Crypt_if";
Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key,
- analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
+ analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
(*This rule supposes "for the sake of argument" that we have the key.*)
goal thy "analz (insert (Crypt K X) H) <= \
@@ -587,7 +534,7 @@
but can synth a pair or encryption from its components...*)
val mk_cases = synth.mk_cases msg.simps;
-(*NO Agent_synth, as any Agent name can be synthd*)
+(*NO Agent_synth, as any Agent name can be synthesized*)
val Nonce_synth = mk_cases "Nonce n : synth H";
val Key_synth = mk_cases "Key K : synth H";
val Hash_synth = mk_cases "Hash X : synth H";
@@ -752,17 +699,6 @@
by (Fast_tac 1);
qed "Fake_analz_insert";
-(*Needed????????????????*)
-goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
-\ analz (insert X H) <= synth (analz H) Un analz H";
-by (rtac subsetI 1);
-by (subgoal_tac "x : analz (synth (analz H))" 1);
-by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
- addSEs [impOfSubs analz_mono]) 2);
-by (Full_simp_tac 1);
-by (Fast_tac 1);
-qed "Fake_analz_insert_old";
-
goal thy "(X: analz H & X: parts H) = (X: analz H)";
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
val analz_conj_parts = result();
@@ -788,8 +724,8 @@
qed "Crypt_synth_analz";
-goal thy "!!K. Key K ~: analz H \
-\ ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)";
+goal thy "!!K. X ~: synth (analz H) \
+\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
by (Fast_tac 1);
qed "Hash_synth_analz";
Addsimps [Hash_synth_analz];
@@ -799,41 +735,41 @@
(*** Freeness ***)
-goalw thy [HPair_def] "Agent A ~= HPair X Y";
+goalw thy [HPair_def] "Agent A ~= Hash[X] Y";
by (Simp_tac 1);
qed "Agent_neq_HPair";
-goalw thy [HPair_def] "Nonce N ~= HPair X Y";
+goalw thy [HPair_def] "Nonce N ~= Hash[X] Y";
by (Simp_tac 1);
qed "Nonce_neq_HPair";
-goalw thy [HPair_def] "Key K ~= HPair X Y";
+goalw thy [HPair_def] "Key K ~= Hash[X] Y";
by (Simp_tac 1);
qed "Key_neq_HPair";
-goalw thy [HPair_def] "Hash Z ~= HPair X Y";
+goalw thy [HPair_def] "Hash Z ~= Hash[X] Y";
by (Simp_tac 1);
qed "Hash_neq_HPair";
-goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
+goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y";
by (Simp_tac 1);
qed "Crypt_neq_HPair";
val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair,
- Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
+ Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
AddIffs HPair_neqs;
AddIffs (HPair_neqs RL [not_sym]);
-goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
+goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
by (Simp_tac 1);
qed "HPair_eq";
-goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
+goalw thy [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
by (Simp_tac 1);
qed "MPair_eq_HPair";
-goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
+goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
by (Auto_tac());
qed "HPair_eq_MPair";
@@ -842,31 +778,31 @@
(*** Specialized laws, proved in terms of those for Hash and MPair ***)
-goalw thy [HPair_def] "keysFor (insert (HPair X Y) H) = keysFor H";
+goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
by (Simp_tac 1);
qed "keysFor_insert_HPair";
goalw thy [HPair_def]
- "parts (insert (HPair X Y) H) = \
-\ insert (HPair X Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
+ "parts (insert (Hash[X] Y) H) = \
+\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
by (Simp_tac 1);
qed "parts_insert_HPair";
goalw thy [HPair_def]
- "analz (insert (HPair X Y) H) = \
-\ insert (HPair X Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
+ "analz (insert (Hash[X] Y) H) = \
+\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
by (Simp_tac 1);
qed "analz_insert_HPair";
goalw thy [HPair_def] "!!H. X ~: synth (analz H) \
-\ ==> (HPair X Y : synth (analz H)) = \
+\ ==> (Hash[X] Y : synth (analz H)) = \
\ (Hash {|X, Y|} : analz H & Y : synth (analz H))";
by (Simp_tac 1);
by (Fast_tac 1);
qed "HPair_synth_analz";
Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair,
- HPair_synth_analz, HPair_synth_analz];
+ HPair_synth_analz, HPair_synth_analz];
(*We do NOT want Crypt... messages broken up in protocols!!*)
@@ -881,7 +817,7 @@
val pushKeys = map (insComm thy "Key ?K")
["Agent ?C", "Nonce ?N", "Hash ?X",
- "MPair ?X ?Y", "Crypt ?X ?K'"];
+ "MPair ?X ?Y", "Crypt ?X ?K'"];
val pushCrypts = map (insComm thy "Crypt ?X ?K")
["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
@@ -898,7 +834,7 @@
val Fake_insert_tac =
dresolve_tac [impOfSubs Fake_analz_insert,
- impOfSubs Fake_parts_insert] THEN'
+ impOfSubs Fake_parts_insert] THEN'
eresolve_tac [asm_rl, synth.Inj];
(*Analysis of Fake cases and of messages that forward unknown parts.
@@ -916,9 +852,9 @@
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
DEPTH_SOLVE
(REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
- THEN
- IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
- impOfSubs analz_subset_parts]) 2 1))
+ THEN
+ IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
+ impOfSubs analz_subset_parts]) 2 1))
]) i);
(** Useful in many uniqueness proofs **)
@@ -929,10 +865,10 @@
their standard form*)
fun prove_unique_tac lemma =
EVERY' [dtac lemma,
- REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
- (*Duplicate the assumption*)
- forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
- fast_tac (!claset addSDs [spec])];
+ REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
+ (*Duplicate the assumption*)
+ forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
+ fast_tac (!claset addSDs [spec])];
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
--- a/src/HOL/Auth/Message.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Message.thy Fri Jan 17 12:49:31 1997 +0100
@@ -41,7 +41,7 @@
(*Allows messages of the form {|A,B,NA|}, etc...*)
syntax
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+ "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
@@ -50,8 +50,8 @@
constdefs
(*Message Y, paired with a MAC computed with the help of X*)
- HPair :: "[msg,msg]=>msg"
- "HPair X Y == {| Hash{|X,Y|}, Y|}"
+ HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000])
+ "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
(*Keys useful to decrypt elements of a message set*)
keysFor :: msg set => key set
--- a/src/HOL/Auth/NS_Public.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML Fri Jan 17 12:49:31 1997 +0100
@@ -11,7 +11,6 @@
proof_timing:=true;
HOL_quantifiers := false;
-Pretty.setdepth 20;
AddIffs [Spy_in_lost];
@@ -26,10 +25,7 @@
\ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list 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 (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
- addss (!simpset setsolver safe_solver))));
+by possibility_tac;
result();
@@ -84,9 +80,9 @@
fun analz_induct_tac i =
- etac ns_public.induct i THEN
+ etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
- (!simpset addsimps [not_parts_not_analz]
+ (!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if]));
(**** Authenticity properties obtained from NS2 ****)
@@ -105,9 +101,9 @@
by (fast_tac (!claset addSEs partsEs) 3);
(*Fake*)
by (best_tac (!claset addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2);
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
+ addss (!simpset)) 2);
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
@@ -132,8 +128,8 @@
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
addss (!simpset)) 1);
val lemma = result();
@@ -158,7 +154,7 @@
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -191,9 +187,9 @@
by (fast_tac (!claset addss (!simpset)) 1);
by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
qed_spec_mp "NA_decrypt_imp_B_msg";
(*Corollary: if A receives B's message NS2 and the nonce NA agrees
@@ -219,10 +215,10 @@
by (analz_induct_tac 1);
(*Fake*)
by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 2);
+ addSDs [impOfSubs Fake_parts_insert]
+ addIs [analz_insertI]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 2);
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
qed_spec_mp "B_trusts_NS1";
@@ -252,9 +248,9 @@
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
val lemma = result();
goal thy
@@ -317,14 +313,14 @@
by (fast_tac (!claset addss (!simpset)) 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
(*NS3*)
by (Step_tac 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
- addDs [unique_NB]) 1);
+ addDs [unique_NB]) 1);
qed_spec_mp "NB_decrypt_imp_A_msg";
(*Corollary: if B receives message NS3 and the nonce NB agrees,
@@ -363,14 +359,14 @@
by (fast_tac (!claset addss (!simpset)) 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (best_tac (!claset addSIs [disjI2]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 1);
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
+ addss (!simpset)) 1);
(*NS3*)
by (Step_tac 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
- addDs [unique_NB]) 1);
+ addDs [unique_NB]) 1);
val lemma = result() RSN (2, rev_mp) RSN (2, rev_mp);
goal thy
--- a/src/HOL/Auth/NS_Public.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/NS_Public.thy Fri Jan 17 12:49:31 1997 +0100
@@ -37,9 +37,9 @@
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent 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|})
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
: set_of_list evs |]
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
--- a/src/HOL/Auth/NS_Public_Bad.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Jan 17 12:49:31 1997 +0100
@@ -15,7 +15,6 @@
proof_timing:=true;
HOL_quantifiers := false;
-Pretty.setdepth 20;
AddIffs [Spy_in_lost];
@@ -30,10 +29,7 @@
\ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list 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 (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
- addss (!simpset setsolver safe_solver))));
+by possibility_tac;
result();
@@ -88,9 +84,9 @@
fun analz_induct_tac i =
- etac ns_public.induct i THEN
+ etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
- (!simpset addsimps [not_parts_not_analz]
+ (!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if]));
@@ -110,9 +106,9 @@
by (fast_tac (!claset addSEs partsEs) 3);
(*Fake*)
by (best_tac (!claset addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset)) 2);
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
+ addss (!simpset)) 2);
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
@@ -137,8 +133,8 @@
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
addss (!simpset)) 1);
val lemma = result();
@@ -163,7 +159,7 @@
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]
addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
@@ -193,9 +189,9 @@
by (fast_tac (!claset addss (!simpset)) 1);
by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
(*NS2*)
by (Step_tac 1);
by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
@@ -225,10 +221,10 @@
by (analz_induct_tac 1);
(*Fake*)
by (best_tac (!claset addSIs [disjI2]
- addSDs [impOfSubs Fake_parts_insert]
- addIs [analz_insertI]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 2);
+ addSDs [impOfSubs Fake_parts_insert]
+ addIs [analz_insertI]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 2);
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
qed_spec_mp "B_trusts_NS1";
@@ -257,9 +253,9 @@
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
val lemma = result();
goal thy
@@ -316,18 +312,18 @@
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
by (fast_tac (!claset addss (!simpset)) 1);
-br (ccontr RS disjI2) 1;
+by (rtac (ccontr RS disjI2) 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (Fast_tac 1);
by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
(*NS3*)
by (Step_tac 1);
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT1 (assume_tac 1));
by (Fast_tac 1);
by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addDs [unique_NB]) 1);
+ addDs [unique_NB]) 1);
qed_spec_mp "NB_decrypt_imp_A_msg";
--- a/src/HOL/Auth/NS_Public_Bad.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Jan 17 12:49:31 1997 +0100
@@ -41,9 +41,9 @@
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
+ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
: set_of_list evs;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
: set_of_list evs |]
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
--- a/src/HOL/Auth/NS_Shared.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Fri Jan 17 12:49:31 1997 +0100
@@ -22,10 +22,9 @@
\ ==> EX N K. EX evs: ns_shared lost. \
\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list 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);
-by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+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);
+by possibility_tac;
result();
@@ -52,15 +51,13 @@
(*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 \
\ ==> X : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+by (fast_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 \
\ ==> K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
val parts_Fake_tac =
@@ -107,72 +104,18 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
-
-(*Nobody can have SEEN keys that will be generated in the future. *)
+(*Nobody can have used non-existent keys!*)
goal thy "!!evs. evs : ns_shared lost ==> \
-\ length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-by (ALLGOALS (fast_tac (!claset addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK i) : parts {X}; \
-\ evs : ns_shared lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-
-(*** Future nonces can't be seen or used! ***)
-
-goal thy "!!evs. evs : ns_shared lost ==> \
-\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (REPEAT_FIRST
- (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un, Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-
-(*Nobody can have USED keys that will be generated in the future.
- ...very like new_keys_not_seen*)
-goal thy "!!evs. evs : ns_shared lost ==> \
-\ length evs <= i --> \
-\ newK i ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
-(*NS1 and NS2*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]));
-(*Fake and NS3*)
-by (EVERY
- (map
- (best_tac
- (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset)))
- [2,1]));
-(*NS4 and NS5: nonce exchange*)
-by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
- addIs [less_SucI, impOfSubs keysFor_mono]
- addss (!simpset addsimps [le_def])) 1));
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
+(*NS2, NS4, NS5*)
+by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -186,14 +129,15 @@
(*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, K, X|}) : set_of_list evs; \
-\ evs : ns_shared lost |] \
-\ ==> (EX i. K = Key(newK i) & \
-\ X = (Crypt (shrK B) {|K, Agent A|}) & \
-\ K' = shrK A)";
+ "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
+\ : set_of_list evs; \
+\ evs : ns_shared lost |] \
+\ ==> K ~: range shrK & \
+\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \
+\ K' = shrK A";
by (etac rev_mp 1);
by (etac ns_shared.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (Auto_tac());
qed "Says_Server_message_form";
@@ -219,16 +163,14 @@
goal thy
"!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
\ : set_of_list evs; evs : ns_shared lost |] \
-\ ==> (EX i. K = newK i & i < length evs & \
-\ X = (Crypt (shrK B) {|Key K, Agent A|})) \
-\ | X : analz (sees lost Spy evs)";
+\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
+\ | X : analz (sees lost Spy evs)";
by (case_tac "A : lost" 1);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
addss (!simpset)) 1);
by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
by (fast_tac (!claset addEs partsEs
addSDs [A_trusts_NS2, Says_Server_message_form]
- addIs [Says_imp_old_keys]
addss (!simpset)) 1);
qed "Says_S_message_form";
@@ -237,14 +179,13 @@
val analz_Fake_tac =
forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN
- Full_simp_tac 7 THEN
- REPEAT_FIRST (eresolve_tac [asm_rl, exE, disjE] ORELSE' hyp_subst_tac);
+ REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -256,8 +197,8 @@
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
goal thy
- "!!evs. evs : ns_shared lost ==> \
-\ (Crypt (newK i) X) : parts (sees lost Spy evs) & \
+ "!!evs. [| evs : ns_shared lost; Kab ~: range shrK |] ==> \
+\ (Crypt KAB X) : parts (sees lost Spy evs) & \
\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
by (etac ns_shared.induct 1);
by parts_Fake_tac;
@@ -276,31 +217,28 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
"!!evs. evs : ns_shared lost ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
-\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac ns_shared.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 18 secs*)
- (asm_simp_tac
- (!simpset addsimps [Un_assoc RS sym,
- insert_Key_singleton, insert_Key_image, pushKey_newK]
- setloop split_tac [expand_if])));
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+(*Takes 24 secs*)
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*NS4, Fake*)
-by (EVERY (map spy_analz_tac [5,2]));
-(*NS3, NS2, Base*)
-by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
-qed_spec_mp "analz_image_newK";
+by (EVERY (map spy_analz_tac [3,2]));
+(*Base*)
+by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. evs : ns_shared lost ==> \
-\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
-\ (K = newK i | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : ns_shared lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
(** The session key K uniquely identifies the message, if encrypted
@@ -320,8 +258,8 @@
(*NS2: it can't be a new key*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
- delrules [conjI] (*prevent split-up into 4 subgoals*)
+by (fast_tac (!claset delrules [conjI] (*prevent split-up into 4 subgoals*)
+ addSEs sees_Spy_partsEs
addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
@@ -352,15 +290,14 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
setloop split_tac [expand_if])));
+(*NS4, Fake*)
+by (EVERY (map spy_analz_tac [4,1]));
(*NS2*)
-by (fast_tac (!claset addIs [parts_insertI]
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 2);
-(*NS4, Fake*)
-by (EVERY (map spy_analz_tac [3,1]));
+by (fast_tac (!claset addSEs sees_Spy_partsEs
+ addIs [parts_insertI, impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
(*NS3 and Oops subcases*) (**LEVEL 5 **)
by (step_tac (!claset delrules [impCE]) 1);
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
@@ -382,10 +319,10 @@
(*Final version: Server's message in the most abstract form*)
goal thy
"!!evs. [| Says Server A \
-\ (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs; \
-\ (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs); \
+\ (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); \
\ A ~: lost; B ~: lost; evs : ns_shared lost \
-\ |] ==> K ~: analz (sees lost Spy evs)";
+\ |] ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -394,10 +331,10 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server A \
-\ (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs; \
-\ (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs); \
+\ (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); \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
-\ ==> K ~: analz (sees lost C evs)";
+\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
@@ -449,8 +386,8 @@
addDs [impOfSubs analz_subset_parts]) 1);
by (Fast_tac 2);
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
-(*Contradiction from the assumption
- Crypt (newK(length evsa)) (Nonce NB) : parts (sees lost Spy evsa) *)
+(*Subgoal 1: contradiction from the assumptions
+ Key K ~: used evsa and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
by (dtac Crypt_imp_invKey_keysFor 1);
(**LEVEL 10**)
by (Asm_full_simp_tac 1);
@@ -460,7 +397,7 @@
by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN
REPEAT (assume_tac 1));
-by (fast_tac (!claset addDs [unique_session_keys]) 1);
+by (best_tac (!claset addDs [unique_session_keys]) 1);
val lemma = result();
goal thy
--- a/src/HOL/Auth/NS_Shared.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Fri Jan 17 12:49:31 1997 +0100
@@ -26,20 +26,20 @@
==> Says Spy B X # evs : ns_shared lost"
(*Alice initiates a protocol run, requesting to talk to any B*)
- NS1 "[| evs: ns_shared lost; A ~= Server |]
- ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|}
- # evs : ns_shared lost"
+ NS1 "[| evs: ns_shared lost; A ~= Server; Nonce NA ~: used evs |]
+ ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
+ : ns_shared lost"
(*Server's response to Alice's message.
!! It may respond more than once to A's request !!
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;
+ 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 Server A
(Crypt (shrK A)
- {|Nonce NA, Agent B, Key (newK(length evs)),
- (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|})
+ {|Nonce NA, Agent B, Key KAB,
+ (Crypt (shrK B) {|Key KAB, Agent A|})|})
# evs : ns_shared lost"
(*We can't assume S=Server. Agent A "remembers" her nonce.
@@ -52,9 +52,9 @@
(*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;
+ 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 B A (Crypt K (Nonce (newN(length evs)))) # evs
+ ==> Says B A (Crypt K (Nonce NB)) # evs
: ns_shared lost"
(*Alice responds with Nonce NB if she has seen the key before.
--- a/src/HOL/Auth/OtwayRees.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Fri Jan 17 12:49:31 1997 +0100
@@ -26,9 +26,7 @@
\ : set_of_list 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 (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+by possibility_tac;
result();
@@ -59,15 +57,14 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
-goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs \
+goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
\ ==> X : analz (sees lost Spy evs)";
by (fast_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 \
\ ==> K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
@@ -84,9 +81,9 @@
harder to complete, since simplification does less for us.*)
val parts_Fake_tac =
let val tac = forw_inst_tac [("lost","lost")]
- in tac OR2_parts_sees_Spy 4 THEN
- tac OR4_parts_sees_Spy 6 THEN
- tac Oops_parts_sees_Spy 7
+ in tac OR2_parts_sees_Spy 4 THEN
+ tac OR4_parts_sees_Spy 6 THEN
+ tac Oops_parts_sees_Spy 7
end;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
@@ -128,77 +125,18 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
-
-(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!i. evs : otway lost ==> \
-\ length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK i) : parts {X}; \
-\ evs : otway lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-(*** Future nonces can't be seen or used! ***)
-
-goal thy "!!evs. evs : otway lost ==> \
-\ length evs <= i --> \
-\ Nonce (newN i) ~: parts (sees lost Spy evs)";
+(*Nobody can have used non-existent keys!*)
+goal thy "!!evs. evs : otway lost ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-(*Variant: old messages must contain old nonces!*)
-goal thy "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN i) : parts {X}; \
-\ evs : otway lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_nonces";
-
-
-(*Nobody can have USED keys that will be generated in the future.
- ...very like new_keys_not_seen*)
-goal thy "!!i. evs : otway lost ==> \
-\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
-by (parts_induct_tac 1);
-(*OR1 and OR3*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
-(*Fake, OR2, OR4: these messages send unknown (X) components*)
-by (REPEAT
- (best_tac
- (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset)) 1));
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
+(*OR1-3*)
+by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -214,11 +152,10 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
+ "!!evs. [| Says Server B \
+\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \
\ evs : otway lost |] \
-\ ==> (EX n. K = Key(newK n)) & \
-\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
+\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -230,14 +167,14 @@
dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
- assume_tac 7 THEN Full_simp_tac 7 THEN
+ assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -248,32 +185,28 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway lost ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
-\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : otway lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 11 secs*)
- (asm_simp_tac
- (!simpset addsimps [Un_assoc RS sym,
- insert_Key_singleton, insert_Key_image, pushKey_newK]
- setloop split_tac [expand_if])));
-(*OR4, OR2, Fake*)
-by (EVERY (map spy_analz_tac [5,3,2]));
-(*Oops, OR3, Base*)
-by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
-qed_spec_mp "analz_image_newK";
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Base*)
+by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+(*Fake, OR2, OR4*)
+by (REPEAT (spy_analz_tac 1));
+qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. evs : otway lost ==> \
-\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
-\ (K = newK i | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
(*** The Key K uniquely identifies the Server's message. **)
@@ -291,8 +224,8 @@
by (Fast_tac 2);
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a very new message, and handle this case by contradiction*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+(*...we assume X is a recent message, and handle this case by contradiction*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs
delrules [conjI] (*prevent split-up into 4 subgoals*)
addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
@@ -333,8 +266,7 @@
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*OR1: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NA = ?y" 1);
-by (best_tac (!claset addSEs partsEs
- addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1);
+by (best_tac (!claset addSEs sees_Spy_partsEs) 1);
val lemma = result();
goal thy
@@ -346,8 +278,6 @@
qed "unique_NA";
-val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
-
(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see OtwayRees_Bad.*)
@@ -358,7 +288,7 @@
\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
\ ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
-by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
+by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs
addSDs [impOfSubs parts_insert_subset_Un]
addss (!simpset)) 1));
qed_spec_mp"no_nonce_OR1_OR2";
@@ -380,16 +310,14 @@
by (parts_induct_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
+ addSEs sees_Spy_partsEs
addss (!simpset)) 1);
(*OR3 and OR4*)
(*OR4*)
by (REPEAT (Safe_step_tac 2));
by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
by (fast_tac (!claset addSIs [Crypt_imp_OR1]
- addEs partsEs
- addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
+ addEs sees_Spy_partsEs) 2);
(*OR3*) (** LEVEL 5 **)
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
by (step_tac (!claset delrules [disjCI, impCE]) 1);
@@ -420,8 +348,7 @@
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
- addEs partsEs
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addEs sees_Spy_partsEs) 1);
qed "A_trusts_OR4";
@@ -439,11 +366,13 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
- analz_insert_Key_newK]
- setloop split_tac [expand_if])));
+ (asm_simp_tac (!simpset addcongs [conj_cong]
+ addsimps [not_parts_not_analz, analz_insert_freshK]
+ setloop split_tac [expand_if])));
(*OR3*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+by (fast_tac (!claset delrules [impCE]
+ addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]
addss (!simpset addsimps [parts_insert2])) 3);
(*OR4, OR2, Fake*)
by (REPEAT_FIRST spy_analz_tac);
@@ -453,12 +382,12 @@
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, K|}, \
-\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
+ "!!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; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> K ~: analz (sees lost Spy evs)";
+\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -467,11 +396,11 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, K|}, \
-\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
+\ {|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; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> K ~: analz (sees lost C evs)";
+\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
@@ -507,7 +436,7 @@
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
(*OR2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NB = ?y" 1);
-by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
+by (deepen_tac (!claset addSEs sees_Spy_partsEs) 3 1);
val lemma = result();
goal thy
@@ -537,8 +466,7 @@
by (parts_induct_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
+ addSEs sees_Spy_partsEs
addss (!simpset)) 1);
(*OR4*)
by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
@@ -570,8 +498,7 @@
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
- addEs partsEs
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addEs sees_Spy_partsEs) 1);
qed "B_trusts_OR3";
--- a/src/HOL/Auth/OtwayRees.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Fri Jan 17 12:49:31 1997 +0100
@@ -28,27 +28,26 @@
==> Says Spy B X # evs : otway lost"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway lost; A ~= B; B ~= Server |]
- ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B,
- Crypt (shrK A)
- {|Nonce (newN(length evs)), Agent A, Agent B|} |}
+ OR1 "[| evs: otway lost; A ~= B; B ~= Server; Nonce NA ~: used evs |]
+ ==> Says A B {|Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs : otway lost"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.
Note that NB is encrypted.*)
- OR2 "[| evs: otway lost; B ~= Server;
+ 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 B Server
{|Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
- {|Nonce NA, Nonce(newN(length evs)), Agent A, Agent B|}|}
+ {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
# evs : otway lost"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs: otway lost; B ~= Server;
+ OR3 "[| evs: otway lost; B ~= Server; Key KAB ~: used evs;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
@@ -56,18 +55,18 @@
: set_of_list evs |]
==> Says Server B
{|Nonce NA,
- Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
- Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
+ Crypt (shrK A) {|Nonce NA, Key KAB|},
+ Crypt (shrK B) {|Nonce NB, Key KAB|}|}
# evs : otway lost"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
OR4 "[| evs: otway lost; A ~= B;
- Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set_of_list evs;
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;
+ Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs |]
==> Says B A {|Nonce NA, X|} # evs : otway lost"
--- a/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 17 12:49:31 1997 +0100
@@ -26,9 +26,7 @@
\ : set_of_list 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 (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+by possibility_tac;
result();
@@ -54,15 +52,14 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says S B {|X, X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
by (fast_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)";
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
(*OR4_analz_sees_Spy lets us treat those cases using the same
@@ -81,9 +78,9 @@
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
(DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
+ (*Fake message*)
+ TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
addss (!simpset)) 2)) THEN
(*Base case*)
fast_tac (!claset addss (!simpset)) 1 THEN
@@ -117,49 +114,18 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
-
-(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!i. evs : otway lost ==> \
-\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
+(*Nobody can have used non-existent keys!*)
+goal thy "!!evs. evs : otway lost ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK i) : parts {X}; \
-\ evs : otway lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-(*Nobody can have USED keys that will be generated in the future.
- ...very like new_keys_not_seen*)
-goal thy "!!i. evs : otway lost ==> \
-\ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
-(*Fake, OR4: these messages send unknown (X) components*)
-by (EVERY
- (map
- (best_tac
- (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset))) [5,1]));
-(*Remaining subgoals*)
-by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1));
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
+(*OR3*)
+by (fast_tac (!claset addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -174,12 +140,12 @@
(*Describes the form of K and NA when the Server sends this message.*)
goal thy
- "!!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; \
-\ evs : otway lost |] \
-\ ==> (EX n. K = Key(newK n)) & \
-\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
+ "!!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; \
+\ evs : otway lost |] \
+\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -190,18 +156,17 @@
val analz_Fake_tac =
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
- assume_tac 7 THEN Full_simp_tac 7 THEN
+ assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
-
****)
@@ -210,31 +175,28 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
"!!evs. evs : otway lost ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
-\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 18 secs*)
- (asm_simp_tac
- (!simpset addsimps [Un_assoc RS sym,
- insert_Key_singleton, insert_Key_image, pushKey_newK]
- setloop split_tac [expand_if])));
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+(*14 seconds*)
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*OR4, Fake*)
-by (EVERY (map spy_analz_tac [4,2]));
-(*Oops, OR3, Base*)
-by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
-qed_spec_mp "analz_image_newK";
+by (EVERY (map spy_analz_tac [3,2]));
+(*Base*)
+by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. evs : otway lost ==> \
-\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
-\ (K = newK i | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
(*** The Key K uniquely identifies the Server's message. **)
@@ -254,8 +216,8 @@
by (Fast_tac 2);
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a very new message, and handle this case by contradiction*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+(*...we assume X is a recent message and handle this case by contradiction*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs
delrules [conjI] (*prevent split-up into 4 subgoals*)
addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
@@ -306,8 +268,7 @@
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
- addEs partsEs
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addEs sees_Spy_partsEs) 1);
qed "A_trusts_OR4";
@@ -326,38 +287,43 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
- analz_insert_Key_newK]
- setloop split_tac [expand_if])));
+ (asm_simp_tac (!simpset addcongs [conj_cong]
+ addsimps [not_parts_not_analz,
+ analz_insert_freshK]
+ setloop split_tac [expand_if])));
(*OR3*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+by (fast_tac (!claset delrules [impCE]
+ addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]
addss (!simpset addsimps [parts_insert2])) 2);
+(*Oops*)
+by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3);
(*OR4, Fake*)
by (REPEAT_FIRST spy_analz_tac);
-(*Oops*)
-by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
- "!!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;\
-\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> K ~: analz (sees lost Spy evs)";
+ "!!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; \
+\ 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);
by (fast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
goal thy
- "!!evs. [| C ~: {A,B,Server}; \
-\ 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;\
-\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> K ~: analz (sees lost C evs)";
+ "!!evs. [| C ~: {A,B,Server}; \
+\ 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; \
+\ 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);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
@@ -394,6 +360,5 @@
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
- addEs partsEs
- addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+ addEs sees_Spy_partsEs) 1);
qed "B_trusts_OR3";
--- a/src/HOL/Auth/OtwayRees_AN.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Jan 17 12:49:31 1997 +0100
@@ -7,6 +7,11 @@
Simplified version with minimal encryption but explicit messages
+Note that the formalization does not even assume that nonces are fresh.
+This is because the protocol does not rely on uniqueness of nonces for
+security, only for freshness, and the proof script does not prove freshness
+properties.
+
From page 11 of
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
IEEE Trans. SE 22 (1), 1996
@@ -29,36 +34,31 @@
(*Alice initiates a protocol run*)
OR1 "[| evs: otway lost; A ~= B; B ~= Server |]
- ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|}
- # evs : otway lost"
+ ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway lost"
(*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 B Server {|Agent A, Agent B, Nonce NA,
- Nonce (newN(length evs))|}
+ ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
# evs : otway lost"
(*The Server receives Bob's message. Then he sends a new
session key to Bob with a packet for forwarding to Alice.*)
- OR3 "[| evs: otway lost; B ~= Server; A ~= B;
+ 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 |]
==> Says Server B
- {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B,
- Key(newK(length evs))|},
- Crypt (shrK B) {|Nonce NB, Agent A, Agent B,
- Key(newK(length evs))|}|}
+ {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
+ Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
# evs : otway lost"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
OR4 "[| evs: otway lost; A ~= B;
- Says S B {|X,
- Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
+ Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set_of_list evs;
- Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+ Says S B {|X, Crypt(shrK B){|Nonce NB, Agent A, Agent B, Key K|}|}
: set_of_list evs |]
==> Says B A X # evs : otway lost"
--- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 17 12:49:31 1997 +0100
@@ -29,24 +29,12 @@
\ : set_of_list 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 (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+by possibility_tac;
result();
(**** Inductive proofs about otway ****)
-(*The Spy can see more than anybody else, except for their initial state*)
-goal thy
- "!!evs. evs : otway ==> \
-\ sees lost A evs <= initState lost A Un sees lost Spy evs";
-by (etac otway.induct 1);
-by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]
- addss (!simpset))));
-qed "sees_agent_subset_sees_Spy";
-
-
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
by (etac otway.induct 1);
@@ -63,15 +51,14 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
-goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
by (fast_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 \
\ ==> K : parts (sees lost Spy evs)";
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
qed "Oops_parts_sees_Spy";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
@@ -92,9 +79,9 @@
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
(DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
- (*Fake message*)
- TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
+ (*Fake message*)
+ TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
addss (!simpset)) 2)) THEN
(*Base case*)
fast_tac (!claset addss (!simpset)) 1 THEN
@@ -129,76 +116,18 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
-
-(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!i. evs : otway ==> \
-\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK i) : parts {X}; \
-\ evs : otway \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-(*** Future nonces can't be seen or used! ***)
-
-goal thy "!!i. evs : otway ==> \
-\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
+(*Nobody can have used non-existent keys!*)
+goal thy "!!evs. evs : otway ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (REPEAT_FIRST
- (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un, Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-(*Variant: old messages must contain old nonces!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN i) : parts {X}; \
-\ evs : otway \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_nonces";
-
-
-(*Nobody can have USED keys that will be generated in the future.
- ...very like new_keys_not_seen*)
-goal thy "!!i. evs : otway ==> \
-\ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
-by (parts_induct_tac 1);
-(*OR1 and OR3*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
-(*Fake, OR2, OR4: these messages send unknown (X) components*)
-by (REPEAT
- (best_tac
- (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset)) 1));
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
+(*OR1-3*)
+by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -214,11 +143,10 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ evs : otway |] \
-\ ==> (EX n. K = Key(newK n)) & \
-\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
+ "!!evs. [| Says Server B \
+\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \
+\ evs : otway |] \
+\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -229,61 +157,46 @@
val analz_Fake_tac =
dtac OR2_analz_sees_Spy 4 THEN
dtac OR4_analz_sees_Spy 6 THEN
- forward_tac [Says_Server_message_form] 7 THEN
- assume_tac 7 THEN Full_simp_tac 7 THEN
+ forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
-
****)
(** Session keys are not used to encrypt other session keys **)
-(*Lemma for the trivial direction of the if-and-only-if*)
-goal thy
- "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
-\ (K : nE | Key K : analz sEe) ==> \
-\ (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
-val lemma = result();
-
-
(*The equality makes the induction hypothesis easier to apply*)
goal thy
"!!evs. evs : otway ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
-\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (ares_tac [allI, lemma]));
-by (ALLGOALS (*Takes 18 secs*)
- (asm_simp_tac
- (!simpset addsimps [Un_assoc RS sym,
- insert_Key_singleton, insert_Key_image, pushKey_newK]
- setloop split_tac [expand_if])));
-(*OR4, OR2, Fake*)
-by (EVERY (map spy_analz_tac [5,3,2]));
-(*Oops, OR3, Base*)
-by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
-qed_spec_mp "analz_image_newK";
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Base*)
+by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+(*Fake, OR2, OR4*)
+by (REPEAT (spy_analz_tac 1));
+qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. evs : otway ==> \
-\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
-\ (K = newK i | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
(*** The Key K uniquely identifies the Server's message. **)
@@ -301,8 +214,8 @@
by (Fast_tac 2);
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a very new message, and handle this case by contradiction*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+(*...we assume X is a recent message, and handle this case by contradiction*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs
delrules [conjI] (*prevent split-up into 4 subgoals*)
addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
@@ -328,27 +241,28 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
- analz_insert_Key_newK]
- setloop split_tac [expand_if])));
+ (asm_simp_tac (!simpset addcongs [conj_cong]
+ addsimps [not_parts_not_analz, analz_insert_freshK]
+ setloop split_tac [expand_if])));
(*OR3*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+by (fast_tac (!claset delrules [impCE]
+ addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]
addss (!simpset addsimps [parts_insert2])) 3);
(*OR4, OR2, Fake*)
by (REPEAT_FIRST spy_analz_tac);
(*Oops*) (** LEVEL 5 **)
by (fast_tac (!claset delrules [disjE]
- addDs [unique_session_keys] addss (!simpset)) 1);
+ addDs [unique_session_keys] addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
-
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, K|}, \
-\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
+ "!!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; \
\ A ~: lost; B ~: lost; evs : otway |] \
-\ ==> K ~: analz (sees lost Spy evs)";
+\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -359,9 +273,9 @@
(*Only OR1 can have caused such a part of a message to appear.
I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
Perhaps it's because OR2 has two similar-looking encrypted messages in
- this version.*)
+ this version.*)
goal thy
- "!!evs. [| A ~: lost; A ~= B; evs : otway |] \
+ "!!evs. [| A ~: lost; A ~= B; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
\ : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
@@ -390,15 +304,13 @@
by (parts_induct_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
+ addSEs sees_Spy_partsEs
addss (!simpset)) 1);
(*OR4*)
by (REPEAT (Safe_step_tac 2));
by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
by (fast_tac (!claset addSIs [Crypt_imp_OR1]
- addEs partsEs
- addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
+ addEs sees_Spy_partsEs) 2);
(*OR3*) (** LEVEL 5 **)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
by (step_tac (!claset delrules [disjCI, impCE]) 1);
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Jan 17 12:49:31 1997 +0100
@@ -27,26 +27,25 @@
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway; A ~= B; B ~= Server |]
- ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B,
- Crypt (shrK A)
- {|Nonce (newN(length evs)), Agent A, Agent B|} |}
+ OR1 "[| evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs |]
+ ==> Says A B {|Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs : otway"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.
We modify the published protocol by NOT encrypting NB.*)
- OR2 "[| evs: otway; B ~= Server;
+ OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs;
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
==> Says B Server
- {|Nonce NA, Agent A, Agent B, X, Nonce (newN(length evs)),
+ {|Nonce NA, Agent A, Agent B, X, Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
# evs : otway"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs: otway; B ~= Server;
+ OR3 "[| evs: otway; B ~= Server; Key KAB ~: used evs;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
@@ -55,16 +54,16 @@
: set_of_list evs |]
==> Says Server B
{|Nonce NA,
- Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
- Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
+ Crypt (shrK A) {|Nonce NA, Key KAB|},
+ Crypt (shrK B) {|Nonce NB, Key KAB|}|}
# evs : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
OR4 "[| evs: otway; A ~= B;
- Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
: set_of_list evs;
- Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
+ Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs |]
==> Says B A {|Nonce NA, X|} # evs : otway"
--- a/src/HOL/Auth/Public.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Public.ML Fri Jan 17 12:49:31 1997 +0100
@@ -158,18 +158,20 @@
AddIffs [Nonce_notin_initState];
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
-be (impOfSubs parts_mono) 1;
+by (etac (impOfSubs parts_mono) 1);
by (Fast_tac 1);
qed "usedI";
AddIs [usedI];
-(*Yields a supply of fresh nonces for possibility theorems.*)
+(** A supply of fresh nonces for possibility theorems. **)
+
goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
by (list.induct_tac "evs" 1);
by (res_inst_tac [("x","0")] exI 1);
by (Step_tac 1);
by (Full_simp_tac 1);
+(*Inductive step*)
by (event.induct_tac "a" 1);
by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
by (msg.induct_tac "msg" 1);
@@ -184,11 +186,18 @@
val lemma = result();
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
-br (lemma RS exE) 1;
-br selectI 1;
+by (rtac (lemma RS exE) 1);
+by (rtac selectI 1);
by (Fast_tac 1);
qed "Nonce_supply";
+(*Tactic for possibility theorems*)
+val possibility_tac =
+ REPEAT
+ (ALLGOALS (simp_tac (!simpset setsolver safe_solver))
+ THEN
+ REPEAT_FIRST (eq_assume_tac ORELSE'
+ resolve_tac [refl, conjI, Nonce_supply]));
(** Power of the Spy **)
--- a/src/HOL/Auth/Recur.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Recur.ML Fri Jan 17 12:49:31 1997 +0100
@@ -10,29 +10,26 @@
proof_timing:=true;
HOL_quantifiers := false;
-Pretty.setdepth 25;
+Pretty.setdepth 30;
(** Possibility properties: traces that reach the end
- ONE theorem would be more elegant and faster!
- By induction on a list of agents (no repetitions)
+ ONE theorem would be more elegant and faster!
+ By induction on a list of agents (no repetitions)
**)
+
(*Simplest case: Alice goes directly to the server*)
goal thy
"!!A. A ~= Server \
\ ==> EX K NA. EX evs: recur lost. \
-\ Says Server A {|Agent A, \
-\ Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
+\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
\ Agent Server|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS
- (respond.One RSN (4,recur.RA3))) 2);
-by (REPEAT
- (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
- THEN
- REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])));
+ (respond.One RSN (4,recur.RA3))) 2);
+by possibility_tac;
result();
@@ -40,44 +37,42 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
-\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} \
\ : set_of_list evs";
+by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
+by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS
- (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
- recur.RA4) 2);
-bw HPair_def;
-by (REPEAT
- (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
- THEN
- ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
+ (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
+ recur.RA4) 2);
+by basic_possibility_tac;
+by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2,
+ less_not_refl2 RS not_sym] 1));
result();
-(*Case three: Alice, Bob, Charlie and the server*)
+(*Case three: Alice, Bob, Charlie and the server
goal thy
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+ "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
-\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} \
\ : set_of_list evs";
+by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
+by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
- (respond.One RS respond.Cons RS respond.Cons RSN
- (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
-bw HPair_def;
-by (REPEAT (*SLOW: 37 seconds*)
- (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
- THEN
- ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
-by (ALLGOALS
- (SELECT_GOAL (DEPTH_SOLVE
- (swap_res_tac [refl, conjI, disjI1, disjI2] 1 APPEND
- etac not_sym 1))));
+ (respond.One RS respond.Cons RS respond.Cons RSN
+ (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
+(*SLOW: 70 seconds*)
+by basic_possibility_tac;
+by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1
+ ORELSE
+ eresolve_tac [asm_rl, less_not_refl2,
+ less_not_refl2 RS not_sym] 1));
result();
-
-
+****************)
(**** Inductive proofs about recur ****)
@@ -99,10 +94,30 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
+
+goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
+by (etac respond.induct 1);
+by (ALLGOALS Simp_tac);
+qed "respond_Key_in_parts";
+
+goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
+by (etac respond.induct 1);
+by (REPEAT (assume_tac 1));
+qed "respond_imp_not_used";
+
+goal thy
+ "!!evs. [| Key K : parts {RB}; (PB,RB,K') : respond evs |] \
+\ ==> Key K ~: used evs";
+by (etac rev_mp 1);
+by (etac respond.induct 1);
+by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
+ !simpset));
+qed_spec_mp "Key_in_parts_respond";
+
(*Simple inductive reasoning about responses*)
-goal thy "!!j. (j,PA,RB) : respond i ==> RB : responses i";
+goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
by (etac respond.induct 1);
-by (REPEAT (ares_tac responses.intrs 1));
+by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
qed "respond_imp_responses";
@@ -110,7 +125,7 @@
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
-goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \
+goal thy "!!evs. Says C' B {|X, X', RA|} : set_of_list evs \
\ ==> RA : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "RA4_analz_sees_Spy";
@@ -131,8 +146,8 @@
let val tac = forw_inst_tac [("lost","lost")]
in tac RA2_parts_sees_Spy 4 THEN
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN
- forward_tac [respond_imp_responses] 5 THEN
- tac RA4_parts_sees_Spy 6
+ forward_tac [respond_imp_responses] 5 THEN
+ tac RA4_parts_sees_Spy 6
end;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
@@ -153,14 +168,6 @@
(** Spy never sees another agent's long-term key (unless initially lost) **)
goal thy
- "!!evs. (j,PB,RB) : respond i \
-\ ==> Key K : parts {RB} --> (EX j'. K = newK2(i,j') & j<=j')";
-be respond.induct 1;
-by (Auto_tac());
-by (best_tac (!claset addDs [Suc_leD]) 1);
-qed_spec_mp "Key_in_parts_respond";
-
-goal thy
"!!evs. evs : recur lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
by (parts_induct_tac 1);
@@ -189,115 +196,30 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
+
+(** Nobody can have used non-existent keys! **)
-(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : recur lost ==> \
-\ length evs <= i --> \
-\ Key (newK2(i,j)) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-(*RA2*)
-by (best_tac (!claset addSEs partsEs
- addSDs [parts_cut]
- addDs [Suc_leD]
- addss (!simpset)) 3);
-(*Fake*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset)) 1);
-(*For RA3*)
-by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
-(*RA1-RA4*)
-by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD]
- addss (!simpset)) 1));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK2(i,j)) : parts {X}; \
-\ evs : recur lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-(*** Future nonces can't be seen or used! ***)
-
-goal thy
- "!!evs. (j, PB, RB) : respond i \
-\ ==> Nonce N : parts {RB} --> Nonce N : parts {PB}";
-be respond.induct 1;
+goal thy
+ "!!evs. [| K : keysFor (parts {RB}); (PB,RB,K') : respond evs |] \
+\ ==> K : range shrK";
+by (etac rev_mp 1);
+by (etac (respond_imp_responses RS responses.induct) 1);
by (Auto_tac());
-qed_spec_mp "Nonce_in_parts_respond";
+qed_spec_mp "Key_in_keysFor_parts";
-goal thy "!!i. evs : recur lost ==> \
-\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-(*For RA3*)
-by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4);
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
- addDs [Nonce_in_parts_respond, parts_cut, Suc_leD]
- addss (!simpset)) 0 4);
-(*Fake*)
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset)) 1);
-(*RA1, RA2, RA4*)
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addEs [leD RS notE]
- addDs [Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-(*Variant: old messages must contain old nonces!*)
-goal thy "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN i) : parts {X}; \
-\ evs : recur lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_nonces";
-
-
-(** Nobody can have USED keys that will be generated in the future. **)
-
-goal thy
- "!!evs. (j,PB,RB) : respond i \
-\ ==> K : keysFor (parts {RB}) --> (EX A. K = shrK A)";
-be (respond_imp_responses RS responses.induct) 1;
-by (Auto_tac());
-qed_spec_mp "Key_in_keysFor_parts_respond";
-
-
-goal thy "!!i. evs : recur lost ==> \
-\ length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!evs. evs : recur lost ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
(*RA3*)
-by (fast_tac (!claset addDs [Key_in_keysFor_parts_respond, Suc_leD]
- addss (!simpset addsimps [parts_insert_sees])) 4);
-(*RA2*)
-by (fast_tac (!claset addSEs partsEs
- addDs [Suc_leD] addss (!simpset)) 3);
-(*Fake, RA1, RA4*)
-by (REPEAT
- (best_tac
- (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset)) 1));
+by (best_tac (!claset addDs [Key_in_keysFor_parts]
+ addss (!simpset addsimps [parts_insert_sees])) 2);
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
@@ -319,86 +241,82 @@
dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
-Delsimps [image_insert];
-
(** Session keys are not used to encrypt other session keys **)
(*Version for "responses" relation. Handles case RA3 in the theorem below.
Note that it holds for *any* set H (not just "sees lost Spy evs")
satisfying the inductive hypothesis.*)
goal thy
- "!!evs. [| RB : responses i; \
-\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
-\ (K : newK``I | Key K : analz H) |] \
-\ ==> ALL K I. (Key K : analz (insert RB (Key``(newK``I) Un H))) = \
-\ (K : newK``I | Key K : analz (insert RB H))";
-be responses.induct 1;
-by (ALLGOALS
- (asm_simp_tac
- (!simpset addsimps [insert_Key_singleton, insert_Key_image,
- Un_assoc RS sym, pushKey_newK]
- setloop split_tac [expand_if])));
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
-qed "resp_analz_image_newK_lemma";
+ "!!evs. [| RB : responses evs; \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un H)) = \
+\ (K : KK | Key K : analz H) |] \
+\ ==> ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (insert RB (Key``KK Un H))) = \
+\ (K : KK | Key K : analz (insert RB H))";
+by (etac responses.induct 1);
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+qed "resp_analz_image_freshK_lemma";
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
goal thy
- "!!evs. evs : recur lost ==> \
-\ ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \
-\ (K : newK``I | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : recur lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac recur.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (ALLGOALS
+ (asm_simp_tac
+ (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
(*Base*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
(*RA4, RA2, Fake*)
by (REPEAT (spy_analz_tac 1));
-val raw_analz_image_newK = result();
-qed_spec_mp "analz_image_newK";
+val raw_analz_image_freshK = result();
+qed_spec_mp "analz_image_freshK";
(*Instance of the lemma with H replaced by (sees lost Spy evs):
- [| RB : responses i; evs : recur lost |]
- ==> Key xa : analz (insert RB (Key``newK``x Un sees lost Spy evs)) =
- (xa : newK``x | Key xa : analz (insert RB (sees lost Spy evs)))
+ [| RB : responses evs; evs : recur lost; |]
+ ==> KK <= Compl (range shrK) -->
+ Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
+ (K : KK | Key K : analz (insert RB (sees lost Spy evs)))
*)
-bind_thm ("resp_analz_image_newK",
- raw_analz_image_newK RSN
- (2, resp_analz_image_newK_lemma) RS spec RS spec);
+bind_thm ("resp_analz_image_freshK",
+ raw_analz_image_freshK RSN
+ (2, resp_analz_image_freshK_lemma) RS spec RS spec);
goal thy
- "!!evs. evs : recur lost ==> \
-\ Key K : analz (insert (Key (newK x)) (sees lost Spy evs)) = \
-\ (K = newK x | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : recur lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
-(*This is more general than proving Hash_new_nonces_not_seen: we don't prove
- that "future nonces" can't be hashed, but that everything that's hashed is
- already in past traffic. *)
+(*Everything that's hashed is already in past traffic. *)
goal thy "!!i. [| evs : recur lost; A ~: lost |] ==> \
\ Hash {|Key(shrK A), X|} : parts (sees lost Spy evs) --> \
\ X : parts (sees lost Spy evs)";
-be recur.induct 1;
+by (etac recur.induct 1);
by parts_Fake_tac;
(*RA3 requires a further induction*)
-be responses.induct 5;
+by (etac responses.induct 5);
by (ALLGOALS Asm_simp_tac);
(*Fake*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset addsimps [parts_insert_sees])) 2);
+ impOfSubs Fake_parts_insert]
+ addss (!simpset addsimps [parts_insert_sees])) 2);
(*Two others*)
by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
bind_thm ("Hash_imp_body", result() RSN (2, rev_mp));
(** The Nonce NA uniquely identifies A's message.
- This theorem applies to rounds RA1 and RA2!
+ This theorem applies to steps RA1 and RA2!
Unicity is not used in other proofs but is desirable in its own right.
**)
@@ -409,29 +327,20 @@
\ Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
\ : parts (sees lost Spy evs) --> B=B' & P=P'";
by (parts_induct_tac 1);
-be responses.induct 3;
+by (etac responses.induct 3);
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
by (step_tac (!claset addSEs partsEs) 1);
-(*RA1: creation of new Nonce. Move assertion into global context*)
-by (expand_case_tac "NA = ?y" 1);
-by (best_tac (!claset addSIs [exI]
- addSDs [Hash_imp_body]
- addSEs (new_nonces_not_seen::partsEs)
- addss (!simpset)) 1);
-by (best_tac (!claset addss (!simpset)) 1);
-(*RA2: creation of new Nonce*)
-by (expand_case_tac "NA = ?y" 1);
-by (best_tac (!claset addSIs [exI]
- addSDs [Hash_imp_body]
- addSEs (new_nonces_not_seen::partsEs)
- addss (!simpset)) 1);
-by (best_tac (!claset addss (!simpset)) 1);
+(*RA1,2: creation of new Nonce. Move assertion into global context*)
+by (ALLGOALS (expand_case_tac "NA = ?y"));
+by (REPEAT_FIRST (ares_tac [exI]));
+by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
+ addSEs sees_Spy_partsEs) 1));
val lemma = result();
goalw thy [HPair_def]
- "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|} \
+ "!!evs.[| Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} \
\ : parts (sees lost Spy evs); \
-\ HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \
+\ Hash[Key(shrK A)] {|Agent A, Agent B', Nonce NA, P'|} \
\ : parts (sees lost Spy evs); \
\ evs : recur lost; A ~: lost |] \
\ ==> B=B' & P=P'";
@@ -445,39 +354,36 @@
***)
goal thy
- "!!evs. [| RB : responses i; evs : recur lost |] \
+ "!!evs. [| RB : responses evs; evs : recur lost |] \
\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
-be responses.induct 1;
+by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [resp_analz_image_newK, insert_Key_singleton]
- setloop split_tac [expand_if])));
+ (analz_image_freshK_ss addsimps [Spy_analz_shrK,
+ resp_analz_image_freshK])));
qed "shrK_in_analz_respond";
Addsimps [shrK_in_analz_respond];
goal thy
- "!!evs. [| RB : responses i; \
-\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
-\ (K : newK``I | Key K : analz H) |] \
+ "!!evs. [| RB : responses evs; \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un H)) = \
+\ (K : KK | Key K : analz H) |] \
\ ==> (Key K : analz (insert RB H)) --> \
-\ (Key K : parts{RB} | Key K : analz H)";
-be responses.induct 1;
+\ (Key K : parts{RB} | Key K : analz H)";
+by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [read_instantiate [("H", "?ff``?xx")] parts_insert,
- resp_analz_image_newK_lemma,
- insert_Key_singleton, insert_Key_image,
- Un_assoc RS sym, pushKey_newK]
- setloop split_tac [expand_if])));
-(*The "Message" simpset gives the standard treatment of "image"*)
-by (simp_tac (simpset_of "Message") 1);
+ (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
+(*Simplification using two distinct treatments of "image"*)
+by (simp_tac (!simpset addsimps [parts_insert2]) 1);
by (fast_tac (!claset delrules [allE]) 1);
qed "resp_analz_insert_lemma";
bind_thm ("resp_analz_insert",
- raw_analz_image_newK RSN
- (2, resp_analz_insert_lemma) RSN(2, rev_mp));
+ raw_analz_image_freshK RSN
+ (2, resp_analz_insert_lemma) RSN(2, rev_mp));
(*The Server does not send such messages. This theorem lets us avoid
@@ -487,44 +393,51 @@
\ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
\ ~: set_of_list evs";
by (etac recur.induct 1);
-be (respond.induct) 5;
+by (etac (respond.induct) 5);
by (Auto_tac());
qed_spec_mp "Says_Server_not";
AddSEs [Says_Server_not RSN (2,rev_notE)];
+(*The last key returned by respond indeed appears in a certificate*)
goal thy
- "!!i. (j,PB,RB) : respond i \
-\ ==> EX A' B'. ALL A B N. \
+ "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
+\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
+by (etac respond.elim 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "respond_certificate";
+
+
+goal thy
+ "!!K'. (PB,RB,KXY) : respond evs \
+\ ==> EX A' B'. ALL A B N. \
\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
\ --> (A'=A & B'=B) | (A'=B & B'=A)";
-be respond.induct 1;
+by (etac respond.induct 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib])));
(*Base case*)
by (Fast_tac 1);
by (Step_tac 1);
+(*Case analysis on K=KBC*)
by (expand_case_tac "K = ?y" 1);
+by (dtac respond_Key_in_parts 1);
by (best_tac (!claset addSIs [exI]
addSEs partsEs
- addDs [Key_in_parts_respond]
- addss (!simpset)) 1);
+ addDs [Key_in_parts_respond]) 1);
+(*Case analysis on K=KAB*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [exI] 2));
by (ex_strip_tac 1);
-be respond.elim 1;
-by (REPEAT_FIRST (etac Pair_inject ORELSE' hyp_subst_tac));
-by (ALLGOALS (asm_full_simp_tac
- (!simpset addsimps [all_conj_distrib, ex_disj_distrib])));
-by (Fast_tac 1);
+by (dtac respond_certificate 1);
by (Fast_tac 1);
val lemma = result();
goal thy
"!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
-\ (j,PB,RB) : respond i |] \
+\ (PB,RB,KXY) : respond evs |] \
\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
-by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*)
+by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*)
qed "unique_session_keys";
@@ -533,47 +446,34 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \
-\ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}";
-be respond.elim 1;
-by (ALLGOALS Asm_full_simp_tac);
-qed "newK2_respond_lemma";
-
-
-goal thy
- "!!evs. [| (j,PB,RB) : respond (length evs); evs : recur lost |] \
+ "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur lost |] \
\ ==> ALL A A' N. A ~: lost & A' ~: lost --> \
\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
\ Key K ~: analz (insert RB (sees lost Spy evs))";
-be respond.induct 1;
+by (etac respond.induct 1);
by (forward_tac [respond_imp_responses] 2);
-by (ALLGOALS (*4 MINUTES???*)
+by (forward_tac [respond_imp_not_used] 2);
+by (ALLGOALS (*43 seconds*)
(asm_simp_tac
- (!simpset addsimps
- ([analz_image_newK, not_parts_not_analz,
- read_instantiate [("H", "?ff``?xx")] parts_insert,
- Un_assoc RS sym, resp_analz_image_newK,
- insert_Key_singleton, analz_insert_Key_newK])
- setloop split_tac [expand_if])));
-by (ALLGOALS (simp_tac (simpset_of "Message")));
-by (Fast_tac 1);
+ (analz_image_freshK_ss addsimps
+ [analz_image_freshK, not_parts_not_analz,
+ shrK_in_analz_respond,
+ read_instantiate [("H", "?ff``?xx")] parts_insert,
+ resp_analz_image_freshK, analz_insert_freshK])));
+by (ALLGOALS Simp_tac);
+by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
by (step_tac (!claset addSEs [MPair_parts]) 1);
-(** LEVEL 6 **)
-by (fast_tac (!claset addDs [resp_analz_insert, Key_in_parts_respond]
- addSEs [new_keys_not_seen RS not_parts_not_analz
- RSN(2,rev_notE)]
- addss (!simpset)) 4);
-by (fast_tac (!claset addSDs [newK2_respond_lemma]) 3);
+(** LEVEL 7 **)
+by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
+ addDs [impOfSubs analz_subset_parts]) 4);
+by (fast_tac (!claset addSDs [respond_certificate]) 3);
by (best_tac (!claset addSEs partsEs
addDs [Key_in_parts_respond]
addss (!simpset)) 2);
-by (thin_tac "ALL x.?P(x)" 1);
-be respond.elim 1;
-by (fast_tac (!claset addss (!simpset)) 1);
-by (step_tac (!claset addss (!simpset)) 1);
-by (best_tac (!claset addSEs partsEs
- addDs [Key_in_parts_respond]
- addss (!simpset)) 1);
+by (dtac unique_session_keys 1);
+by (etac respond_certificate 1);
+by (assume_tac 1);
+by (Fast_tac 1);
qed_spec_mp "respond_Spy_not_see_encrypted_key";
@@ -586,7 +486,7 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
+ (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
setloop split_tac [expand_if])));
(*RA4*)
by (spy_analz_tac 4);
@@ -596,13 +496,14 @@
(*RA2*)
by (spy_analz_tac 1);
(*RA3, case 2: K is an old key*)
-by (fast_tac (!claset addSDs [resp_analz_insert]
- addSEs partsEs
- addDs [Key_in_parts_respond]
- addEs [Says_imp_old_keys RS less_irrefl]) 2);
+by (best_tac (!claset addSDs [resp_analz_insert]
+ addSEs partsEs
+ addDs [Key_in_parts_respond,
+ Says_imp_sees_Spy RS parts.Inj RSN (2, parts_cut)]
+ addss (!simpset)) 2);
(*RA3, case 1: use lemma previously proved by induction*)
by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN
- (2,rev_notE)]) 1);
+ (2,rev_notE)]) 1);
bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp));
@@ -622,34 +523,29 @@
(**** Authenticity properties for Agents ****)
(*The response never contains Hashes*)
-(*NEEDED????????????????*)
goal thy
- "!!evs. (j,PB,RB) : respond i \
+ "!!evs. (PB,RB,K) : respond evs \
\ ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
\ Hash {|Key (shrK B), M|} : parts H";
-be (respond_imp_responses RS responses.induct) 1;
+by (etac (respond_imp_responses RS responses.induct) 1);
by (Auto_tac());
bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
-(*NEEDED????????????????*)
(*Only RA1 or RA2 can have caused such a part of a message to appear.*)
goalw thy [HPair_def]
"!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \
\ : parts (sees lost Spy evs); \
\ A ~: lost; evs : recur lost |] \
-\ ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|}) \
+\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \
\ : set_of_list evs";
-be rev_mp 1;
+by (etac rev_mp 1);
by (parts_induct_tac 1);
(*RA3*)
by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
qed_spec_mp "Hash_auth_sender";
-val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
-
-
-(** These two results should subsume (for all agents) the guarantees proved
+(** These two results subsume (for all agents) the guarantees proved
separately for A and B in the Otway-Rees protocol.
**)
--- a/src/HOL/Auth/Recur.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Recur.thy Fri Jan 17 12:49:31 1997 +0100
@@ -8,56 +8,47 @@
Recur = Shared +
-syntax
- newK2 :: "nat*nat => key"
-
-translations
- "newK2 x" == "newK(nPair x)"
-
(*Two session keys are distributed to each agent except for the initiator,
- who receives one.
+ who receives one.
Perhaps the two session keys could be bundled into a single message.
*)
-consts respond :: "nat => (nat*msg*msg)set"
-inductive "respond i" (*Server's response to the nested message*)
+consts respond :: "event list => (msg*msg*key)set"
+inductive "respond evs" (*Server's response to the nested message*)
intrs
(*The message "Agent Server" marks the end of a list.*)
- One "A ~= Server
- ==> (j, HPair (Key(shrK A))
+ One "[| A ~= Server; Key KAB ~: used evs |]
+ ==> (Hash[Key(shrK A)]
{|Agent A, Agent B, Nonce NA, Agent Server|},
- {|Agent A,
- Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|},
- Agent Server|})
- : respond i"
+ {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
+ KAB) : respond evs"
(*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
- Cons "[| (Suc j, PA, RA) : respond i;
- PA = HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|};
+ Cons "[| (PA, RA, KAB) : respond evs;
+ Key KBC ~: used evs; Key KBC ~: parts {RA};
+ PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
B ~= Server |]
- ==> (j, HPair (Key(shrK B)) {|Agent B, Agent C, Nonce NB, PA|},
- {|Agent B,
- Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|},
- Agent B,
- Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|},
- RA|})
- : respond i"
+ ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|},
+ {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
+ Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
+ RA|},
+ KBC)
+ : respond evs"
(*Induction over "respond" can be difficult due to the complexity of the
subgoals. The "responses" relation formalizes the general form of its
third component.
*)
-consts responses :: nat => msg set
-inductive "responses i"
+consts responses :: event list => msg set
+inductive "responses evs"
intrs
(*Server terminates lists*)
- Nil "Agent Server : responses i"
+ Nil "Agent Server : responses evs"
- Cons "RA : responses i
- ==> {|Agent B,
- Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|},
- RA|} : responses i"
+ Cons "[| RA : responses evs; Key KAB ~: used evs |]
+ ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
+ RA|} : responses evs"
consts recur :: agent set => event list set
@@ -75,40 +66,36 @@
(*Alice initiates a protocol run.
"Agent Server" is just a placeholder, to terminate the nesting.*)
- RA1 "[| evs: recur lost; A ~= B; A ~= Server |]
+ RA1 "[| evs: recur lost; A ~= B; A ~= Server; Nonce NA ~: used evs |]
==> Says A B
- (HPair (Key(shrK A))
- {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|})
+ (Hash[Key(shrK A)]
+ {|Agent A, Agent B, Nonce NA, Agent Server|})
# evs : recur lost"
(*Bob's response to Alice's message. C might be the Server.
XA should be the Hash of the remaining components with KA, but
- Bob cannot check that.
+ Bob cannot check that.
P is the previous recur message from Alice's caller.
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;
+ 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;
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
- ==> Says B C
- (HPair (Key(shrK B))
- {|Agent B, Agent C, Nonce (newN(length evs)), PA|})
+ ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
# evs : recur lost"
(*The Server receives and decodes Bob's message. Then he generates
a new session key and a response.*)
RA3 "[| evs: recur lost; B ~= Server;
Says B' Server PB : set_of_list evs;
- (0,PB,RB) : respond (length evs) |]
+ (PB,RB,K) : respond evs |]
==> Says Server B RB # evs : recur lost"
(*Bob receives the returned message and compares the Nonces with
- those in the message he previously sent the Server.*)
+ those in the message he previously sent the Server.*)
RA4 "[| evs: recur lost; A ~= B;
- Says C' B {|Agent B,
- Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
- Agent B,
- Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|}
+ Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
+ Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|}
: set_of_list evs;
Says B C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|}
--- a/src/HOL/Auth/Shared.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Shared.ML Fri Jan 17 12:49:31 1997 +0100
@@ -28,18 +28,16 @@
(*Injectiveness and freshness of new keys and nonces*)
AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq,
- inj_newK RS inj_eq, inj_nPair RS inj_eq];
+ inj_newK RS inj_eq, inj_nPair RS inj_eq];
(* invKey (shrK A) = shrK A *)
-bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
+bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys);
-(* invKey (newK i) = newK i *)
-bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
-Addsimps [invKey_shrK, invKey_newK];
+Addsimps [invKey_id];
goal thy "!!K. newK i = invKey K ==> newK i = K";
by (rtac (invKey_eq RS iffD1) 1);
-by (Simp_tac 1);
+by (Full_simp_tac 1);
val newK_invKey = result();
AddSDs [newK_invKey, sym RS newK_invKey];
@@ -54,12 +52,7 @@
by (Auto_tac ());
qed "newK_notin_initState";
-goal thy "Nonce (newN i) ~: parts (initState lost B)";
-by (agent.induct_tac "B" 1);
-by (Auto_tac ());
-qed "newN_notin_initState";
-
-AddIffs [newK_notin_initState, newN_notin_initState];
+AddIffs [newK_notin_initState];
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
by (agent.induct_tac "C" 1);
@@ -156,6 +149,10 @@
by (Auto_tac ());
qed_spec_mp "Says_imp_sees_Spy";
+(*Use with addSEs to derive contradictions from old Says events containing
+ items known to be fresh*)
+val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
+
goal thy
"!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; C : lost |] \
\ ==> X : analz (sees lost Spy evs)";
@@ -194,6 +191,181 @@
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
+(*** Fresh nonces ***)
+
+goal thy "Nonce N ~: parts (initState lost B)";
+by (agent.induct_tac "B" 1);
+by (Auto_tac ());
+qed "Nonce_notin_initState";
+
+AddIffs [Nonce_notin_initState];
+
+goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
+by (etac (impOfSubs parts_mono) 1);
+by (Fast_tac 1);
+qed "usedI";
+
+AddIs [usedI];
+
+(** Fresh keys never clash with long-term shared keys **)
+
+goal thy "Key (shrK A) : used evs";
+by (Best_tac 1);
+qed "shrK_in_used";
+AddIffs [shrK_in_used];
+
+(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys
+ from long-term shared keys*)
+goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
+by (Best_tac 1);
+qed "Key_not_used";
+
+(*A session key cannot clash with a long-term shared key*)
+goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
+by (Fast_tac 1);
+qed "shrK_neq";
+
+Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
+
+
+goal thy "used (Says A B X # evs) = parts{X} Un used evs";
+by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
+qed "used_Says";
+Addsimps [used_Says];
+
+goal thy "used [] <= used l";
+by (list.induct_tac "l" 1);
+by (event.induct_tac "a" 2);
+by (ALLGOALS Asm_simp_tac);
+by (Best_tac 1);
+qed "used_nil_subset";
+
+goal thy "used l <= used (l@l')";
+by (list.induct_tac "l" 1);
+by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
+by (event.induct_tac "a" 1);
+by (Asm_simp_tac 1);
+by (Best_tac 1);
+qed "used_subset_append";
+
+
+(*** Supply fresh nonces for possibility theorems. ***)
+
+goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+by (list.induct_tac "evs" 1);
+by (res_inst_tac [("x","0")] exI 1);
+by (Step_tac 1);
+by (Full_simp_tac 1);
+(*Inductive step*)
+by (event.induct_tac "a" 1);
+by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
+by (msg.induct_tac "msg" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
+by (Step_tac 1);
+(*MPair case*)
+by (res_inst_tac [("x","Na+Nb")] exI 2);
+by (fast_tac (!claset addSEs [add_leE]) 2);
+(*Nonce case*)
+by (res_inst_tac [("x","N + Suc nat")] exI 1);
+by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
+val lemma = result();
+
+goal thy "EX N. Nonce N ~: used evs";
+by (rtac (lemma RS exE) 1);
+by (Fast_tac 1);
+qed "Nonce_supply1";
+
+goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
+by (cut_inst_tac [("evs","evs")] lemma 1);
+by (cut_inst_tac [("evs","evs'")] lemma 1);
+by (Step_tac 1);
+by (res_inst_tac [("x","N")] exI 1);
+by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
+by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym,
+ le_add2, le_add1,
+ le_eq_less_Suc RS sym]) 1);
+qed "Nonce_supply2";
+
+goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
+\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
+by (cut_inst_tac [("evs","evs")] lemma 1);
+by (cut_inst_tac [("evs","evs'")] lemma 1);
+by (cut_inst_tac [("evs","evs''")] lemma 1);
+by (Step_tac 1);
+by (res_inst_tac [("x","N")] exI 1);
+by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
+by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
+by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym,
+ le_add2, le_add1,
+ le_eq_less_Suc RS sym]) 1);
+by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
+by (stac (le_eq_less_Suc RS sym) 1);
+by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2);
+by (REPEAT (rtac le_add1 1));
+qed "Nonce_supply3";
+
+goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
+by (rtac (lemma RS exE) 1);
+by (rtac selectI 1);
+by (Fast_tac 1);
+qed "Nonce_supply";
+
+(*** Supply fresh keys for possibility theorems. ***)
+
+goal thy "EX K. Key K ~: used evs";
+by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
+by (Fast_tac 1);
+qed "Key_supply1";
+
+val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
+
+goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
+by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
+by (etac exE 1);
+by (cut_inst_tac [("evs","evs'")]
+ (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
+by (Auto_tac());
+qed "Key_supply2";
+
+goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
+\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
+by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
+by (etac exE 1);
+by (cut_inst_tac [("evs","evs'")]
+ (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
+by (etac exE 1);
+by (cut_inst_tac [("evs","evs''")]
+ (Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
+by (Step_tac 1);
+by (Full_simp_tac 1);
+by (fast_tac (!claset addSEs [allE]) 1);
+qed "Key_supply3";
+
+goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
+by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
+by (rtac selectI 1);
+by (Fast_tac 1);
+qed "Key_supply";
+
+(*** Tactics for possibility theorems ***)
+
+val possibility_tac =
+ REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
+ (ALLGOALS (simp_tac
+ (!simpset delsimps [used_Says] setsolver safe_solver))
+ THEN
+ REPEAT_FIRST (eq_assume_tac ORELSE'
+ resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
+
+(*For harder protocols (such as Recur) where we have to set up some
+ nonces and keys initially*)
+val basic_possibility_tac =
+ REPEAT
+ (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
+ THEN
+ REPEAT_FIRST (resolve_tac [refl, conjI]));
+
+
(** Power of the Spy **)
(*The Spy can see more than anybody else, except for their initial state*)
@@ -227,25 +399,35 @@
(*Push newK applications in, allowing other keys to be pulled out*)
val pushKey_newK = insComm thy "Key (newK ?evs)" "Key (shrK ?C)";
-Delsimps [image_insert];
-Addsimps [image_insert RS sym];
-
-Delsimps [image_Un];
-Addsimps [image_Un RS sym];
-
-goal thy "insert (Key (newK x)) H = Key `` (newK``{x}) Un H";
+goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
by (Fast_tac 1);
-qed "insert_Key_singleton";
+qed "subset_Compl_range";
goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
\ Key `` (f `` (insert x E)) Un C";
by (Fast_tac 1);
qed "insert_Key_image";
+goal thy "insert (Key K) H = Key `` {K} Un H";
+by (Fast_tac 1);
+qed "insert_Key_singleton";
+
+goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
+by (Fast_tac 1);
+qed "insert_Key_image'";
+
+val analz_image_freshK_ss =
+ !simpset delsimps [image_insert, image_Un]
+ addsimps ([image_insert RS sym, image_Un RS sym,
+ Key_not_used,
+ insert_Key_singleton, subset_Compl_range,
+ insert_Key_image', Un_assoc RS sym]
+ @disj_comms)
+ setloop split_tac [expand_if];
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
"!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \
\ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
-qed "analz_image_newK_lemma";
+qed "analz_image_freshK_lemma";
--- a/src/HOL/Auth/Shared.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Shared.thy Fri Jan 17 12:49:31 1997 +0100
@@ -8,13 +8,14 @@
Server keys; initial states of agents; new nonces and keys; function "sees"
*)
-Shared = Message + List +
+Shared = Message + List + Finite +
consts
shrK :: agent => key (*symmetric keys*)
rules
- isSym_shrK "isSymKey (shrK A)"
+ (*ALL keys are symmetric*)
+ isSym_keys "isSymKey K"
consts (*Initial states of agents -- parameter of the construction*)
initState :: [agent set, agent] => msg set
@@ -44,6 +45,23 @@
sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
+constdefs
+ (*Set of items that might be visible to somebody: complement of the set
+ of fresh items*)
+ used :: event list => msg set
+ "used evs == parts (UN lost B. sees lost B evs)"
+
+
+rules
+ (*Unlike the corresponding property of nonces, this cannot be proved.
+ We have infinitely many agents and there is nothing to stop their
+ long-term keys from exhausting all the natural numbers. The axiom
+ assumes that their keys are dispersed so as to leave room for infinitely
+ many fresh session keys. We could, alternatively, restrict agents to
+ an unspecified finite number.*)
+ Key_supply_ax "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
+
+
(*Agents generate random (symmetric) keys and nonces.
The numeric argument is typically the length of the current trace.
An injective pairing function allows multiple keys/nonces to be generated
@@ -63,6 +81,5 @@
inj_newK "inj newK"
newK_neq_shrK "newK i ~= shrK A"
- isSym_newK "isSymKey (newK i)"
end
--- a/src/HOL/Auth/WooLam.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/WooLam.ML Fri Jan 17 12:49:31 1997 +0100
@@ -25,10 +25,11 @@
\ : 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
- woolam.WL4 RS woolam.WL5) 2);
+ woolam.WL4 RS woolam.WL5) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
+ addss (!simpset setsolver safe_solver))));
result();
@@ -94,23 +95,6 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future nonces can't be seen or used! ***)
-
-goal thy "!!i. evs : woolam ==> \
-\ length evs <= i --> Nonce(newN(i)) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-
(**** Autheticity properties for Woo-Lam ****)
@@ -201,6 +185,5 @@
\ --> 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
- addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1);
+by (best_tac (!claset addSEs partsEs) 1);
**)
--- a/src/HOL/Auth/WooLam.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/WooLam.thy Fri Jan 17 12:49:31 1997 +0100
@@ -35,16 +35,16 @@
==> Says A B (Agent A) # evs : woolam"
(*Bob responds to Alice's message with a challenge.*)
- WL2 "[| evs: woolam; A ~= B;
+ WL2 "[| evs: woolam; A ~= B;
Says A' B (Agent A) : set_of_list evs |]
- ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
+ ==> 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 B' A (Nonce NB) : set_of_list evs;
- Says A B (Agent A) : set_of_list evs |]
+ Says A B (Agent A) : set_of_list evs;
+ Says B' A (Nonce NB) : set_of_list evs |]
==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
(*Bob forwards Alice's response to the Server.*)
--- a/src/HOL/Auth/Yahalom.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML Fri Jan 17 12:49:31 1997 +0100
@@ -14,7 +14,7 @@
proof_timing:=true;
HOL_quantifiers := false;
-Pretty.setdepth 20;
+Pretty.setdepth 25;
(*A "possibility property": there are traces that reach the end*)
@@ -23,9 +23,9 @@
\ ==> EX X NB K. EX evs: yahalom lost. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set_of_list 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);
-by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (ALLGOALS Fast_tac);
+by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS
+ yahalom.YM4) 2);
+by possibility_tac;
result();
@@ -115,64 +115,20 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
-
-(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!i. evs : yahalom lost ==> \
-\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
+(*Nobody can have used non-existent keys!*)
+goal thy "!!evs. evs : yahalom lost ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK i) : parts {X}; \
-\ evs : yahalom lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-(*Ready-made for the classical reasoner*)
-goal thy "!!evs. [| Says A B {|Crypt K {|b,Key(newK(length evs)),na,nb|}, X|}\
-\ : set_of_list evs; evs : yahalom lost |] \
-\ ==> R";
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset addsimps [parts_insertI])) 1);
-qed "Says_too_new_key";
-AddSEs [Says_too_new_key];
-
-
-(*Nobody can have USED keys that will be generated in the future.
- ...very like new_keys_not_seen*)
-goal thy "!!i. evs : yahalom lost ==> \
-\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
-by (parts_induct_tac 1);
-(*YM1, YM2 and YM3*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
-(*Fake and Oops: these messages send unknown (X) components*)
-by (EVERY
- (map (fast_tac
- (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addss (!simpset))) [3,1]));
-(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
-by (fast_tac
- (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [new_keys_not_seen RSN(2,rev_notE)]
- addDs [Suc_leD]) 1);
+(*YM4: Key K is not fresh!*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
+(*YM3*)
+by (fast_tac (!claset addss (!simpset)) 2);
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -185,10 +141,10 @@
(*Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.*)
goal thy
- "!!evs. [| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
-\ evs : yahalom lost |] \
-\ ==> EX i. K = Key(newK i)";
+ "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
+\ : set_of_list evs; \
+\ evs : yahalom lost |] \
+\ ==> K ~: range shrK";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -199,68 +155,42 @@
val analz_Fake_tac =
forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
- assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
+ assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
-
****)
-
-(*NOT useful in this form, but it says that session keys are not used
- to encrypt messages containing other keys, in the actual protocol.
- We require that agents should behave like this subsequently also.*)
-goal thy
- "!!evs. evs : yahalom lost ==> \
-\ (Crypt (newK i) X) : parts (sees lost Spy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
-by (etac yahalom.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Deals with Faked messages*)
-by (best_tac (!claset addSEs partsEs
- addDs [impOfSubs parts_insert_subset_Un]
- addss (!simpset)) 2);
-(*Base case*)
-by (Auto_tac());
-result();
-
-
(** Session keys are not used to encrypt other session keys **)
goal thy
"!!evs. evs : yahalom lost ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
-\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac yahalom.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 11 secs*)
- (asm_simp_tac
- (!simpset addsimps [Un_assoc RS sym,
- insert_Key_singleton, insert_Key_image, pushKey_newK]
- setloop split_tac [expand_if])));
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Base*)
+by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
(*YM4, Fake*)
-by (EVERY (map spy_analz_tac [4, 2]));
-(*Oops, YM3, Base*)
-by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
-qed_spec_mp "analz_image_newK";
+by (REPEAT (spy_analz_tac 1));
+qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. evs : yahalom lost ==> \
-\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
-\ (K = newK i | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
(*** The Key K uniquely identifies the Server's message. **)
@@ -279,8 +209,10 @@
(*Remaining case: YM3*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a very new message, and handle this case by contradiction*)
-by (Fast_tac 1); (*uses Says_too_new_key*)
+(*...we assume X is a recent message and handle this case by contradiction*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs
+ delrules [conjI] (*prevent split-up into 4 subgoals*)
+ addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
goal thy
@@ -324,10 +256,13 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
+ (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
setloop split_tac [expand_if])));
(*YM3*)
-by (Fast_tac 2); (*uses Says_too_new_key*)
+by (fast_tac (!claset delrules [impCE]
+ addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]
+ addss (!simpset addsimps [parts_insert2])) 2);
(*OR4, Fake*)
by (REPEAT_FIRST spy_analz_tac);
(*Oops*)
@@ -339,25 +274,27 @@
(*Final version: Server's message in the most abstract form*)
goal thy
- "!!evs. [| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, \
-\ Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs; \
-\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
-\ K ~: analz (sees lost Spy evs)";
+ "!!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; \
+\ 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);
by (fast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
goal thy
- "!!evs. [| C ~: {A,B,Server}; \
-\ Says Server A \
-\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, \
-\ Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs; \
-\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
-\ K ~: analz (sees lost C evs)";
+ "!!evs. [| C ~: {A,B,Server}; \
+\ 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; \
+\ 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);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
@@ -374,7 +311,7 @@
\ B ~: lost; evs : yahalom lost |] \
\ ==> EX NA NB. Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
+\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
@@ -384,40 +321,8 @@
qed "B_trusts_YM4_shrK";
-(*** General properties of nonces ***)
-
-goal thy "!!evs. evs : yahalom lost ==> \
-\ length evs <= i --> \
-\ Nonce (newN i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-(*Variant: old messages must contain old nonces!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN i) : parts {X}; \
-\ evs : yahalom lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_nonces";
-
-
(** The Nonce NB uniquely identifies B's message. **)
-val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
-
goal thy
"!!evs. evs : yahalom lost ==> \
\ EX NA' A' B'. ALL NA A B. \
@@ -427,14 +332,15 @@
(*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
by (REPEAT (etac exE 2) THEN
best_tac (!claset addSIs [exI]
- addDs [impOfSubs Fake_parts_insert]
- addss (!simpset)) 2);
+ addDs [impOfSubs Fake_parts_insert]
+ addss (!simpset)) 2);
(*Base case*)
by (fast_tac (!claset addss (!simpset)) 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
(*YM2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NB = ?y" 1);
-by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
+by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
val lemma = result();
goal thy
@@ -447,16 +353,6 @@
by (prove_unique_tac lemma 1);
qed "unique_NB";
-(*OLD VERSION
-fun lost_tac s =
- case_tac ("(" ^ s ^ ") : lost") THEN'
- SELECT_GOAL
- (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
- REPEAT_DETERM (etac MPair_analz 1) THEN
- dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
- assume_tac 1 THEN Fast_tac 1);
-*)
-
fun lost_tac s =
case_tac ("(" ^ s ^ ") : lost") THEN'
SELECT_GOAL
@@ -502,7 +398,6 @@
by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
addSIs [parts_insertI]
addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
addss (!simpset)) 1);
val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
@@ -518,8 +413,8 @@
\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
\ (EX A B NA. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
+\ {|Crypt (shrK A) {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs)";
by (etac yahalom.induct 1);
@@ -602,81 +497,97 @@
val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
-fun grind_tac i =
- SELECT_GOAL
- (REPEAT_FIRST
- (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
- assume_tac ORELSE'
- depth_tac (!claset delrules [conjI]
- addSIs [exI, analz_insertI,
- impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
(*The only nonces that can be found with the help of session keys are
those distributed as nonce NB by the Server. The form of the theorem
- recalls analz_image_newK, but it is much more complicated.*)
+ recalls analz_image_freshK, but it is much more complicated.*)
+
+(*As with analz_image_freshK, we take some pains to express the property
+ as a logical equivalence so that the simplifier can apply it.*)
+goal thy
+ "!!evs. P --> (X : analz (G Un H)) --> (X : analz H) ==> \
+\ P --> (X : analz (G Un H)) = (X : analz H)";
+by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+qed "Nonce_secrecy_lemma";
+
goal thy
- "!!evs. evs : yahalom lost ==> \
-\ ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
-\ (EX K: newK``E. EX A B na X. \
-\ Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
-\ : set_of_list evs) | Nonce NB : analz (sees lost Spy evs)";
+ "!!evs. evs : yahalom lost ==> \
+\ (ALL KK. KK <= Compl (range shrK) --> \
+\ (ALL K: KK. ALL A B na X. \
+\ Says Server A \
+\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
+\ ~: set_of_list evs) --> \
+\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (Nonce NB : analz (sees lost Spy evs)))";
by (etac yahalom.induct 1);
by analz_Fake_tac;
+by (REPEAT_FIRST (resolve_tac [impI RS allI]));
+by (REPEAT_FIRST (rtac Nonce_secrecy_lemma ));
+by (rtac ccontr 7);
+by (subgoal_tac "ALL A B na X. \
+\ Says Server A \
+\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
+\ ~: set_of_list evsa" 7);
+by (eres_inst_tac [("P","?PP-->?QQ")] notE 7);
+by (subgoal_tac "ALL A B na X. \
+\ Says Server A \
+\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
+\ ~: set_of_list evsa" 5);
by (ALLGOALS (*22 seconds*)
(asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz, analz_image_newK,
- insert_Key_singleton, insert_Key_image]
- @ pushes)
- setloop split_tac [expand_if])));
+ (analz_image_freshK_ss addsimps
+ ([all_conj_distrib,
+ not_parts_not_analz, analz_image_freshK]
+ @ pushes @ ball_simps))));
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
-(*Fake*) (** LEVEL 4 **)
+(*Fake*) (** LEVEL 10 **)
by (spy_analz_tac 1);
-(*YM1-YM3*) (*24 seconds*)
-by (EVERY (map grind_tac [3,2,1]));
+(*YM3*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
(*Oops*)
-by (Full_simp_tac 2);
-by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
-by (grind_tac 2);
-by (fast_tac (!claset delrules [bexI]
- addDs [unique_session_keys]
+(*20 secs*)
+by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys]
addss (!simpset)) 2);
(*YM4*)
-(** LEVEL 10 **)
-by (rtac (impI RS allI) 1);
+(** LEVEL 13 **)
+by (REPEAT (resolve_tac [impI, allI] 1));
by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
+by (stac insert_commute 1);
by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
-by (asm_simp_tac (!simpset addsimps [analz_image_newK]
- setloop split_tac [expand_if]) 1);
-(** LEVEL 14 **)
-by (grind_tac 1);
-by (REPEAT (dtac not_analz_insert 1));
+by (asm_simp_tac (analz_image_freshK_ss
+ addsimps [analz_insertI, analz_image_freshK]) 1);
+by (step_tac (!claset addSDs [not_analz_insert]) 1);
by (lost_tac "A" 1);
+(** LEVEL 20 **)
by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
THEN REPEAT (assume_tac 1));
-by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
-by (fast_tac (!claset delrules [conjI]
- addIs [analz_insertI]
- addss (!simpset)) 1);
-val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
+by (thin_tac "All ?PP" 1);
+by (Fast_tac 1);
+qed_spec_mp "Nonce_secrecy";
(*Version required below: if NB can be decrypted using a session key then it
was distributed with that key. The more general form above is required
for the induction to carry through.*)
goal thy
- "!!evs. [| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key (newK i), na, Nonce NB'|}, X|} \
-\ : set_of_list evs; \
-\ Nonce NB : analz (insert (Key (newK i)) (sees lost Spy evs)); \
-\ evs : yahalom lost |] \
-\ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
-by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
-by (dtac Nonce_secrecy 1 THEN assume_tac 1);
-by (fast_tac (!claset addDs [unique_session_keys]
- addss (!simpset)) 1);
-val single_Nonce_secrecy = result();
+ "!!evs. [| Says Server A \
+\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
+\ : set_of_list evs; \
+\ Nonce NB : analz (insert (Key KAB) (sees lost Spy evs)); \
+\ Nonce NB ~: analz (sees lost Spy evs); \
+\ KAB ~: range shrK; evs : yahalom lost |] \
+\ ==> NB = NB'";
+by (rtac ccontr 1);
+by (subgoal_tac "ALL A B na X. \
+\ Says Server A \
+\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
+\ ~: set_of_list evs" 1);
+by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
+by (asm_simp_tac (analz_image_freshK_ss
+ addsimps ([Nonce_secrecy] @ ball_simps)) 1);
+by (auto_tac (!claset addDs [unique_session_keys], (!simpset)));
+qed "single_Nonce_secrecy";
goal thy
@@ -691,46 +602,41 @@
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ analz_insert_freshK] @ pushes)
setloop split_tac [expand_if])));
by (fast_tac (!claset addSIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
+ addSEs sees_Spy_partsEs
addss (!simpset)) 2);
(*Proof of YM2*) (** LEVEL 4 **)
-by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2));
-by (fast_tac (!claset addIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
- addss (!simpset)) 3);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2);
+by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj,
+ impOfSubs analz_subset_parts]
+ addSEs partsEs) 3 2);
(*Prove YM3 by showing that no NB can also be an NA*)
by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
(*Fake*)
by (spy_analz_tac 1);
-(*YM4*) (** LEVEL 10 **)
+(*YM4*) (** LEVEL 8 **)
by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+(*43 secs??*)
by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
-(** LEVEL 13 **)
by (lost_tac "Aa" 1);
by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
by (forward_tac [Says_Server_message_form] 3);
by (forward_tac [Says_Server_imp_YM2] 4);
+(** LEVEL 15 **)
by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
-by (Full_simp_tac 1);
-by (REPEAT_FIRST hyp_subst_tac);
-(** LEVEL 20 **)
by (lost_tac "Ba" 1);
by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
addSEs [MPair_parts]) 1);
by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1));
+(** LEVEL 20 **)
by (dtac Spy_not_see_encrypted_key 1);
by (REPEAT (assume_tac 1 ORELSE Fast_tac 1));
by (spy_analz_tac 1);
-(*Oops case*) (** LEVEL 27 **)
+(*Oops case*) (** LEVEL 23 **)
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
by (step_tac (!claset delrules [disjE, conjI]) 1);
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
@@ -738,7 +644,7 @@
by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
by (rtac conjI 1);
by (no_nonce_tac 1);
-(** LEVEL 34 **)
+(** LEVEL 30 **)
by (thin_tac "?PP|?QQ" 1); (*subsumption!*)
by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
@@ -750,16 +656,16 @@
ALL POSSIBLE keys instead of our particular K (though at least the
nonces are forced to agree with NA and NB). *)
goal thy
- "!!evs. [| Says B Server \
+ "!!evs. [| Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
\ : set_of_list 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; \
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
-\ ==> Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
+\ ==> 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";
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
@@ -771,4 +677,3 @@
by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
qed "B_trusts_YM4";
-
--- a/src/HOL/Auth/Yahalom.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Yahalom.thy Fri Jan 17 12:49:31 1997 +0100
@@ -26,30 +26,26 @@
==> Says Spy B X # evs : yahalom lost"
(*Alice initiates a protocol run*)
- YM1 "[| evs: yahalom lost; A ~= B |]
- ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs
- : yahalom lost"
+ YM1 "[| evs: yahalom lost; A ~= B; Nonce NA ~: used evs |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
(*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;
+ YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs;
Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
==> Says B Server
- {|Agent B,
- Crypt (shrK B)
- {|Agent A, Nonce NA, Nonce (newN(length evs))|}|}
- # evs : yahalom lost"
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ # evs : yahalom lost"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3 "[| evs: yahalom lost; A ~= Server;
+ 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 |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key (newK(length evs)),
- Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key (newK(length evs))|}|}
+ {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key KAB|}|}
# evs : yahalom lost"
(*Alice receives the Server's (?) message, checks her Nonce, and
--- a/src/HOL/Auth/Yahalom2.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Fri Jan 17 12:49:31 1997 +0100
@@ -24,9 +24,9 @@
\ ==> EX X NB K. EX evs: yahalom lost. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set_of_list 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);
-by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (ALLGOALS Fast_tac);
+by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS
+ yahalom.YM4) 2);
+by possibility_tac;
result();
@@ -91,87 +91,45 @@
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
+(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. [| evs : yahalom lost; A ~: lost |] \
-\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
+ "!!evs. evs : yahalom lost \
+\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
by (parts_induct_tac 1);
by (Auto_tac());
-qed "Spy_not_see_shrK";
-
-bind_thm ("Spy_not_analz_shrK",
- [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
-
-Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
+qed "Spy_see_shrK";
+Addsimps [Spy_see_shrK];
-(*We go to some trouble to preserve R in the 3rd and 4th subgoals
- As usual fast_tac cannot be used because it uses the equalities too soon*)
-val major::prems =
-goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \
-\ evs : yahalom lost; \
-\ A:lost ==> R \
-\ |] ==> R";
-by (rtac ccontr 1);
-by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
-by (swap_res_tac prems 2);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
-qed "Spy_see_shrK_E";
+goal thy
+ "!!evs. evs : yahalom lost \
+\ ==> (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];
-bind_thm ("Spy_analz_shrK_E",
- analz_subset_parts RS subsetD RS Spy_see_shrK_E);
+goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
+\ evs : yahalom lost |] ==> A:lost";
+by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+qed "Spy_see_shrK_D";
-AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
+bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
+AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
-
-(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!i. evs : yahalom lost ==> \
-\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
+(*Nobody can have used non-existent keys!*)
+goal thy "!!evs. evs : yahalom lost ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK i) : parts {X}; \
-\ evs : yahalom lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-(*Nobody can have USED keys that will be generated in the future.
- ...very like new_keys_not_seen*)
-goal thy "!!i. evs : yahalom lost ==> \
-\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
-by (parts_induct_tac 1);
-by (dtac YM4_Key_parts_sees_Spy 5);
-(*YM1, YM2 and YM3*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
-(*Fake and Oops: these messages send unknown (X) components*)
-by (EVERY
- (map (fast_tac
- (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addss (!simpset))) [3,1]));
-(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
-by (fast_tac
- (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [new_keys_not_seen RSN(2,rev_notE)]
- addDs [Suc_leD]) 1);
+(*YM4: Key K is not fresh!*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
+(*YM3*)
+by (fast_tac (!claset addss (!simpset)) 2);
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -184,10 +142,10 @@
(*Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.*)
goal thy
- "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
+ "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
\ : set_of_list evs; \
\ evs : yahalom lost |] \
-\ ==> (EX i. K = Key(newK i)) & A ~= B";
+\ ==> K ~: range shrK & A ~= B";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -198,14 +156,14 @@
val analz_Fake_tac =
dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
- assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((eresolve_tac [exE,conjE] ORELSE' hyp_subst_tac) 7);
+ assume_tac 7 THEN
+ REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -216,30 +174,26 @@
goal thy
"!!evs. evs : yahalom lost ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
-\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac yahalom.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 11 secs*)
- (asm_simp_tac
- (!simpset addsimps [Un_assoc RS sym,
- insert_Key_singleton, insert_Key_image, pushKey_newK]
- setloop split_tac [expand_if])));
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Base*)
+by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
(*YM4, Fake*)
-by (EVERY (map spy_analz_tac [4, 2]));
-(*Oops, YM3, Base*)
-by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
-qed_spec_mp "analz_image_newK";
+by (REPEAT (spy_analz_tac 1));
+qed_spec_mp "analz_image_freshK";
goal thy
- "!!evs. evs : yahalom lost ==> \
-\ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) = \
-\ (K = newK i | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
(*** The Key K uniquely identifies the Server's message. **)
@@ -256,8 +210,8 @@
(*Remaining case: YM3*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a very new message, and handle this case by contradiction*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+(*...we assume X is a recent message and handle this case by contradiction*)
+by (fast_tac (!claset addSEs sees_Spy_partsEs
delrules [conjI] (*prevent split-up into 4 subgoals*)
addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
@@ -290,12 +244,13 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
+ (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
setloop split_tac [expand_if])));
(*YM3*)
-by (fast_tac (!claset addIs [parts_insertI]
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 2);
+by (fast_tac (!claset delrules [impCE]
+ addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]
+ addss (!simpset addsimps [parts_insert2])) 2);
(*OR4, Fake*)
by (REPEAT_FIRST spy_analz_tac);
(*Oops*)
@@ -308,12 +263,12 @@
(*Final version: Server's message in the most abstract form*)
goal thy
"!!evs. [| Says Server A \
-\ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \
-\ Crypt (shrK B) {|NB, K, Agent 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, K|} ~: set_of_list evs; \
+\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> K ~: analz (sees lost Spy evs)";
+\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -322,12 +277,12 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server A \
-\ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \
-\ Crypt (shrK B) {|NB, K, Agent 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, K|} ~: set_of_list evs; \
+\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> K ~: analz (sees lost C evs)";
+\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
--- a/src/HOL/Auth/Yahalom2.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.thy Fri Jan 17 12:49:31 1997 +0100
@@ -30,26 +30,26 @@
==> Says Spy B X # evs : yahalom lost"
(*Alice initiates a protocol run*)
- YM1 "[| evs: yahalom lost; A ~= B |]
- ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost"
+ YM1 "[| evs: yahalom lost; A ~= B; Nonce NA ~: used evs |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
(*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;
+ YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs;
Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
- ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|}
- # evs : yahalom lost"
+ ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs
+ : yahalom lost"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.
Fields are reversed in the 2nd packet to prevent attacks.*)
- YM3 "[| evs: yahalom lost; A ~= B; A ~= Server;
+ YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs;
Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set_of_list evs |]
==> Says Server A
{|Nonce NB,
- Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|},
- Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|}
+ Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
+ Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
# evs : yahalom lost"
(*Alice receives the Server's (?) message, checks her Nonce, and