--- 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";
--- a/src/HOL/Auth/NS_Shared.thy Tue Sep 03 17:54:39 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Tue Sep 03 18:24:42 1996 +0200
@@ -22,46 +22,49 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: ns_shared; B ~= Enemy; X: synth (analz (sees Enemy evs))
- |] ==> (Says Enemy B X) # evs : ns_shared"
+ |] ==> Says Enemy B X # evs : ns_shared"
(*Alice initiates a protocol run*)
NS1 "[| evs: ns_shared; A ~= Server
- |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|})
- # evs : ns_shared"
+ |] ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
+ : ns_shared"
(*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; A ~= B; A ~= Server;
- (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
- |] ==> (Says Server A
+ Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs
+ |] ==> Says Server A
(Crypt {|Nonce NA, Agent B, Key (newK evs),
- (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
- (serverKey A))) # evs : ns_shared"
+ (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
+ (shrK A)) # evs : ns_shared"
(*We can't assume S=Server. Agent A "remembers" her nonce.
May assume WLOG that she is NOT the Enemy: the Fake rule
covers this case. Can inductively show A ~= Server*)
NS3 "[| evs: ns_shared; A ~= B;
- (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;
A = Friend i;
- (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
- |] ==> (Says A B X) # evs : ns_shared"
+ Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs
+ |] ==> Says A B X # evs : ns_shared"
(*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; A ~= B;
- (Says A' B (Crypt {|Key K, Agent A|} (serverKey B)))
- : set_of_list evs
- |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : ns_shared"
+ Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs
+ |] ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
- (*Alice responds with (Suc N), if she has seen the key before.*)
+ (*Alice responds with the Nonce, if she has seen the key before.
+ We do NOT use N-1 or similar as the Enemy cannot spoof such things.
+ Allowing the Enemy to add or subtract 1 allows him to send ALL
+ nonces. Instead we distinguish the messages by sending the
+ nonce twice.*)
NS5 "[| evs: ns_shared; A ~= B;
- (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
- (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)))
+ Says B' A (Crypt (Nonce N) K) : set_of_list evs;
+ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
: set_of_list evs
- |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : ns_shared"
+ |] ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
end
--- a/src/HOL/Auth/Shared.ML Tue Sep 03 17:54:39 1996 +0200
+++ b/src/HOL/Auth/Shared.ML Tue Sep 03 18:24:42 1996 +0200
@@ -12,13 +12,6 @@
Addsimps [parts_cut_eq];
-proof_timing:=true;
-
-(*IN SET.ML*)
-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";
-
(*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);
@@ -34,37 +27,37 @@
will not!*)
Addsimps [o_def];
-(*** Basic properties of serverKey and newK ***)
+(*** Basic properties of shrK and newK ***)
-(* invKey (serverKey A) = serverKey A *)
-bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
+(* invKey (shrK A) = shrK A *)
+bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
(* invKey (newK evs) = newK evs *)
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
-Addsimps [invKey_serverKey, invKey_newK];
+Addsimps [invKey_shrK, invKey_newK];
(*New keys and nonces are fresh*)
-val serverKey_inject = inj_serverKey RS injD;
+val shrK_inject = inj_shrK RS injD;
val newN_inject = inj_newN RS injD
and newK_inject = inj_newK RS injD;
-AddSEs [serverKey_inject, newN_inject, newK_inject,
+AddSEs [shrK_inject, newN_inject, newK_inject,
fresh_newK RS notE, fresh_newN RS notE];
-Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
+Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
Addsimps [fresh_newN, fresh_newK];
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
-goal thy "newK evs ~= serverKey B";
-by (subgoal_tac "newK evs = serverKey B --> \
+goal thy "newK evs ~= shrK B";
+by (subgoal_tac "newK evs = shrK B --> \
\ Key (newK evs) : parts (initState B)" 1);
by (Fast_tac 1);
by (agent.induct_tac "B" 1);
by (auto_tac (!claset addIs [range_eqI], !simpset));
-qed "newK_neq_serverKey";
+qed "newK_neq_shrK";
-Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
+Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
(*Good for talking about Server's initial state*)
goal thy "!!H. H <= Key``E ==> parts H = H";
@@ -96,25 +89,25 @@
qed "keysFor_image_Key";
Addsimps [keysFor_image_Key];
-goal thy "serverKey A ~: newK``E";
+goal thy "shrK A ~: newK``E";
by (agent.induct_tac "A" 1);
by (Auto_tac ());
-qed "serverKey_notin_image_newK";
-Addsimps [serverKey_notin_image_newK];
+qed "shrK_notin_image_newK";
+Addsimps [shrK_notin_image_newK];
-(*Agents see their own serverKeys!*)
-goal thy "Key (serverKey A) : analz (sees A evs)";
+(*Agents see their own shrKs!*)
+goal thy "Key (shrK A) : analz (sees A evs)";
by (list.induct_tac "evs" 1);
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 "analz_own_serverKey";
+qed "analz_own_shrK";
-bind_thm ("parts_own_serverKey",
- [analz_subset_parts, analz_own_serverKey] MRS subsetD);
+bind_thm ("parts_own_shrK",
+ [analz_subset_parts, analz_own_shrK] MRS subsetD);
-Addsimps [analz_own_serverKey, parts_own_serverKey];
+Addsimps [analz_own_shrK, parts_own_shrK];
@@ -143,6 +136,11 @@
by (Fast_tac 1);
qed "sees_Says_subset_insert";
+goal thy "sees A (Notes A' X # evs) <= insert X (sees A evs)";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (Fast_tac 1);
+qed "sees_Notes_subset_insert";
+
goal thy "sees A evs <= sees A (Says A' B X # evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
@@ -166,7 +164,7 @@
Addsimps [Says_imp_sees_Enemy];
AddIs [Says_imp_sees_Enemy];
-goal thy "initState C <= Key `` range serverKey";
+goal thy "initState C <= Key `` range shrK";
by (agent.induct_tac "C" 1);
by (Auto_tac ());
qed "initState_subset";
@@ -174,7 +172,7 @@
goal thy "X : sees C 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))";
+\ (EX A. X = Key (shrK A))";
by (list.induct_tac "evs" 1);
by (ALLGOALS Asm_simp_tac);
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
@@ -211,6 +209,6 @@
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
val pushes = pushKeys@pushCrypts;
-val pushKey_newK = insComm "Key (newK ?evs)" "Key (serverKey ?C)";
+val pushKey_newK = insComm "Key (newK ?evs)" "Key (shrK ?C)";
--- a/src/HOL/Auth/Shared.thy Tue Sep 03 17:54:39 1996 +0200
+++ b/src/HOL/Auth/Shared.thy Tue Sep 03 18:24:42 1996 +0200
@@ -6,24 +6,26 @@
Theory of Shared Keys (common to all symmetric-key protocols)
Server keys; initial states of agents; new nonces and keys; function "sees"
+
+IS THE Notes constructor needed??
*)
Shared = Message + List +
consts
- serverKey :: agent => key (*symmetric keys*)
+ shrK :: agent => key (*symmetric keys*)
rules
- isSym_serverKey "isSymKey (serverKey A)"
+ isSym_shrK "isSymKey (shrK A)"
consts (*Initial states of agents -- parameter of the construction*)
initState :: agent => msg set
primrec initState agent
(*Server knows all keys; other agents know only their own*)
- initState_Server "initState Server = Key `` range serverKey"
- initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}"
- initState_Enemy "initState Enemy = {Key (serverKey Enemy)}"
+ initState_Server "initState Server = Key `` range shrK"
+ initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
+ initState_Enemy "initState Enemy = {Key (shrK Enemy)}"
datatype (*Messages, and components of agent stores*)
event = Says agent agent msg
@@ -55,7 +57,7 @@
newK :: "event list => key"
rules
- inj_serverKey "inj serverKey"
+ inj_shrK "inj shrK"
inj_newN "inj newN"
fresh_newN "Nonce (newN evs) ~: parts (initState B)"