--- a/src/HOL/Auth/NS_Shared.ML Mon Sep 09 17:34:24 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Mon Sep 09 17:44:20 1996 +0200
@@ -54,7 +54,7 @@
(*Enemy never sees another agent's shared key!*)
goal thy
- "!!evs. [| evs : ns_shared; A ~= Enemy |] ==> \
+ "!!evs. [| evs : ns_shared; A ~= Enemy; A ~: Friend``leaked |] ==> \
\ Key (shrK A) ~: parts (sees Enemy evs)";
be ns_shared.induct 1;
bd NS3_msg_in_parts_sees_Enemy 5;
@@ -72,16 +72,21 @@
Enemy_not_analz_shrK,
not_sym RSN (2, Enemy_not_analz_shrK)];
-(*We go to some trouble to preserve R in the 3rd subgoal*)
+(*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
+ REDO USING 'BAD' SET TO AVOID CASE SPLIT!*)
val major::prems =
-goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
-\ evs : ns_shared; \
-\ A=Enemy ==> R \
+goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
+\ evs : ns_shared; \
+\ A=Enemy ==> R; \
+\ !!i. [| A = Friend i; i: leaked |] ==> R \
\ |] ==> R";
br ccontr 1;
br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
+br notI 3;
+be imageE 3;
by (swap_res_tac prems 2);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
+by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems)));
qed "Enemy_see_shrK_E";
bind_thm ("Enemy_analz_shrK_E",
@@ -91,23 +96,11 @@
AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
-(*No Friend will ever see another agent's shared key
- (excluding the Enemy, who might transmit his).
- The Server, of course, knows all shared keys.*)
-goal thy
- "!!evs. [| evs : ns_shared; A ~= Enemy; A ~= Friend j |] ==> \
-\ Key (shrK A) ~: parts (sees (Friend j) evs)";
-br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
-by (ALLGOALS Asm_simp_tac);
-qed "Friend_not_see_shrK";
-
-
(*Not for Addsimps -- it can cause goals to blow up!*)
goal thy
- "!!evs. evs : ns_shared ==> \
-\ (Key (shrK A) \
-\ : analz (insert (Key (shrK B)) (sees Enemy evs))) = \
-\ (A=B | A=Enemy)";
+ "!!evs. evs : ns_shared ==> \
+\ (Key (shrK A) : analz (sees Enemy evs)) = \
+\ (A=Enemy | A : Friend``leaked)";
by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
addIs [impOfSubs (subset_insertI RS analz_mono)]
addss (!simpset)) 1);
@@ -212,63 +205,54 @@
(*Describes the form of X when the following message is sent. The use of
- "parts" strengthens the induction hyp for proving the Fake case*)
+ "parts" strengthens the induction hyp for proving the Fake case. The
+ assumptions on A are needed to prevent its being a Faked message.*)
goal thy
- "!!evs. evs : ns_shared ==> \
-\ ALL A NA B K X. \
-\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
-\ : parts (sees Enemy evs) & A ~= Enemy --> \
+ "!!evs. evs : ns_shared ==> \
+\ ALL A NA B K X. \
+\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
+\ : parts (sees Enemy evs) & \
+\ A ~= Enemy & A ~: Friend``leaked --> \
\ (EX evt:ns_shared. K = newK evt & \
\ X = (Crypt {|Key K, Agent A|} (shrK B)))";
be ns_shared.induct 1;
bd NS3_msg_in_parts_sees_Enemy 5;
by (Step_tac 1);
by (ALLGOALS Asm_full_simp_tac);
+by (fast_tac (!claset addss (!simpset)) 1);
(*Remaining cases are Fake and NS2*)
by (fast_tac (!claset addSDs [spec]) 2);
(*Now for the Fake case*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
+by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
addss (!simpset)) 1);
qed_spec_mp "encrypted_form";
-(*For eliminating the A ~= Enemy condition from the previous result*)
-goal thy
- "!!evs. evs : ns_shared ==> \
-\ ALL S A NA B K X. \
-\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
-\ : set_of_list evs --> \
-\ S = Server | S = Enemy";
-be ns_shared.induct 1;
-by (ALLGOALS Asm_simp_tac);
-(*We are left with NS3*)
-by (subgoal_tac "S = Server | S = Enemy" 1);
-(*First justify this assumption!*)
-by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
-by (Step_tac 1);
-bd Says_Server_message_form 1;
-by (ALLGOALS Full_simp_tac);
-(*Final case. Clear out needless quantifiers to speed the following step*)
-by (thin_tac "ALL x. ?P(x)" 1);
-bd encrypted_form 1;
-br (parts.Inj RS conjI) 1;
-auto();
-qed_spec_mp "Server_or_Enemy";
+(*If such a message is sent with a bad key then the Enemy sees it (even if
+ he didn't send it in the first place).*)
+goal thy
+ "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
+\ : set_of_list evs; \
+\ A = Enemy | A : Friend``leaked |] \
+\ ==> X : analz (sees Enemy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
+ addss (!simpset)) 1);
+qed_spec_mp "bad_encrypted_form";
-(*Describes the form of X when the following message is sent;
- use Says_Server_message_form if applicable*)
+
+(*EITHER describes the form of X when the following message is sent,
+ OR reduces it to the Fake case.
+ Use Says_Server_message_form if applicable.*)
goal thy
"!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
-\ : set_of_list evs; \
-\ evs : ns_shared |] \
+\ : set_of_list evs; evs : ns_shared |] \
\ ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
-\ X = (Crypt {|Key K, Agent A|} (shrK B)))";
-by (forward_tac [Server_or_Enemy] 1);
-ba 1;
-by (Step_tac 1);
-by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
+\ X = (Crypt {|Key K, Agent A|} (shrK B))) | \
+\ X : analz (sees Enemy evs)";
+by (excluded_middle_tac "A = Enemy | A : Friend``leaked" 1);
+by (fast_tac (!claset addIs [bad_encrypted_form]) 2);
by (forward_tac [encrypted_form] 1);
br (parts.Inj RS conjI) 1;
by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
@@ -279,9 +263,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt))
- (insert (Key (shrK C)) (sees Enemy evs))) ==>
- Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
+ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
+ Key K : analz (sees Enemy evs)
A more general formula must be proved inductively.
@@ -302,8 +285,8 @@
by (best_tac (!claset addSEs partsEs
addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un]
- addss (!simpset)) 1);
-(*NS4 and NS5*)
+ addss (!simpset)) 2);
+(*Base, NS4 and NS5*)
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
result();
@@ -313,6 +296,9 @@
Delsimps [image_insert];
Addsimps [image_insert RS sym];
+Delsimps [image_Un];
+Addsimps [image_Un RS sym];
+
goal thy "insert (Key (newK x)) (sees A evs) = \
\ Key `` (newK``{x}) Un (sees A evs)";
by (Fast_tac 1);
@@ -328,23 +314,30 @@
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
- "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \
-\ (K : nE | Key K : analz (insert KsC sEe)) ==> \
-\ (Key K : analz (insert KsC (Key``nE Un sEe))) = \
-\ (K : nE | Key K : analz (insert KsC sEe))";
+ "!!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();
+(*Copied from OtwayRees.ML*)
+val enemy_analz_tac =
+ SELECT_GOAL
+ (EVERY [REPEAT (resolve_tac [impI,notI] 1),
+ dtac (impOfSubs Fake_analz_insert) 1,
+ eresolve_tac [asm_rl, synth.Inj] 1,
+ Fast_tac 1,
+ Asm_full_simp_tac 1,
+ IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
+ ]);
+
goal thy
"!!evs. evs : ns_shared ==> \
-\ ALL K E. (Key K : analz (insert (Key (shrK C)) \
-\ (Key``(newK``E) Un (sees Enemy evs)))) = \
-\ (K : newK``E | \
-\ Key K : analz (insert (Key (shrK C)) \
-\ (sees Enemy evs)))";
+\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
+\ (K : newK``E | Key K : analz (sees Enemy evs))";
be ns_shared.induct 1;
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
-by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
+by (REPEAT ((eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac) 5));
by (REPEAT_FIRST (resolve_tac [allI, lemma]));
by (ALLGOALS
(asm_simp_tac
@@ -352,18 +345,14 @@
@ pushes)
setloop split_tac [expand_if])));
(** LEVEL 5 **)
+(*NS3, Fake subcase*)
+by (enemy_analz_tac 5);
(*Cases NS2 and NS3!! Simple, thanks to auto case splits*)
by (REPEAT (Fast_tac 3));
-(*Fake case*) (** LEVEL 6 **)
+(*Fake case*) (** LEVEL 7 **)
by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")]
(insert_commute RS ssubst) 2);
-(*This is enemy_analz_tac from OtwayRees.ML*)
-by (EVERY [rtac impI 2,
- dtac (impOfSubs Fake_analz_insert) 2,
- eresolve_tac [asm_rl, synth.Inj] 2,
- Fast_tac 2,
- Asm_full_simp_tac 2,
- deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 2]);
+by (enemy_analz_tac 2);
(*Base case*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
qed_spec_mp "analz_image_newK";
@@ -371,61 +360,68 @@
goal thy
"!!evs. evs : ns_shared ==> \
-\ Key K : analz (insert (Key (newK evt)) \
-\ (insert (Key (shrK C)) \
-\ (sees Enemy evs))) = \
-\ (K = newK evt | \
-\ Key K : analz (insert (Key (shrK C)) \
-\ (sees Enemy evs)))";
+\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
+\ (K = newK evt | Key K : analz (sees Enemy 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";
+(** First, two lemmas for the Fake and NS3 cases **)
+
+goal thy
+ "!!evs. [| X : synth (analz (sees Enemy evs)); \
+\ Crypt X' (shrK C) : parts{X}; \
+\ C ~= Enemy; C ~: Friend``leaked; evs : ns_shared |] \
+\ ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
+by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs parts_insert_subset_Un]
+ addss (!simpset)) 1);
+qed "Crypt_Fake_parts";
+
+goal thy
+ "!!evs. [| Crypt X' K : parts (sees A evs); evs : ns_shared |] \
+\ ==> EX S S' Y. Says S S' Y : set_of_list evs & \
+\ Crypt X' K : parts {Y}";
+bd parts_singleton 1;
+by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
+qed "Crypt_parts_singleton";
+
+fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
(*This says that the Key, K, uniquely identifies the message.
- But if C=Enemy then he could send all sorts of nonsense.*)
+ But if Enemy knows C's key then he could send all sorts of nonsense.*)
goal thy
"!!evs. evs : ns_shared ==> \
-\ EX X'. ALL C S A Y N B X. \
-\ C ~= Enemy --> \
-\ Says S A Y : set_of_list evs --> \
-\ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> X=X')";
+\ EX X'. ALL C. \
+\ C ~= Enemy & C ~: Friend``leaked --> \
+\ (ALL S A Y. Says S A Y : set_of_list evs --> \
+\ (ALL N B X. Crypt {|N, Agent B, Key K, X|} (shrK C) : parts{Y} --> \
+\ X=X'))";
be ns_shared.induct 1;
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
+by (REPEAT_FIRST (eresolve_tac [exE,disjE]));
+(*NS3: Fake (compromised) case*)
+by (ex_strip_tac 4);
+by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts,
+ Crypt_parts_singleton]) 4);
+(*NS3: Good case, no relevant messages*)
+by (fast_tac (!claset addSEs [exI] addss (!simpset)) 3);
(*NS2: Case split propagates some context to other subgoal...*)
by (excluded_middle_tac "K = newK evsa" 2);
by (Asm_simp_tac 2);
+be exI 2;
(*...we assume X is a very new message, and handle this case by contradiction*)
by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
addSEs partsEs
addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset)) 2);
-(*NS3: No relevant messages*)
-by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2);
-(*Fake*)
-by (Step_tac 1);
-br exI 1;
-br conjI 1;
-ba 2;
-by (Step_tac 1);
-(** LEVEL 12 **)
-by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \
-\ : parts (sees Enemy evsa)" 1);
-by (thin_tac "ALL S.?P(S)" 2);
-by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
- addDs [impOfSubs parts_insert_subset_Un]
- addss (!simpset)) 2);
-by (thin_tac "?aa : parts {X}" 1);
-bd parts_singleton 1;
-by (Step_tac 1);
-bd seesD 1;
-by (Step_tac 1);
-by (Full_simp_tac 2);
-by (fast_tac (!claset addSDs [spec]) 1);
+(*Fake*) (** LEVEL 11 **)
+by (ex_strip_tac 1);
+by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
val lemma = result();
@@ -433,31 +429,33 @@
goal thy
"!!evs. [| Says S A \
\ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \
-\ : set_of_list evs; \
- \ Says S' A' \
+\ : set_of_list evs; \
+\ Says S' A' \
\ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
\ : set_of_list evs; \
-\ evs : ns_shared; C ~= Enemy; C' ~= Enemy |] ==> X = X'";
+\ evs : ns_shared; C ~= Enemy; C ~: Friend``leaked; C' ~= Enemy; C' ~: Friend``leaked |] ==> X = X'";
bd lemma 1;
be exE 1;
+(*Duplicate the assumption*)
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (Fast_tac 1);
+(*Are these instantiations essential?*)
+by (dres_inst_tac [("x","C")] spec 1);
+by (dres_inst_tac [("x","C'")] spec 1);
+by (fast_tac (!claset addSDs [spec]) 1);
qed "unique_session_keys";
-(*Crucial secrecy property: Enemy does not see the keys sent in msg NS2
- -- even if another key is compromised*)
+(*Crucial secrecy property: Enemy does not see the keys sent in msg NS2*)
goal thy
- "!!evs. [| Says Server (Friend i) \
+ "!!evs. [| Says Server (Friend i) \
\ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \
-\ evs : ns_shared; Friend i ~= C; Friend j ~= C \
-\ |] ==> \
-\ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
+\ i ~: leaked; j ~: leaked; evs : ns_shared \
+\ |] ==> \
+\ K ~: analz (sees Enemy evs)";
be rev_mp 1;
be ns_shared.induct 1;
-(*TRY CHANGING NEXT CMD TO by (ALLGOALS Asm_simp_tac);*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
+by (ALLGOALS Asm_simp_tac);
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
@@ -469,36 +467,28 @@
setloop split_tac [expand_if])));
(*NS2*)
by (fast_tac (!claset addSEs [less_irrefl]) 2);
-(** LEVEL 8 **)
-(*Now for the Fake case*)
-br notI 1;
-by (subgoal_tac
- "Key (newK evt) : \
-\ analz (synth (analz (insert (Key (shrK C)) \
-\ (sees Enemy evsa))))" 1);
-be (impOfSubs analz_mono) 2;
-by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
- impOfSubs synth_increasing,
- impOfSubs analz_increasing]) 0 2);
-(*Proves the Fake goal*)
-by (fast_tac (!claset addss (!simpset)) 1);
-
-(**LEVEL 13**)
+(*Fake case*) (** LEVEL 8 **)
+by (enemy_analz_tac 1);
(*NS3: that message from the Server was sent earlier*)
by (mp_tac 1);
by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
-by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
+by (REPEAT_FIRST (eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac));
+by (enemy_analz_tac 2); (*Prove the Fake subcase*)
by (asm_full_simp_tac
(!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
-by (Step_tac 1);
-(**LEVEL 18 **)
+(**************** by (Step_tac 1); ****************)
+by (step_tac HOL_cs 1);
+(**LEVEL 15 **)
+by (excluded_middle_tac "ia : leaked" 1);
+bd (Says_imp_sees_Enemy RS analz.Inj) 2;
+bd analz.Decrypt 2;
+by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 2);
+by (Fast_tac 2);
+(*So now we know that Friend ia is a good agent*)
bd unique_session_keys 1;
by (REPEAT_FIRST assume_tac);
by (ALLGOALS Full_simp_tac);
by (Step_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1);
+by (auto_tac (!claset, !simpset addsimps [shrK_mem_analz]));
qed "Enemy_not_see_encrypted_key";
-
-
-