--- a/src/HOL/Auth/Event.ML Mon Aug 19 11:19:16 1996 +0200
+++ b/src/HOL/Auth/Event.ML Mon Aug 19 11:19:55 1996 +0200
@@ -15,29 +15,25 @@
Delrules [less_SucE]; (*Perhaps avoid inserting this in Arith.ML????*)
(*FOR LIST.ML??*)
-goal List.thy "x : setOfList (x#xs)";
+goal List.thy "x : set_of_list (x#xs)";
by (Simp_tac 1);
-qed "setOfList_I1";
+qed "set_of_list_I1";
-goal List.thy "!!x. xs = x#xs' ==> x : setOfList xs";
+goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs";
by (Asm_simp_tac 1);
-qed "setOfList_eqI1";
+qed "set_of_list_eqI1";
-goal List.thy "setOfList l <= setOfList (x#l)";
+goal List.thy "set_of_list l <= set_of_list (x#l)";
by (Simp_tac 1);
by (Fast_tac 1);
-qed "setOfList_subset_Cons";
+qed "set_of_list_subset_Cons";
(*Not for Addsimps -- it can cause goals to blow up!*)
goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
qed "mem_if";
-(*DELETE, AS ALREADY IN SET.ML*)
-prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))";
-
-
-(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE!!*)
+(*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();
@@ -45,10 +41,6 @@
open Event;
-goal Set.thy "A Un (insert a B) = insert a (A Un B)";
-by (Fast_tac 1);
-qed "Un_insert_right";
-
Addsimps [Un_insert_left, Un_insert_right];
(*By default only o_apply is built-in. But in the presence of eta-expansion
@@ -94,15 +86,15 @@
bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
-goal thy "!!H. H <= Key``E ==> analyze H = H";
+goal thy "!!H. H <= Key``E ==> analz H = H";
by (Auto_tac ());
-be analyze.induct 1;
+be analz.induct 1;
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "analyze_image_subset";
+qed "analz_image_subset";
-bind_thm ("analyze_image_Key", subset_refl RS analyze_image_subset);
+bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
-Addsimps [parts_image_Key, analyze_image_Key];
+Addsimps [parts_image_Key, analz_image_Key];
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
by (agent.induct_tac "C" 1);
@@ -123,17 +115,17 @@
(*Agents see their own serverKeys!*)
-goal thy "Key (serverKey A) : analyze (sees A evs)";
+goal thy "Key (serverKey A) : analz (sees A evs)";
by (list.induct_tac "evs" 1);
-by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analyze_mono)]) 2);
+by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
by (agent.induct_tac "A" 1);
by (auto_tac (!claset addIs [range_eqI], !simpset));
-qed "analyze_own_serverKey";
+qed "analz_own_serverKey";
bind_thm ("parts_own_serverKey",
- [analyze_subset_parts, analyze_own_serverKey] MRS subsetD);
+ [analz_subset_parts, analz_own_serverKey] MRS subsetD);
-Addsimps [analyze_own_serverKey, parts_own_serverKey];
+Addsimps [analz_own_serverKey, parts_own_serverKey];
@@ -197,7 +189,7 @@
by (ALLGOALS (fast_tac (!claset addss ss)));
qed "UN_parts_sees_Says";
-goal thy "Says A B X : setOfList evs --> X : sees Enemy evs";
+goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
by (list.induct_tac "evs" 1);
by (Auto_tac ());
qed_spec_mp "Says_imp_sees_Enemy";
@@ -211,8 +203,8 @@
qed "initState_subset";
goal thy "X : sees C evs --> \
-\ (EX A B. Says A B X : setOfList evs) | \
-\ (EX A. Notes A X : setOfList evs) | \
+\ (EX A B. Says A B X : set_of_list evs) | \
+\ (EX A. Notes A X : set_of_list evs) | \
\ (EX A. X = Key (serverKey A))";
by (list.induct_tac "evs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -244,14 +236,14 @@
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs";
+goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs";
be traces.induct 1;
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
-goal thy "!!evs. evs : traces ==> Notes A X ~: setOfList evs";
+goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs";
be traces.induct 1;
by (Auto_tac());
qed "not_Notes";
@@ -269,18 +261,18 @@
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
by (auto_tac(!claset, !simpset addsimps [parts_insert2]));
(*Deals with Faked messages*)
-by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
+by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un]
addss (!simpset)) 1);
qed "Enemy_not_see_serverKey";
-bind_thm ("Enemy_not_analyze_serverKey",
- [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
+bind_thm ("Enemy_not_analz_serverKey",
+ [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
Addsimps [Enemy_not_see_serverKey,
not_sym RSN (2, Enemy_not_see_serverKey),
- Enemy_not_analyze_serverKey,
- not_sym RSN (2, Enemy_not_analyze_serverKey)];
+ Enemy_not_analz_serverKey,
+ not_sym RSN (2, Enemy_not_analz_serverKey)];
(*We go to some trouble to preserve R in the 3rd subgoal*)
val major::prems =
@@ -294,11 +286,11 @@
by (ALLGOALS (fast_tac (!claset addIs prems)));
qed "Enemy_see_serverKey_E";
-bind_thm ("Enemy_analyze_serverKey_E",
- analyze_subset_parts RS subsetD RS Enemy_see_serverKey_E);
+bind_thm ("Enemy_analz_serverKey_E",
+ analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
-AddSEs [Enemy_see_serverKey_E, Enemy_analyze_serverKey_E];
+AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
(*No Friend will ever see another agent's server key
@@ -316,12 +308,12 @@
goal thy
"!!evs. evs : traces ==> \
\ (Key (serverKey A) \
-\ : analyze (insert (Key (serverKey B)) (sees Enemy evs))) = \
+\ : analz (insert (Key (serverKey B)) (sees Enemy evs))) = \
\ (A=B | A=Enemy)";
-by (best_tac (!claset addDs [impOfSubs analyze_subset_parts]
- addIs [impOfSubs (subset_insertI RS analyze_mono)]
+by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
+ addIs [impOfSubs (subset_insertI RS analz_mono)]
addss (!simpset)) 1);
-qed "serverKey_mem_analyze";
+qed "serverKey_mem_analz";
@@ -349,7 +341,7 @@
(*Rule NS3 in protocol*)
by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
(*Rule Fake: where an Enemy agent can say practically anything*)
-by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
+by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
less_imp_le]
addss (!simpset)) 1);
@@ -365,7 +357,7 @@
(*Another variant: old messages must contain old keys!*)
goal thy
- "!!evs. [| Says A B X : setOfList evs; \
+ "!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
\ evs : traces \
\ |] ==> length evt < length evs";
@@ -398,10 +390,10 @@
(*Rule Fake: where an Enemy agent can say practically anything*)
by (best_tac
(!claset addSDs [newK_invKey]
- addDs [impOfSubs (analyze_subset_parts RS keysFor_mono),
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono),
less_imp_le]
- addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)]
+ addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
addss (!simpset)) 1);
(*Rule NS3: quite messy...*)
by (hyp_subst_tac 1);
@@ -422,15 +414,15 @@
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
qed "new_keys_not_used";
-bind_thm ("new_keys_not_analyzed",
- [analyze_subset_parts RS keysFor_mono,
+bind_thm ("new_keys_not_analzd",
+ [analz_subset_parts RS keysFor_mono,
new_keys_not_used] MRS contra_subsetD);
-Addsimps [new_keys_not_used, new_keys_not_analyzed];
+Addsimps [new_keys_not_used, new_keys_not_analzd];
(** Rewrites to push in Key and Crypt messages, so that other messages can
- be pulled out using the analyze_insert rules **)
+ be pulled out using the analz_insert rules **)
fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)]
insert_commute;
@@ -452,7 +444,7 @@
(*Describes the form *and age* of K, and the form of X,
when the following message is sent*)
goal thy
- "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \
+ "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
\ evs : traces \
\ |] ==> (EX evt:traces. \
\ K = Key(newK evt) & \
@@ -465,9 +457,9 @@
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
qed "Says_Server_message_form";
-(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *)
-bind_thm ("not_parts_not_keysFor_analyze",
- analyze_subset_parts RS keysFor_mono RS contra_subsetD);
+(* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *)
+bind_thm ("not_parts_not_keysFor_analz",
+ analz_subset_parts RS keysFor_mono RS contra_subsetD);
@@ -477,13 +469,13 @@
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \
\ evs : traces; i~=k \
\ |] ==> \
-\ K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
+\ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
be rev_mp 1;
be traces.induct 1;
be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*)
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
by (Step_tac 1);
-by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1);
+by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
val Enemy_not_see_encrypted_key_lemma = result();
*)
@@ -519,9 +511,9 @@
(*Now for the Fake case*)
by (subgoal_tac
"Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey A) : \
-\ parts (synthesize (analyze (sees Enemy evsa)) Un (sees Enemy evsa))" 1);
+\ parts (synth (analz (sees Enemy evsa)) Un (sees Enemy evsa))" 1);
by (fast_tac (!claset addSEs [impOfSubs parts_mono]) 2);
-by (best_tac (!claset addDs [impOfSubs analyze_subset_parts]
+by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
addss (!simpset)) 1);
val encrypted_form = result();
@@ -531,7 +523,7 @@
"!!evs. evs : traces ==> \
\ ALL S A NA B K X. \
\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
-\ : setOfList evs --> \
+\ : set_of_list evs --> \
\ S = Server | S = Enemy";
be traces.induct 1;
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
@@ -541,7 +533,7 @@
(*First justify this assumption!*)
by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
by (Step_tac 1);
-bd (setOfList_I1 RS Says_Server_message_form) 1;
+bd (set_of_list_I1 RS Says_Server_message_form) 1;
by (ALLGOALS Full_simp_tac);
(*Final case. Clear out needless quantifiers to speed the following step*)
by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
@@ -555,7 +547,7 @@
use Says_Server_message_form if applicable*)
goal thy
"!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
-\ : setOfList evs; \
+\ : set_of_list evs; \
\ evs : traces \
\ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \
\ X = (Crypt {|Key K, Agent A|} (serverKey B)))";
@@ -576,7 +568,7 @@
\ K = newK evt & \
\ X = (Crypt {|Key K, Agent A|} (serverKey B)))";
by (forward_tac [traces_eq_ConsE] 1);
-by (dtac (setOfList_eqI1 RS Says_S_message_form) 2);
+by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2);
by (Auto_tac());
qed "Says_S_message_form_eq";
@@ -586,9 +578,9 @@
(****
The following is to prove theorems of the form
- Key K : analyze (insert (Key (newK evt))
+ Key K : analz (insert (Key (newK evt))
(insert (Key (serverKey C)) (sees Enemy evs))) ==>
- Key K : analyze (insert (Key (serverKey C)) (sees Enemy evs))
+ Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
A more general formula must be proved inductively.
@@ -610,7 +602,7 @@
by (res_inst_tac [("x1","Xa")] (insert_commute RS ssubst) 2);
by (Asm_full_simp_tac 2);
(*Deals with Faked messages*)
-by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
+by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un]
addss (!simpset)) 1);
result();
@@ -636,10 +628,10 @@
goal thy
"!!evs. evs : traces ==> \
-\ ALL K E. (Key K : analyze (insert (Key (serverKey C)) \
+\ ALL K E. (Key K : analz (insert (Key (serverKey C)) \
\ (Key``(newK``E) Un (sees Enemy evs)))) = \
\ (K : newK``E | \
-\ Key K : analyze (insert (Key (serverKey C)) \
+\ Key K : analz (insert (Key (serverKey C)) \
\ (sees Enemy evs)))";
be traces.induct 1;
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
@@ -657,35 +649,35 @@
(** LEVEL 7 **)
(*Fake case*)
by (REPEAT (Safe_step_tac 1));
-by (fast_tac (!claset addSEs [impOfSubs (analyze_mono)]) 2);
+by (fast_tac (!claset addSEs [impOfSubs (analz_mono)]) 2);
by (subgoal_tac
- "Key K : analyze \
-\ (synthesize \
-\ (analyze (insert (Key (serverKey C)) \
+ "Key K : analz \
+\ (synth \
+\ (analz (insert (Key (serverKey C)) \
\ (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
(*First, justify this subgoal*)
(*Discard the quantified formula for better speed*)
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
-by (best_tac (!claset addIs [impOfSubs (analyze_mono RS synthesize_mono)]
- addSEs [impOfSubs analyze_mono]) 2);
+by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
+ addSEs [impOfSubs analz_mono]) 2);
by (Asm_full_simp_tac 1);
-by (deepen_tac (!claset addIs [impOfSubs analyze_mono]) 0 1);
-qed_spec_mp "analyze_image_newK";
+by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1);
+qed_spec_mp "analz_image_newK";
goal thy
"!!evs. evs : traces ==> \
-\ Key K : analyze (insert (Key (newK evt)) \
+\ Key K : analz (insert (Key (newK evt)) \
\ (insert (Key (serverKey C)) \
\ (sees Enemy evs))) = \
\ (K = newK evt | \
-\ Key K : analyze (insert (Key (serverKey C)) \
+\ Key K : analz (insert (Key (serverKey C)) \
\ (sees Enemy evs)))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analyze_image_newK,
+by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
-qed "analyze_insert_Key_newK";
+qed "analz_insert_Key_newK";
@@ -694,7 +686,7 @@
"!!evs. evs : traces ==> \
\ EX X'. ALL C S A Y N B X. \
\ C ~= Enemy --> \
-\ Says S A Y : setOfList evs --> \
+\ Says S A Y : set_of_list evs --> \
\ ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
\ (X = X'))";
be traces.induct 1;
@@ -721,7 +713,7 @@
by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
\ : parts (sees Enemy evsa)" 1);
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
-by (best_tac (!claset addSEs [impOfSubs analyze_subset_parts]
+by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
addDs [impOfSubs parts_insert_subset_Un]
addss (!simpset)) 2);
by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
@@ -737,9 +729,9 @@
(*In messages of this form, the session key uniquely identifies the rest*)
goal thy
"!!evs. [| Says S A \
-\ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) : setOfList evs; \
+\ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) : set_of_list evs; \
\ Says S' A' \
-\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : setOfList evs; \
+\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : set_of_list evs; \
\ \
\ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'";
bd lemma 1;
@@ -754,10 +746,10 @@
-- even if another key is compromised*)
goal thy
"!!evs. [| Says Server (Friend i) \
-\ (Crypt {|N, Agent(Friend j), K, X|} K') : setOfList evs; \
+\ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \
\ evs : traces; Friend i ~= C; Friend j ~= C \
\ |] ==> \
-\ K ~: analyze (insert (Key (serverKey C)) (sees Enemy evs))";
+\ K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
be rev_mp 1;
be traces.induct 1;
be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*)
@@ -768,8 +760,8 @@
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
by (ALLGOALS
(asm_full_simp_tac
- (!simpset addsimps ([analyze_subset_parts RS contra_subsetD,
- analyze_insert_Key_newK] @ pushes)
+ (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
+ analz_insert_Key_newK] @ pushes)
setloop split_tac [expand_if])));
(*NS2*)
by (fast_tac (!claset addSEs [less_irrefl]) 2);
@@ -778,13 +770,13 @@
br notI 1;
by (subgoal_tac
"Key (newK evt) : \
-\ analyze (synthesize (analyze (insert (Key (serverKey C)) \
+\ analz (synth (analz (insert (Key (serverKey C)) \
\ (sees Enemy evsa))))" 1);
-be (impOfSubs analyze_mono) 2;
-by (deepen_tac (!claset addIs [analyze_mono RS synthesize_mono RSN
+be (impOfSubs analz_mono) 2;
+by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN
(2,rev_subsetD),
- impOfSubs synthesize_increasing,
- impOfSubs analyze_increasing]) 0 2);
+ impOfSubs synth_increasing,
+ impOfSubs analz_increasing]) 0 2);
(*Proves the Fake goal*)
by (fast_tac (!claset addss (!simpset)) 1);
@@ -792,14 +784,14 @@
(*Now for NS3*)
(*NS3, case 1: that message from the Server was just sent*)
by (ALLGOALS (forward_tac [traces_ConsE]));
-by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1);
+by (forward_tac [set_of_list_I1 RS Says_Server_message_form] 1);
by (Full_simp_tac 1);
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
(*Can simplify the Crypt messages: their key is secure*)
by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
by (asm_full_simp_tac
- (!simpset addsimps (pushes @ [analyze_insert_Crypt,
- analyze_subset_parts RS contra_subsetD])) 1);
+ (!simpset addsimps (pushes @ [analz_insert_Crypt,
+ analz_subset_parts RS contra_subsetD])) 1);
(**LEVEL 20, one subgoal left! **)
(*NS3, case 2: that message from the Server was sent earlier*)
@@ -813,18 +805,18 @@
(**LEVEL 24 **)
-by ((forward_tac [setOfList_I1 RS Says_S_message_form]) 1);
+by ((forward_tac [set_of_list_I1 RS Says_S_message_form]) 1);
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
by (asm_full_simp_tac
- (!simpset addsimps (mem_if::analyze_insert_Key_newK::pushes)) 1);
+ (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
by (step_tac (!claset delrules [impCE]) 1);
(**LEVEL 28 **)
-bd ([impOfSubs setOfList_subset_Cons, setOfList_I1] MRS unique_session_keys) 1;
+bd ([impOfSubs set_of_list_subset_Cons, set_of_list_I1] MRS unique_session_keys) 1;
ba 1;
by (ALLGOALS Full_simp_tac);
by (REPEAT_FIRST (eresolve_tac [conjE] ORELSE' hyp_subst_tac));
-by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analyze]) 1);
+by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
qed "Enemy_not_see_encrypted_key";
@@ -839,25 +831,25 @@
goal thy
"!!evs. [| Says Server (Friend i) \
-\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
+\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \
\ evs : traces; i~=j \
-\ |] ==> K ~: analyze (sees (Friend j) evs)";
-br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1;
+\ |] ==> K ~: analz (sees (Friend j) evs)";
+br (sees_agent_subset_sees_Enemy RS analz_mono RS contra_subsetD) 1;
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
qed "Friend_not_see_encrypted_key";
goal thy
"!!evs. [| Says Server (Friend i) \
-\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
+\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \
\ A ~: {Friend i, Server}; \
\ evs : traces \
-\ |] ==> K ~: analyze (sees A evs)";
+\ |] ==> K ~: analz (sees A evs)";
by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
by (agent.induct_tac "A" 1);
by (ALLGOALS Simp_tac);
by (asm_simp_tac (!simpset addsimps [eq_sym_conv,
Friend_not_see_encrypted_key]) 1);
-br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
+br ([analz_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
(* hyp_subst_tac would deletes the equality assumption... *)
by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
qed "Agent_not_see_encrypted_key";
@@ -866,7 +858,7 @@
(*Neatly packaged, perhaps in a useless form*)
goalw thy [knownBy_def]
"!!evs. [| Says Server (Friend i) \
-\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
+\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \
\ evs : traces \
\ |] ==> knownBy evs K <= {Friend i, Server}";
@@ -887,269 +879,38 @@
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \
\ evs : traces; i~=k \
\ |] ==> \
-\ K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
+\ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
be rev_mp 1;
be traces.induct 1;
be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*)
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
by (Step_tac 1);
-by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1);
+by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
val Enemy_not_see_encrypted_key_lemma = result();
-by (asm_full_simp_tac
- (!simpset addsimps (pushes @
- [analyze_subset_parts RS contra_subsetD,
- traces_ConsE RS Enemy_not_see_serverKey])) 1);
-
-by (asm_full_simp_tac
- (!simpset addsimps [analyze_subset_parts RS keysFor_mono RS contra_subsetD,
- traces_ConsE RS new_keys_not_used]) 1);
-by (Fast_tac 1);
-
-
-
-
-(*Precisely formulated as needed below. Perhaps redundant, as simplification
- with the aid of analyze_subset_parts RS contra_subsetD might do the
- same thing.*)
-goal thy
- "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \
-\ Key (serverKey A) ~: \
-\ analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
-br (analyze_subset_parts RS contra_subsetD) 1;
-by (Asm_simp_tac 1);
-qed "insert_not_analyze_serverKey";
-
-
-
-
-by (asm_full_simp_tac
- (!simpset addsimps (pushes @
- [insert_not_analyze_serverKey,
- traces_ConsE RS insert_not_analyze_serverKey])) 1);
-
-
-by (stac analyze_insert_Crypt 1);
-
-
-
-
-
-
-
-
-
-(*NS3, case 1: that message from the Server was just sent*)
-by (asm_full_simp_tac (!simpset addsimps pushes) 1);
-
-(*NS3, case 2: that message from the Server was sent earlier*)
-by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
-by (mp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps pushes) 1);
-
-by (Step_tac 1);
-by (asm_full_simp_tac
- (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
-
-
-
-(*pretend we have the right lemma!*)
-by (subgoal_tac "(EX evt. X = (Crypt {|Key(newK evt), Agent(Friend ia)|} (serverKey B)))" 1);
-by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
-by (asm_full_simp_tac (!simpset addsimps pushes) 1);
+(*Precisely formulated as needed below. Perhaps redundant, as simplification
+ with the aid of analz_subset_parts RS contra_subsetD might do the
+ same thing.*)
+goal thy
+ "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \
+\ Key (serverKey A) ~: \
+\ analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
+br (analz_subset_parts RS contra_subsetD) 1;
+by (Asm_simp_tac 1);
+qed "insert_not_analz_serverKey";
-by (excluded_middle_tac "ia=k" 1);
-(*Case where the key is compromised*)
-by (hyp_subst_tac 2);
-by (stac insert_commute 2); (*Pushes in the "insert X" for simplification*)
-by (Asm_full_simp_tac 2);
-
-
-
-by (asm_full_simp_tac (!simpset addsimps pushes) 1);
-
-by (REPEAT_FIRST Safe_step_tac);
-by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
-
-
-by (REPEAT (Safe_step_tac 1));
-
-
-
-by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
-
-by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
-
-by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); (*deletes the bad implication*)
-by ((forward_tac [Says_Server_message_form] THEN'
- fast_tac (!claset addSEs [traces_ConsE])) 1);
-by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
proof_timing:=true;
-(*Case where the key is secure*)
-by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
-by (asm_full_simp_tac
- (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
-
-
-
-by (full_simp_tac (!simpset addsimps [insert_Key_Agent_delay,
- insert_Key_Crypt_delay]) 1);
-
-by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1);
-by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
-
-
-by (asm_full_simp_tac
- (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
-
-
-by (stac insert_commute 1); (*Pushes in the "insert X" for simplification*)
-by (stac analyze_insert_Crypt 1);
-
-by (asm_full_simp_tac
- (!simpset addsimps [insert_not_analyze_serverKey,
- traces_ConsE RS insert_not_analyze_serverKey]) 1);
-
-
- 1. !!evs A B K NA S X evsa evs' ia evs'a.
- [| i ~= k; j ~= k;
- Says S (Friend ia)
- (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) #
- evs' :
- traces;
- Friend ia ~= B;
- Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} :
- setOfList evs';
- Says Server (Friend i)
- (Crypt
- {|N, Agent (Friend j), Key (newK evs'a),
- Crypt {|Key (newK evs'a), Agent (Friend i)|}
- (serverKey (Friend j))|}
- K') :
- setOfList evs';
- Key (newK evs'a) ~:
- analyze
- (insert
- (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
- (insert (Key (serverKey (Friend k))) (sees Enemy evs')));
- length evs'a < length evs' |] ==>
- Key (newK evs'a) ~:
- analyze
- (insert X
- (insert
- (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
- (insert (Key (serverKey (Friend k))) (sees Enemy evs'))))
-
-
-by (Asm_full_simp_tac 1);
-
-
-by (Simp_tac 2);
-
-
-by (Simp_tac 2);
-
-by (simp_tac (HOL_ss addsimps [insert_commute]) 2);
-
-
-by (simp_tac (HOL_ss addsimps [analyze_insert_insert]) 2);
-by (Asm_full_simp_tac 2);
-by (simp_tac (!simpset addsimps [insert_absorb]) 2);
-
-
-by (stac analyze_insert_Decrypt 2);
-
-
-goal thy "analyze (insert X (insert Y H)) = analyze (insert X (analyze (insert Y H)))";
-br analyze_insert_cong 1;
-by (Simp_tac 1);
-qed "analyze_insert_insert";
-
-
-
-
-
-
-
- 1. !!evs A B K NA S X evsa evs' ia evs'a.
- [| i ~= k; j ~= k;
- Says S (Friend ia)
- (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) #
- evs' :
- traces;
- Friend ia ~= B;
- Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} :
- setOfList evs';
- Says Server (Friend i)
- (Crypt
- {|N, Agent (Friend j), Key (newK evs'a),
- Crypt {|Key (newK evs'a), Agent (Friend i)|}
- (serverKey (Friend j))|}
- K') :
- setOfList evs';
- length evs'a < length evs'; ia ~= k;
- Key (newK evs'a) ~:
- analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs')) |] ==>
- Key (newK evs'a) ~:
- analyze
- (insert X
- (insert
- (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
- (insert (Key (serverKey (Friend k))) (sees Enemy evs'))))
-
-
-by (ALLGOALS Asm_full_simp_tac);
-
-by (Asm_full_simp_tac 1);
-
-by (asm_simp_tac (!simpset addsimps [insert_not_analyze_serverKey]) 1);
-fr insert_not_analyze_serverKey;
-by (fast_tac (!claset addSEs [traces_ConsE]) 1);
-
-by (forward_tac [traces_ConsE] 1);
-
-
-
-by (asm_full_simp_tac (!simpset addsimps [analyze_subset_parts RS contra_subsetD]) 1);
-
-
-
-auto();
-
-by (REPEAT_FIRST (resolve_tac [conjI, impI] (*DELETE NEXT TWO LINES??*)
- ORELSE' eresolve_tac [conjE]
- ORELSE' hyp_subst_tac));
-
-by (forward_tac [Says_Server_message_form] 2);
-
-bd Says_Server_message_form 2;
-by (fast_tac (!claset addSEs [traces_ConsE]) 2);
-auto();
-by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
-
-(*SUBGOAL 1: use analyze_insert_Crypt to pull out
- Crypt{|...|} (serverKey (Friend i))
- SUBGOAL 2: cannot do this, as we don't seem to have ia~=j
-*)
-
-
-
-qed "Enemy_not_see_encrypted_key";
-
-XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
-
-
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
@@ -1161,9 +922,9 @@
goal thy
"!!evs. evs : traces ==> \
\ ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
-\ : setOfList evs --> \
-\ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : setOfList evs | \
-\ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : setOfList evs)";
+\ : set_of_list evs --> \
+\ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \
+\ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)";
be traces.induct 1;
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
by (Step_tac 1);
@@ -1200,10 +961,10 @@
by (Best_tac 2);
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
-be Crypt_synthesize 1;
-be Key_synthesize 2;
+be Crypt_synth 1;
+be Key_synth 2;
-(*Split up the possibilities of that message being synthesized...*)
+(*Split up the possibilities of that message being synthd...*)
by (Step_tac 1);
by (Best_tac 6);
--- a/src/HOL/Auth/Message.ML Mon Aug 19 11:19:16 1996 +0200
+++ b/src/HOL/Auth/Message.ML Mon Aug 19 11:19:55 1996 +0200
@@ -4,30 +4,12 @@
Copyright 1996 University of Cambridge
Datatypes of agents and messages;
-Inductive relations "parts", "analyze" and "synthesize"
+Inductive relations "parts", "analz" and "synth"
*)
open Message;
-(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
-
-(*Maybe swap the safe_tac and simp_tac lines?**)
-fun auto_tac (cs,ss) =
- TRY (safe_tac cs) THEN
- ALLGOALS (asm_full_simp_tac ss) THEN
- REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
-
-fun Auto_tac() = auto_tac (!claset, !simpset);
-
-fun auto() = by (Auto_tac());
-
-fun impOfSubs th = th RSN (2, rev_subsetD);
-
-(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
-
-
-
(** Inverse of keys **)
goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
@@ -172,7 +154,7 @@
by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
qed "parts_UN1";
-(*Added to simplify arguments to parts, analyze and synthesize*)
+(*Added to simplify arguments to parts, analz and synth*)
Addsimps [parts_Un, parts_UN, parts_UN1];
goal thy "insert X (parts H) <= parts(insert X H)";
@@ -259,362 +241,360 @@
parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
-(**** Inductive relation "analyze" ****)
+(**** Inductive relation "analz" ****)
val major::prems =
-goal thy "[| {|X,Y|} : analyze H; \
-\ [| X : analyze H; Y : analyze H |] ==> P \
+goal thy "[| {|X,Y|} : analz H; \
+\ [| X : analz H; Y : analz H |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
brs prems 1;
-by (REPEAT (eresolve_tac [asm_rl, analyze.Fst, analyze.Snd] 1));
-qed "MPair_analyze";
+by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
+qed "MPair_analz";
-AddIs [analyze.Inj];
-AddSEs [MPair_analyze];
-AddDs [analyze.Decrypt];
+AddIs [analz.Inj];
+AddSEs [MPair_analz];
+AddDs [analz.Decrypt];
-Addsimps [analyze.Inj];
+Addsimps [analz.Inj];
-goal thy "H <= analyze(H)";
+goal thy "H <= analz(H)";
by (Fast_tac 1);
-qed "analyze_increasing";
+qed "analz_increasing";
-goal thy "analyze H <= parts H";
+goal thy "analz H <= parts H";
by (rtac subsetI 1);
-be analyze.induct 1;
+be analz.induct 1;
by (ALLGOALS Fast_tac);
-qed "analyze_subset_parts";
+qed "analz_subset_parts";
-bind_thm ("not_parts_not_analyze", analyze_subset_parts RS contra_subsetD);
+bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
-goal thy "parts (analyze H) = parts H";
+goal thy "parts (analz H) = parts H";
br equalityI 1;
-br (analyze_subset_parts RS parts_mono RS subset_trans) 1;
+br (analz_subset_parts RS parts_mono RS subset_trans) 1;
by (Simp_tac 1);
-by (fast_tac (!claset addDs [analyze_increasing RS parts_mono RS subsetD]) 1);
-qed "parts_analyze";
-Addsimps [parts_analyze];
+by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
+qed "parts_analz";
+Addsimps [parts_analz];
-goal thy "analyze (parts H) = parts H";
+goal thy "analz (parts H) = parts H";
by (Auto_tac());
-be analyze.induct 1;
+be analz.induct 1;
by (Auto_tac());
-qed "analyze_parts";
-Addsimps [analyze_parts];
+qed "analz_parts";
+Addsimps [analz_parts];
(*Monotonicity; Lemma 1 of Lowe*)
-goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)";
+goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
-qed "analyze_mono";
+qed "analz_mono";
(** General equational properties **)
-goal thy "analyze{} = {}";
+goal thy "analz{} = {}";
by (Step_tac 1);
-be analyze.induct 1;
+be analz.induct 1;
by (ALLGOALS Fast_tac);
-qed "analyze_empty";
-Addsimps [analyze_empty];
+qed "analz_empty";
+Addsimps [analz_empty];
-(*Converse fails: we can analyze more from the union than from the
+(*Converse fails: we can analz more from the union than from the
separate parts, as a key in one might decrypt a message in the other*)
-goal thy "analyze(G) Un analyze(H) <= analyze(G Un H)";
-by (REPEAT (ares_tac [Un_least, analyze_mono, Un_upper1, Un_upper2] 1));
-qed "analyze_Un";
+goal thy "analz(G) Un analz(H) <= analz(G Un H)";
+by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
+qed "analz_Un";
-goal thy "insert X (analyze H) <= analyze(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs analyze_mono]) 1);
-qed "analyze_insert";
+goal thy "insert X (analz H) <= analz(insert X H)";
+by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1);
+qed "analz_insert";
(** Rewrite rules for pulling out atomic messages **)
-goal thy "analyze (insert (Agent agt) H) = insert (Agent agt) (analyze H)";
-by (rtac (analyze_insert RSN (2, equalityI)) 1);
+goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
+by (rtac (analz_insert RSN (2, equalityI)) 1);
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
(*Simplification breaks up equalities between messages;
how to make it work for fast_tac??*)
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "analyze_insert_Agent";
+qed "analz_insert_Agent";
-goal thy "analyze (insert (Nonce N) H) = insert (Nonce N) (analyze H)";
-by (rtac (analyze_insert RSN (2, equalityI)) 1);
+goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
+by (rtac (analz_insert RSN (2, equalityI)) 1);
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "analyze_insert_Nonce";
+qed "analz_insert_Nonce";
(*Can only pull out Keys if they are not needed to decrypt the rest*)
goalw thy [keysFor_def]
- "!!K. K ~: keysFor (analyze H) ==> \
-\ analyze (insert (Key K) H) = insert (Key K) (analyze H)";
-by (rtac (analyze_insert RSN (2, equalityI)) 1);
+ "!!K. K ~: keysFor (analz H) ==> \
+\ analz (insert (Key K) H) = insert (Key K) (analz H)";
+by (rtac (analz_insert RSN (2, equalityI)) 1);
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "analyze_insert_Key";
+qed "analz_insert_Key";
-goal thy "analyze (insert {|X,Y|} H) = \
-\ insert {|X,Y|} (analyze (insert X (insert Y H)))";
+goal thy "analz (insert {|X,Y|} H) = \
+\ insert {|X,Y|} (analz (insert X (insert Y H)))";
br equalityI 1;
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
by (Auto_tac());
-be analyze.induct 1;
-by (ALLGOALS (deepen_tac (!claset addIs [analyze.Fst, analyze.Snd, analyze.Decrypt]) 0));
-qed "analyze_insert_MPair";
+be analz.induct 1;
+by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
+qed "analz_insert_MPair";
(*Can pull out enCrypted message if the Key is not known*)
-goal thy "!!H. Key (invKey K) ~: analyze H ==> \
-\ analyze (insert (Crypt X K) H) = \
-\ insert (Crypt X K) (analyze H)";
-by (rtac (analyze_insert RSN (2, equalityI)) 1);
+goal thy "!!H. Key (invKey K) ~: analz H ==> \
+\ analz (insert (Crypt X K) H) = \
+\ insert (Crypt X K) (analz H)";
+by (rtac (analz_insert RSN (2, equalityI)) 1);
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "analyze_insert_Crypt";
+qed "analz_insert_Crypt";
-goal thy "!!H. Key (invKey K) : analyze H ==> \
-\ analyze (insert (Crypt X K) H) <= \
-\ insert (Crypt X K) (analyze (insert X H))";
+goal thy "!!H. Key (invKey K) : analz H ==> \
+\ analz (insert (Crypt X K) H) <= \
+\ insert (Crypt X K) (analz (insert X H))";
br subsetI 1;
-by (eres_inst_tac [("za","x")] analyze.induct 1);
+by (eres_inst_tac [("za","x")] analz.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
val lemma1 = result();
-goal thy "!!H. Key (invKey K) : analyze H ==> \
-\ insert (Crypt X K) (analyze (insert X H)) <= \
-\ analyze (insert (Crypt X K) H)";
+goal thy "!!H. Key (invKey K) : analz H ==> \
+\ insert (Crypt X K) (analz (insert X H)) <= \
+\ analz (insert (Crypt X K) H)";
by (Auto_tac());
-by (eres_inst_tac [("za","x")] analyze.induct 1);
+by (eres_inst_tac [("za","x")] analz.induct 1);
by (Auto_tac());
-by (best_tac (!claset addIs [subset_insertI RS analyze_mono RS subsetD,
- analyze.Decrypt]) 1);
+by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
+ analz.Decrypt]) 1);
val lemma2 = result();
-goal thy "!!H. Key (invKey K) : analyze H ==> \
-\ analyze (insert (Crypt X K) H) = \
-\ insert (Crypt X K) (analyze (insert X H))";
+goal thy "!!H. Key (invKey K) : analz H ==> \
+\ analz (insert (Crypt X K) H) = \
+\ insert (Crypt X K) (analz (insert X H))";
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
-qed "analyze_insert_Decrypt";
+qed "analz_insert_Decrypt";
(*Case analysis: either the message is secure, or it is not!
Use with expand_if; apparently split_tac does not cope with patterns
- such as "analyze (insert (Crypt X' K) H)" *)
-goal thy "analyze (insert (Crypt X' K) H) = \
-\ (if (Key (invKey K) : analyze H) then \
-\ insert (Crypt X' K) (analyze (insert X' H)) \
-\ else insert (Crypt X' K) (analyze H))";
-by (excluded_middle_tac "Key (invKey K) : analyze H " 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [analyze_insert_Crypt,
- analyze_insert_Decrypt])));
-qed "analyze_Crypt_if";
+ such as "analz (insert (Crypt X' K) H)" *)
+goal thy "analz (insert (Crypt X' K) H) = \
+\ (if (Key (invKey K) : analz H) then \
+\ insert (Crypt X' K) (analz (insert X' H)) \
+\ else insert (Crypt X' K) (analz H))";
+by (excluded_middle_tac "Key (invKey K) : analz H " 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt,
+ analz_insert_Decrypt])));
+qed "analz_Crypt_if";
-Addsimps [analyze_insert_Agent, analyze_insert_Nonce,
- analyze_insert_Key, analyze_insert_MPair,
- analyze_Crypt_if];
+Addsimps [analz_insert_Agent, analz_insert_Nonce,
+ analz_insert_Key, analz_insert_MPair,
+ analz_Crypt_if];
(*This rule supposes "for the sake of argument" that we have the key.*)
-goal thy "analyze (insert (Crypt X K) H) <= \
-\ insert (Crypt X K) (analyze (insert X H))";
+goal thy "analz (insert (Crypt X K) H) <= \
+\ insert (Crypt X K) (analz (insert X H))";
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
by (Auto_tac());
-qed "analyze_insert_Crypt_subset";
+qed "analz_insert_Crypt_subset";
(** Idempotence and transitivity **)
-goal thy "!!H. X: analyze (analyze H) ==> X: analyze H";
-be analyze.induct 1;
+goal thy "!!H. X: analz (analz H) ==> X: analz H";
+be analz.induct 1;
by (ALLGOALS Fast_tac);
-qed "analyze_analyzeE";
-AddSEs [analyze_analyzeE];
+qed "analz_analzE";
+AddSEs [analz_analzE];
-goal thy "analyze (analyze H) = analyze H";
+goal thy "analz (analz H) = analz H";
by (Fast_tac 1);
-qed "analyze_idem";
-Addsimps [analyze_idem];
+qed "analz_idem";
+Addsimps [analz_idem];
-goal thy "!!H. [| X: analyze G; G <= analyze H |] ==> X: analyze H";
-by (dtac analyze_mono 1);
+goal thy "!!H. [| X: analz G; G <= analz H |] ==> X: analz H";
+by (dtac analz_mono 1);
by (Fast_tac 1);
-qed "analyze_trans";
+qed "analz_trans";
(*Cut; Lemma 2 of Lowe*)
-goal thy "!!H. [| X: analyze H; Y: analyze (insert X H) |] ==> Y: analyze H";
-be analyze_trans 1;
+goal thy "!!H. [| X: analz H; Y: analz (insert X H) |] ==> Y: analz H";
+be analz_trans 1;
by (Fast_tac 1);
-qed "analyze_cut";
+qed "analz_cut";
(*Cut can be proved easily by induction on
- "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H"
+ "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H"
*)
-(** A congruence rule for "analyze" **)
+(** A congruence rule for "analz" **)
-goal thy "!!H. [| analyze G <= analyze G'; analyze H <= analyze H' \
-\ |] ==> analyze (G Un H) <= analyze (G' Un H')";
+goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
+\ |] ==> analz (G Un H) <= analz (G' Un H')";
by (Step_tac 1);
-be analyze.induct 1;
-by (ALLGOALS (best_tac (!claset addIs [analyze_mono RS subsetD])));
-qed "analyze_subset_cong";
+be analz.induct 1;
+by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD])));
+qed "analz_subset_cong";
-goal thy "!!H. [| analyze G = analyze G'; analyze H = analyze H' \
-\ |] ==> analyze (G Un H) = analyze (G' Un H')";
-by (REPEAT_FIRST (ares_tac [equalityI, analyze_subset_cong]
+goal thy "!!H. [| analz G = analz G'; analz H = analz H' \
+\ |] ==> analz (G Un H) = analz (G' Un H')";
+by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
ORELSE' etac equalityE));
-qed "analyze_cong";
+qed "analz_cong";
-goal thy "!!H. analyze H = analyze H' ==> \
-\ analyze (insert X H) = analyze (insert X H')";
+goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
by (asm_simp_tac (!simpset addsimps [insert_def]
- setloop (rtac analyze_cong)) 1);
-qed "analyze_insert_cong";
+ setloop (rtac analz_cong)) 1);
+qed "analz_insert_cong";
-(*If there are no pairs or encryptions then analyze does nothing*)
+(*If there are no pairs or encryptions then analz does nothing*)
goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt X K ~: H |] ==> \
-\ analyze H = H";
+\ analz H = H";
by (Step_tac 1);
-be analyze.induct 1;
+be analz.induct 1;
by (ALLGOALS Fast_tac);
-qed "analyze_trivial";
+qed "analz_trivial";
(*Helps to prove Fake cases*)
-goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)";
-be analyze.induct 1;
-by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analyze_mono])));
+goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
+be analz.induct 1;
+by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
val lemma = result();
-goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)";
+goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
by (fast_tac (!claset addIs [lemma]
- addEs [impOfSubs analyze_mono]) 1);
-qed "analyze_UN_analyze";
-Addsimps [analyze_UN_analyze];
+ addEs [impOfSubs analz_mono]) 1);
+qed "analz_UN_analz";
+Addsimps [analz_UN_analz];
-(**** Inductive relation "synthesize" ****)
+(**** Inductive relation "synth" ****)
-AddIs synthesize.intrs;
+AddIs synth.intrs;
-goal thy "H <= synthesize(H)";
+goal thy "H <= synth(H)";
by (Fast_tac 1);
-qed "synthesize_increasing";
+qed "synth_increasing";
(*Monotonicity*)
-goalw thy synthesize.defs "!!G H. G<=H ==> synthesize(G) <= synthesize(H)";
+goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
-qed "synthesize_mono";
+qed "synth_mono";
(** Unions **)
-(*Converse fails: we can synthesize more from the union than from the
+(*Converse fails: we can synth more from the union than from the
separate parts, building a compound message using elements of each.*)
-goal thy "synthesize(G) Un synthesize(H) <= synthesize(G Un H)";
-by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1));
-qed "synthesize_Un";
+goal thy "synth(G) Un synth(H) <= synth(G Un H)";
+by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
+qed "synth_Un";
-goal thy "insert X (synthesize H) <= synthesize(insert X H)";
-by (fast_tac (!claset addEs [impOfSubs synthesize_mono]) 1);
-qed "synthesize_insert";
+goal thy "insert X (synth H) <= synth(insert X H)";
+by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1);
+qed "synth_insert";
(** Idempotence and transitivity **)
-goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H";
-be synthesize.induct 1;
+goal thy "!!H. X: synth (synth H) ==> X: synth H";
+be synth.induct 1;
by (ALLGOALS Fast_tac);
-qed "synthesize_synthesizeE";
-AddSEs [synthesize_synthesizeE];
+qed "synth_synthE";
+AddSEs [synth_synthE];
-goal thy "synthesize (synthesize H) = synthesize H";
+goal thy "synth (synth H) = synth H";
by (Fast_tac 1);
-qed "synthesize_idem";
+qed "synth_idem";
-goal thy "!!H. [| X: synthesize G; G <= synthesize H |] ==> X: synthesize H";
-by (dtac synthesize_mono 1);
+goal thy "!!H. [| X: synth G; G <= synth H |] ==> X: synth H";
+by (dtac synth_mono 1);
by (Fast_tac 1);
-qed "synthesize_trans";
+qed "synth_trans";
(*Cut; Lemma 2 of Lowe*)
-goal thy "!!H. [| X: synthesize H; Y: synthesize (insert X H) \
-\ |] ==> Y: synthesize H";
-be synthesize_trans 1;
+goal thy "!!H. [| X: synth H; Y: synth (insert X H) |] ==> Y: synth H";
+be synth_trans 1;
by (Fast_tac 1);
-qed "synthesize_cut";
+qed "synth_cut";
(*Can only produce a nonce or key if it is already known,
- but can synthesize a pair or encryption from its components...*)
-val mk_cases = synthesize.mk_cases msg.simps;
+ but can synth a pair or encryption from its components...*)
+val mk_cases = synth.mk_cases msg.simps;
-(*NO Agent_synthesize, as any Agent name can be synthesized*)
-val Nonce_synthesize = mk_cases "Nonce n : synthesize H";
-val Key_synthesize = mk_cases "Key K : synthesize H";
-val MPair_synthesize = mk_cases "{|X,Y|} : synthesize H";
-val Crypt_synthesize = mk_cases "Crypt X K : synthesize H";
+(*NO Agent_synth, as any Agent name can be synthd*)
+val Nonce_synth = mk_cases "Nonce n : synth H";
+val Key_synth = mk_cases "Key K : synth H";
+val MPair_synth = mk_cases "{|X,Y|} : synth H";
+val Crypt_synth = mk_cases "Crypt X K : synth H";
-AddSEs [Nonce_synthesize, Key_synthesize, MPair_synthesize, Crypt_synthesize];
+AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth];
-goal thy "(Nonce N : synthesize H) = (Nonce N : H)";
+goal thy "(Nonce N : synth H) = (Nonce N : H)";
by (Fast_tac 1);
-qed "Nonce_synthesize_eq";
+qed "Nonce_synth_eq";
-goal thy "(Key K : synthesize H) = (Key K : H)";
+goal thy "(Key K : synth H) = (Key K : H)";
by (Fast_tac 1);
-qed "Key_synthesize_eq";
+qed "Key_synth_eq";
-Addsimps [Nonce_synthesize_eq, Key_synthesize_eq];
+Addsimps [Nonce_synth_eq, Key_synth_eq];
goalw thy [keysFor_def]
- "keysFor (synthesize H) = keysFor H Un invKey``{K. Key K : H}";
+ "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
by (Fast_tac 1);
-qed "keysFor_synthesize";
-Addsimps [keysFor_synthesize];
+qed "keysFor_synth";
+Addsimps [keysFor_synth];
-(*** Combinations of parts, analyze and synthesize ***)
+(*** Combinations of parts, analz and synth ***)
-goal thy "parts (synthesize H) = parts H Un synthesize H";
+goal thy "parts (synth H) = parts H Un synth H";
br equalityI 1;
br subsetI 1;
be parts.induct 1;
by (ALLGOALS
- (best_tac (!claset addIs ((synthesize_increasing RS parts_mono RS subsetD)
+ (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
::parts.intrs))));
-qed "parts_synthesize";
-Addsimps [parts_synthesize];
+qed "parts_synth";
+Addsimps [parts_synth];
-goal thy "analyze (synthesize H) = analyze H Un synthesize H";
+goal thy "analz (synth H) = analz H Un synth H";
br equalityI 1;
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
by (best_tac
- (!claset addIs [synthesize_increasing RS analyze_mono RS subsetD]) 5);
+ (!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5);
(*Strange that best_tac just can't hack this one...*)
-by (ALLGOALS (deepen_tac (!claset addIs analyze.intrs) 0));
-qed "analyze_synthesize";
-Addsimps [analyze_synthesize];
+by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
+qed "analz_synth";
+Addsimps [analz_synth];
(*Hard to prove; still needed now that there's only one Enemy?*)
-goal thy "analyze (UN i. synthesize (H i)) = \
-\ analyze (UN i. H i) Un (UN i. synthesize (H i))";
+goal thy "analz (UN i. synth (H i)) = \
+\ analz (UN i. H i) Un (UN i. synth (H i))";
br equalityI 1;
br subsetI 1;
-be analyze.induct 1;
+be analz.induct 1;
by (best_tac
- (!claset addEs [impOfSubs synthesize_increasing,
- impOfSubs analyze_mono]) 5);
+ (!claset addEs [impOfSubs synth_increasing,
+ impOfSubs analz_mono]) 5);
by (Best_tac 1);
-by (deepen_tac (!claset addIs [analyze.Fst]) 0 1);
-by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);
-by (deepen_tac (!claset addSEs [analyze.Decrypt]
- addIs [analyze.Decrypt]) 0 1);
-qed "analyze_UN1_synthesize";
-Addsimps [analyze_UN1_synthesize];
+by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
+by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
+by (deepen_tac (!claset addSEs [analz.Decrypt]
+ addIs [analz.Decrypt]) 0 1);
+qed "analz_UN1_synth";
+Addsimps [analz_UN1_synth];