--- a/src/HOL/Auth/NS_Shared.ML Tue Sep 03 17:54:39 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Tue Sep 03 18:24:42 1996 +0200
@@ -12,6 +12,8 @@
open NS_Shared;
+proof_timing:=true;
+
(**** Inductive proofs about ns_shared ****)
(*The Enemy can see more than anybody else, except for their initial state*)
@@ -40,7 +42,7 @@
AddSEs [not_Notes RSN (2, rev_notE)];
-(*For reasoning about message NS3*)
+(*For reasoning about the encrypted portion of message NS3*)
goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
\ X : parts (sees Enemy evs)";
by (fast_tac (!claset addSEs partsEs
@@ -48,68 +50,68 @@
qed "NS3_msg_in_parts_sees_Enemy";
-(*** Server keys are not betrayed ***)
+(*** Shared keys are not betrayed ***)
-(*Enemy never sees another agent's server key!*)
+(*Enemy never sees another agent's shared key!*)
goal thy
"!!evs. [| evs : ns_shared; A ~= Enemy |] ==> \
-\ Key (serverKey A) ~: parts (sees Enemy evs)";
+\ Key (shrK A) ~: parts (sees Enemy evs)";
be ns_shared.induct 1;
bd NS3_msg_in_parts_sees_Enemy 5;
by (Auto_tac());
(*Deals with Fake message*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs synth_analz_parts_insert_subset_Un]) 1);
-qed "Enemy_not_see_serverKey";
+ impOfSubs Fake_parts_insert]) 1);
+qed "Enemy_not_see_shrK";
-bind_thm ("Enemy_not_analz_serverKey",
- [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
+bind_thm ("Enemy_not_analz_shrK",
+ [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
-Addsimps [Enemy_not_see_serverKey,
- not_sym RSN (2, Enemy_not_see_serverKey),
- Enemy_not_analz_serverKey,
- not_sym RSN (2, Enemy_not_analz_serverKey)];
+Addsimps [Enemy_not_see_shrK,
+ not_sym RSN (2, Enemy_not_see_shrK),
+ Enemy_not_analz_shrK,
+ not_sym RSN (2, Enemy_not_analz_shrK)];
(*We go to some trouble to preserve R in the 3rd subgoal*)
val major::prems =
-goal thy "[| Key (serverKey A) : parts (sees Enemy evs); \
+goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
\ evs : ns_shared; \
\ A=Enemy ==> R \
\ |] ==> R";
br ccontr 1;
-br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1;
+br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
by (swap_res_tac prems 2);
by (ALLGOALS (fast_tac (!claset addIs prems)));
-qed "Enemy_see_serverKey_E";
+qed "Enemy_see_shrK_E";
-bind_thm ("Enemy_analz_serverKey_E",
- analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
+bind_thm ("Enemy_analz_shrK_E",
+ analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
-AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
+AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
-(*No Friend will ever see another agent's server key
+(*No Friend will ever see another agent's shared key
(excluding the Enemy, who might transmit his).
- The Server, of course, knows all server keys.*)
+ The Server, of course, knows all shared keys.*)
goal thy
"!!evs. [| evs : ns_shared; A ~= Enemy; A ~= Friend j |] ==> \
-\ Key (serverKey A) ~: parts (sees (Friend j) evs)";
+\ 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_serverKey";
+qed "Friend_not_see_shrK";
(*Not for Addsimps -- it can cause goals to blow up!*)
goal thy
"!!evs. evs : ns_shared ==> \
-\ (Key (serverKey A) \
-\ : analz (insert (Key (serverKey B)) (sees Enemy evs))) = \
+\ (Key (shrK A) \
+\ : analz (insert (Key (shrK B)) (sees Enemy evs))) = \
\ (A=B | A=Enemy)";
by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
addIs [impOfSubs (subset_insertI RS analz_mono)]
addss (!simpset)) 1);
-qed "serverKey_mem_analz";
+qed "shrK_mem_analz";
(*** Future keys can't be seen or used! ***)
@@ -200,8 +202,8 @@
\ evs : ns_shared \
\ |] ==> (EX evt:ns_shared. \
\ K = Key(newK evt) & \
-\ X = (Crypt {|K, Agent A|} (serverKey B)) & \
-\ K' = serverKey A & \
+\ X = (Crypt {|K, Agent A|} (shrK B)) & \
+\ K' = shrK A & \
\ length evt < length evs)";
be rev_mp 1;
be ns_shared.induct 1;
@@ -209,14 +211,15 @@
qed "Says_Server_message_form";
-(*Describes the form of X when the following message is sent*)
+(*Describes the form of X when the following message is sent. The use of
+ "parts" strengthens the induction hyp for proving the Fake case*)
goal thy
"!!evs. evs : ns_shared ==> \
\ ALL A NA B K X. \
-\ (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
+\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
\ : parts (sees Enemy evs) & A ~= Enemy --> \
\ (EX evt:ns_shared. K = newK evt & \
-\ X = (Crypt {|Key K, Agent A|} (serverKey B)))";
+\ 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);
@@ -225,7 +228,7 @@
by (fast_tac (!claset addSDs [spec]) 2);
(*Now for the Fake case*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs synth_analz_parts_insert_subset_Un]
+ impOfSubs Fake_parts_insert]
addss (!simpset)) 1);
qed_spec_mp "encrypted_form";
@@ -234,7 +237,7 @@
goal thy
"!!evs. evs : ns_shared ==> \
\ ALL S A NA B K X. \
-\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
+\ 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;
@@ -247,7 +250,7 @@
bd 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);
+by (thin_tac "ALL x. ?P(x)" 1);
bd encrypted_form 1;
br (parts.Inj RS conjI) 1;
auto();
@@ -257,11 +260,11 @@
(*Describes the form of X when the following message is sent;
use Says_Server_message_form if applicable*)
goal thy
- "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
-\ : set_of_list evs; \
-\ evs : ns_shared \
-\ |] ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
-\ X = (Crypt {|Key K, Agent A|} (serverKey B)))";
+ "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
+\ : 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);
@@ -277,8 +280,8 @@
The following is to prove theorems of the form
Key K : analz (insert (Key (newK evt))
- (insert (Key (serverKey C)) (sees Enemy evs))) ==>
- Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
+ (insert (Key (shrK C)) (sees Enemy evs))) ==>
+ Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
A more general formula must be proved inductively.
@@ -323,52 +326,56 @@
(** 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 (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))";
+by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+val lemma = result();
+
goal thy
"!!evs. evs : ns_shared ==> \
-\ ALL K E. (Key K : analz (insert (Key (serverKey C)) \
+\ 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 (serverKey C)) \
+\ Key K : analz (insert (Key (shrK C)) \
\ (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_FIRST (resolve_tac [allI, lemma]));
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
setloop split_tac [expand_if])));
+(** LEVEL 5 **)
(*Cases NS2 and NS3!! Simple, thanks to auto case splits*)
by (REPEAT (Fast_tac 3));
+(*Fake case*) (** LEVEL 6 **)
+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]);
(*Base case*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
-(** LEVEL 7 **)
-(*Fake case*)
-by (REPEAT (Safe_step_tac 1));
-by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2);
-by (subgoal_tac
- "Key K : analz \
-\ (synth \
-\ (analz (insert (Key (serverKey C)) \
-\ (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
-(*First, justify this subgoal*)
-(*Discard formulae 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 (analz_mono RS synth_mono)]
- addSEs [impOfSubs analz_mono]) 2);
-by (Asm_full_simp_tac 1);
-by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1);
qed_spec_mp "analz_image_newK";
goal thy
"!!evs. evs : ns_shared ==> \
\ Key K : analz (insert (Key (newK evt)) \
-\ (insert (Key (serverKey C)) \
+\ (insert (Key (shrK C)) \
\ (sees Enemy evs))) = \
\ (K = newK evt | \
-\ Key K : analz (insert (Key (serverKey C)) \
+\ Key K : analz (insert (Key (shrK C)) \
\ (sees Enemy evs)))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
@@ -384,8 +391,7 @@
\ 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|} (serverKey C)) : parts{Y} --> \
-\ (X = 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
@@ -407,13 +413,13 @@
ba 2;
by (Step_tac 1);
(** LEVEL 12 **)
-by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
+by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \
\ : parts (sees Enemy evsa)" 1);
-by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
+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 (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
+by (thin_tac "?aa : parts {X}" 1);
bd parts_singleton 1;
by (Step_tac 1);
bd seesD 1;
@@ -426,10 +432,10 @@
(*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)) \
+\ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \
\ : set_of_list evs; \
\ Says S' A' \
-\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \
+\ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
\ : set_of_list evs; \
\ evs : ns_shared; C ~= Enemy; C' ~= Enemy |] ==> X = X'";
bd lemma 1;
@@ -447,9 +453,10 @@
\ (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 (serverKey C)) (sees Enemy evs))";
+\ K ~: analz (insert (Key (shrK C)) (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)));
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
@@ -467,7 +474,7 @@
br notI 1;
by (subgoal_tac
"Key (newK evt) : \
-\ analz (synth (analz (insert (Key (serverKey C)) \
+\ 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),
@@ -489,7 +496,7 @@
by (REPEAT_FIRST assume_tac);
by (ALLGOALS Full_simp_tac);
by (Step_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
+by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1);
qed "Enemy_not_see_encrypted_key";