Removed some dead wood. Transferred lemmas used to prove analz_image_newK
to Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Mon Sep 30 11:10:22 1996 +0200
@@ -297,35 +297,8 @@
result();
-(** Specialized rewriting for this proof **)
-
-Delsimps [image_insert];
-Addsimps [image_insert RS sym];
-
-Delsimps [image_Un];
-Addsimps [image_Un RS sym];
-
-goal thy "insert (Key (newK x)) (sees lost A evs) = \
-\ Key `` (newK``{x}) Un (sees lost A evs)";
-by (Fast_tac 1);
-val insert_Key_singleton = result();
-
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\ Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-val insert_Key_image = result();
-
-
(** 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 : ns_shared lost ==> \
@@ -334,7 +307,7 @@
by (etac ns_shared.induct 1);
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by (REPEAT ((eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac) 5));
-by (REPEAT_FIRST (resolve_tac [allI, lemma]));
+by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
--- a/src/HOL/Auth/OtwayRees.ML Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Mon Sep 30 11:10:22 1996 +0200
@@ -43,7 +43,6 @@
:: otway.intrs))));
qed "otway_mono";
-
(*The Spy can see more than anybody else, except for their initial state*)
goal thy
"!!evs. evs : otway lost ==> \
@@ -301,37 +300,6 @@
result();
-(** Specialized rewriting for this proof **)
-
-Delsimps [image_insert];
-Addsimps [image_insert RS sym];
-
-Delsimps [image_Un];
-Addsimps [image_Un RS sym];
-
-goal thy "insert (Key (newK x)) (sees lost A evs) = \
-\ Key `` (newK``{x}) Un (sees lost A evs)";
-by (Fast_tac 1);
-val insert_Key_singleton = result();
-
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\ Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-val insert_Key_image = result();
-
-
-(*This lets us avoid analyzing the new message -- unless we have to!*)
-(*NEEDED??*)
-goal thy "synth (analz (sees lost Spy evs)) <= \
-\ synth (analz (sees lost Spy (Says A B X # evs)))";
-by (Simp_tac 1);
-by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
-qed "synth_analz_thin";
-
-AddIs [impOfSubs synth_analz_thin];
-
-
-
(** Session keys are not used to encrypt other session keys **)
(*Describes the form of Key K when the following message is sent. The use of
@@ -358,7 +326,8 @@
goal thy
"!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs; \
\ evs : otway lost |] \
-\ ==> (EX evt: otway lost. K = newK evt) | Key K : analz (sees lost Spy evs)";
+\ ==> (EX evt: otway lost. K = newK evt) \
+\ | Key K : analz (sees lost Spy evs)";
by (excluded_middle_tac "A : lost" 1);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
addss (!simpset)) 2);
@@ -369,15 +338,6 @@
qed "Reveal_message_form";
-(*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 lost ==> \
@@ -387,7 +347,7 @@
by (dtac OR2_analz_sees_Spy 4);
by (dtac OR4_analz_sees_Spy 6);
by (dtac Reveal_message_form 7);
-by (REPEAT_FIRST (ares_tac [allI, lemma]));
+by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
by (ALLGOALS (*Takes 28 secs*)
(asm_simp_tac
--- a/src/HOL/Auth/Shared.ML Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/Shared.ML Mon Sep 30 11:10:22 1996 +0200
@@ -10,38 +10,6 @@
-(****************DELETE****************)
-
-local
- fun string_of (a,0) = a
- | string_of (a,i) = a ^ "_" ^ string_of_int i;
-in
- fun freeze_thaw th =
- let val fth = freezeT th
- val {prop,sign,...} = rep_thm fth
- fun mk_inst (Var(v,T)) =
- (cterm_of sign (Var(v,T)),
- cterm_of sign (Free(string_of v, T)))
- val insts = map mk_inst (term_vars prop)
- fun thaw th' =
- th' |> forall_intr_list (map #2 insts)
- |> forall_elim_list (map #1 insts)
- in (instantiate ([],insts) fth, thaw) end;
-end;
-fun defer_tac i state =
- let val (state',thaw) = freeze_thaw state
- val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
- val hyp::hyps' = drop(i-1,hyps)
- in implies_intr hyp (implies_elim_list state' (map assume hyps))
- |> implies_intr_list (take(i-1,hyps) @ hyps')
- |> thaw
- |> Sequence.single
- end
- handle Bind => Sequence.null;
-
-
-
-
(*GOALS.ML??*)
fun prlim n = (goals_limit:=n; pr());
@@ -132,12 +100,12 @@
qed_spec_mp "sees_own_shrK";
(*Spy sees shared keys of lost agents!*)
-goal thy "!!i. A: lost ==> Key (shrK A) : sees lost Spy evs";
+goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs";
by (list.induct_tac "evs" 1);
by (Auto_tac());
-qed "Spy_sees_bad";
+qed "Spy_sees_lost";
-AddSIs [sees_own_shrK, Spy_sees_bad];
+AddSIs [sees_own_shrK, Spy_sees_lost];
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
@@ -259,8 +227,37 @@
(** Simplifying parts (insert X (sees lost A evs))
- = parts {X} Un parts (sees lost A evs) -- since general case loops*)
+ = parts {X} Un parts (sees lost A evs) -- since general case loops*)
val parts_insert_sees =
- parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees lost A evs")]
+ parts_insert |> read_instantiate_sg (sign_of thy)
+ [("H", "sees lost A evs")]
|> standard;
+
+
+(** Specialized rewriting for **)
+
+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";
+by (Fast_tac 1);
+qed "insert_Key_singleton";
+
+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";
+
+
+(*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";
+
+
--- a/src/HOL/Auth/Yahalom.ML Mon Sep 30 11:04:14 1996 +0200
+++ b/src/HOL/Auth/Yahalom.ML Mon Sep 30 11:10:22 1996 +0200
@@ -31,6 +31,14 @@
(**** Inductive proofs about yahalom ****)
+goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
+by (rtac subsetI 1);
+by (etac yahalom.induct 1);
+by (REPEAT_FIRST
+ (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ :: yahalom.intrs))));
+qed "yahalom_mono";
+
(*The Spy can see more than anybody else, except for their initial state*)
goal thy
"!!evs. evs : yahalom lost ==> \
@@ -40,6 +48,15 @@
addss (!simpset))));
qed "sees_agent_subset_sees_Spy";
+(*The Spy can see more than anybody else who's lost their key!*)
+goal thy
+ "!!evs. evs : yahalom lost ==> \
+\ A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
+by (etac yahalom.induct 1);
+by (agent.induct_tac "A" 1);
+by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
+qed_spec_mp "sees_lost_agent_subset_sees_Spy";
+
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
@@ -222,55 +239,15 @@
result();
-(** Specialized rewriting for this proof **)
-
-Delsimps [image_insert];
-Addsimps [image_insert RS sym];
-
-Delsimps [image_Un];
-Addsimps [image_Un RS sym];
-
-goal thy "insert (Key (newK x)) (sees lost A evs) = \
-\ Key `` (newK``{x}) Un (sees lost A evs)";
-by (Fast_tac 1);
-val insert_Key_singleton = result();
-
-goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
-\ Key `` (f `` (insert x E)) Un C";
-by (Fast_tac 1);
-val insert_Key_image = result();
-
-
-(*This lets us avoid analyzing the new message -- unless we have to!*)
-(*NEEDED??*)
-goal thy "synth (analz (sees lost Spy evs)) <= \
-\ synth (analz (sees lost Spy (Says A B X # evs)))";
-by (Simp_tac 1);
-by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
-qed "synth_analz_thin";
-
-AddIs [impOfSubs synth_analz_thin];
-
-
-
(** 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();
-
-
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))";
by (etac yahalom.induct 1);
by (dtac YM4_analz_sees_Spy 6);
-by (REPEAT_FIRST (resolve_tac [allI, lemma]));
+by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@@ -349,6 +326,20 @@
qed "Spy_not_see_encrypted_key";
+goal thy
+ "!!evs. [| C ~: {A,B,Server}; \
+\ Says Server A \
+\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
+\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
+\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
+\ 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));
+by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
+qed "Agent_not_see_encrypted_key";
+
+
(** Towards proofs of stronger authenticity properties **)
goal thy