--- a/src/HOL/Auth/Event.ML Thu Jul 11 15:28:10 1996 +0200
+++ b/src/HOL/Auth/Event.ML Thu Jul 11 15:30:22 1996 +0200
@@ -5,31 +5,39 @@
Datatype of events;
inductive relation "traces" for Needham-Schroeder (shared keys)
+
+Rewrites should not refer to initState (Friend i) -- not in normal form
*)
open Event;
+(*Rewrite using {a} Un A = insert a A *)
+Addsimps [insert_is_Un RS sym];
+
+
+(*** Basic properties of serverKey and newK ***)
+
(* invKey (serverKey A) = serverKey A *)
bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
-(* invKey (newK(A,evs)) = newK(A,evs) *)
+(* invKey (newK evs) = newK evs *)
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
Addsimps [invKey_serverKey, invKey_newK];
(*New keys and nonces are fresh*)
val serverKey_inject = inj_serverKey RS injD;
-val newN_inject = inj_newN RS injD RS Pair_inject
-and newK_inject = inj_newK RS injD RS Pair_inject;
+val newN_inject = inj_newN RS injD
+and newK_inject = inj_newK RS injD;
AddSEs [serverKey_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 [fresh_newN, fresh_newK];
-goal thy "newK (A,evs) ~= serverKey B";
-by (subgoal_tac "newK (A,evs) = serverKey B --> \
-\ Key (newK(A,evs)) : parts (initState B)" 1);
+goal thy "newK evs ~= serverKey B";
+by (subgoal_tac "newK evs = serverKey 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));
@@ -79,7 +87,6 @@
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
by (Simp_tac 1);
-by (Fast_tac 1);
qed "sees_own";
goal thy "!!A. Server ~= A ==> \
@@ -94,13 +101,17 @@
goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
by (Simp_tac 1);
-by (Fast_tac 1);
qed "sees_Enemy";
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
-qed "sees_subset";
+qed "sees_Says_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);
+qed "sees_subset_sees_Says";
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
@@ -114,7 +125,7 @@
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
-Delsimps [sees_Cons];
+Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
(**** Inductive proofs about traces ****)
@@ -124,47 +135,50 @@
"!!evs. evs : traces ==> \
\ sees A evs <= initState A Un sees Enemy evs";
be traces.induct 1;
-be subst 4; (*simply DISCARD evsa = Says A Server... as irrelevant!*)
-by (ALLGOALS (fast_tac (!claset addDs [sees_subset RS subsetD]
+be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*)
+be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*)
+by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]
addss (!simpset))));
qed "sees_agent_subset_sees_Enemy";
+goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList 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)];
+
+
(*** Server keys are not betrayed ***)
-(*No Enemy will ever see a Friend's server key
- -- even if another friend's key is compromised.
- The UN is essential to handle the Fake rule in the induction.*)
+(*Enemy never sees another agent's server key!*)
goal thy
- "!!evs. [| evs : traces; i~=j |] ==> \
-\ Key (serverKey (Friend i)) ~: \
-\ parts (initState (Friend j) Un sees Enemy evs)";
+ "!!evs. [| evs : traces; A ~= Enemy |] ==> \
+\ Key (serverKey A) ~: parts (sees Enemy evs)";
be traces.induct 1;
-be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
-by (Auto_tac());
+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 [imp_of_subset analyze_subset_parts,
- imp_of_subset parts_insert_subset_Un]
+by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
+ impOfSubs parts_insert_subset_Un]
addss (!simpset)) 1);
qed "Enemy_not_see_serverKey";
-(*No Friend will ever see another Friend's server key.*)
-goal thy
- "!!evs. [| evs : traces; i~=j |] ==> \
-\ Key (serverKey (Friend i)) ~: parts (sees (Friend j) evs)";
-br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
-by (REPEAT (ares_tac [Enemy_not_see_serverKey] 1));
-qed "Friend_not_see_serverKey";
+bind_thm ("Enemy_not_analyze_serverKey",
+ [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
+
+Addsimps [Enemy_not_see_serverKey, Enemy_not_analyze_serverKey];
+
-(*Variant needed for the theorem below*)
+(*No Friend will ever see another agent's server key
+ (excluding the Enemy, who might transmit his).*)
goal thy
- "!!evs. evs : traces ==> \
-\ Key (serverKey (Friend i)) ~: analyze (sees Enemy evs)";
-bd Enemy_not_see_serverKey 1;
-br n_not_Suc_n 1;
-by (Full_simp_tac 1);
-by (fast_tac (!claset addDs [imp_of_subset analyze_subset_parts]) 1);
-qed "serverKeys_not_analyzed";
+ "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \
+\ Key (serverKey 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";
(*** Future keys can't be seen or used! ***)
@@ -177,9 +191,9 @@
induction! *)
goal thy "!!evs. evs : traces ==> \
\ length evs <= length evs' --> \
-\ Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
+\ Key (newK evs') ~: (UN C. parts (sees C evs))";
be traces.induct 1;
-be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
by (ALLGOALS (asm_full_simp_tac
(!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
(*Initial state? New keys cannot clash*)
@@ -188,9 +202,11 @@
by (fast_tac (!claset addDs [less_imp_le]) 2);
(*Rule NS2 in protocol*)
by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
+(*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 [imp_of_subset analyze_subset_parts,
- imp_of_subset parts_insert_subset_Un,
+by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
+ impOfSubs parts_insert_subset_Un,
less_imp_le]
addss (!simpset)) 1);
val lemma = result();
@@ -198,22 +214,25 @@
(*Variant needed for the main theorem below*)
goal thy
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \
-\ Key (newK (A,evs')) ~: parts (sees C evs)";
+\ Key (newK evs') ~: parts (sees C evs)";
by (fast_tac (!claset addDs [lemma]) 1);
qed "new_keys_not_seen";
-goal thy "!!K. newK(A,evs) = invKey K ==> newK(A,evs) = K";
+goal thy "!!K. newK evs = invKey K ==> newK evs = K";
br (invKey_eq RS iffD1) 1;
by (Simp_tac 1);
val newK_invKey = result();
+
+val keysFor_parts_mono = parts_mono RS keysFor_mono;
+
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
goal thy "!!evs. evs : traces ==> \
\ length evs <= length evs' --> \
-\ newK (A,evs') ~: keysFor (UN C. parts (sees C evs))";
+\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
be traces.induct 1;
-be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
by (ALLGOALS (asm_full_simp_tac
(!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
(*Rule NS1 in protocol*)
@@ -223,24 +242,52 @@
(*Rule Fake: where an Enemy agent can say practically anything*)
by (best_tac
(!claset addSDs [newK_invKey]
- addDs [imp_of_subset (analyze_subset_parts RS keysFor_mono),
- imp_of_subset (parts_insert_subset_Un RS keysFor_mono),
+ addDs [impOfSubs (analyze_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)]
addss (!simpset)) 1);
+(*Rule NS3: quite messy...*)
+by (hyp_subst_tac 1);
+by (full_simp_tac (!simpset addcongs [conj_cong]) 1);
+br impI 1;
+bd mp 1;
+by (fast_tac (!claset addDs [less_imp_le]) 1);
+by (best_tac (!claset addIs
+ [impOfSubs (sees_subset_sees_Says RS keysFor_parts_mono),
+ impOfSubs (sees_own RS equalityD2 RS keysFor_parts_mono),
+ impOfSubs (empty_subsetI RS insert_mono RS keysFor_parts_mono)]
+ addss (!simpset)) 1);
val lemma = result();
goal thy
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \
-\ newK (A,evs') ~: keysFor (parts (sees C evs))";
+\ newK evs' ~: keysFor (parts (sees C evs))";
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
qed "new_keys_not_used";
+Addsimps [new_keys_not_used];
-bind_thm ("new_keys_not_used_analyze",
+bind_thm ("new_keys_not_analyzed",
[analyze_subset_parts RS keysFor_mono,
new_keys_not_used] MRS contra_subsetD);
+(*Maybe too specific to be of much use...*)
+goal thy
+ "!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \
+\ (serverKey A)) \
+\ : setOfList evs; \
+\ evs : traces \
+\ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
+be rev_mp 1;
+be traces.induct 1;
+be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
+be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*)
+by (ALLGOALS Asm_full_simp_tac);
+by (Fast_tac 1); (*Proves the NS2 case*)
+qed "Says_Server_imp_X_eq_Crypt";
+
+
(*Pushes Crypt events in so that others might be pulled out*)
goal thy "insert (Crypt X K) (insert y evs) = \
\ insert y (insert (Crypt X K) evs)";
@@ -252,157 +299,336 @@
by (Fast_tac 1);
qed "insert_Key_delay";
+
(** Lemmas concerning the form of items passed in messages **)
(*Describes the form *and age* of K when the following message is sent*)
goal thy
- "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
+ "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') \
\ : setOfList evs; \
\ evs : traces \
-\ |] ==> (EX evs'. K = Key (newK(Server,evs')) & \
-\ length evs' < length evs)";
+\ |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)";
be rev_mp 1;
be traces.induct 1;
-be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
qed "Says_Server_imp_Key_newK";
-Addsimps [serverKeys_not_analyzed,
- new_keys_not_seen RS not_parts_not_analyze,
- new_keys_not_used_analyze];
+(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *)
+bind_thm ("not_parts_not_keysFor_analyze",
+ analyze_subset_parts RS keysFor_mono RS contra_subsetD);
+
+
+XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
+ZZZZZZZZZZZZZZZZ;
+
+
+(*Fake case below may need something like this...*)
+goal thy
+ "!!evs. evs : traces ==> \
+\ ALL B X. Crypt X (serverKey B) : analyze (sees Enemy evs) --> \
+\ (EX A A'. Says A A' (Crypt X (serverKey B)) : setOfList evs";
goal thy
- "!!evs. evs : traces ==> \
-\ Says Server (Friend i) \
-\ (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs \
-\ --> K ~: analyze (sees Enemy evs)";
+ "!!evs. evs : traces ==> \
+\ ALL NA B K X. Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B) :
+ analyze (sees Enemy evs) --> \
+\ (EX A A'. Says A A' (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B)) : setOfList evs";
+
+
+
+(*Describes the form of X when the following message is sent*)
+goal thy
+ "!!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 --> \
+\ (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
be traces.induct 1;
-be subst 4; (*simply DISCARD evsa = Says A Server... as irrelevant!*)
+be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
+by (Step_tac 1);
+by (ALLGOALS Asm_full_simp_tac);
+(*Remaining cases are Fake, NS2 and NS3*)
+by (Fast_tac 2); (*Solves the NS2 case*)
+(*The NS3 case needs the induction hypothesis twice!
+ One application is to the X component of the most recent message.*)
+by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
+be conjE 2;
+by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent (Friend i)|} (serverKey B)" 2);
+by (eres_inst_tac [("V","?P|?Q")] thin_rl 3); (*speeds the following step*)
+by (Fast_tac 3);
+(*DELETE the first quantified formula: it's now useless*)
+by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
+by (fast_tac (!claset addss (!simpset)) 2);
+(*Now for the Fake case*)
+be disjE 1;
+(*The subcase of Fake, where the message in question is NOT the most recent*)
+by (Best_tac 2);
+(*The subcase of Fake proved because server keys are kept secret*)
+by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
+be Crypt_synthesize 1;
+be Key_synthesize 2;
+by (Asm_full_simp_tac 2);
+
+
+
+ 1. !!evs B X evsa S A NA Ba K Xa.
+ [| evsa : traces;
+ ! S A NA B K X.
+ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) :
+ setOfList evsa -->
+ (? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B));
+ B ~= Enemy;
+ Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey B) :
+ analyze (sees Enemy evsa) |] ==>
+ ? evs'. Xa = Crypt {|Key (newK evs'), Agent B|} (serverKey Ba)
+
+
+(*Split up the possibilities of that message being synthesized...*)
+by (Step_tac 1);
+by (Best_tac 6);
+
+
+
+
+by (Safe_step_tac 1);
+by (Safe_step_tac 2);
by (ALLGOALS Asm_full_simp_tac);
-(*We infer that K has the form "Key (newK(Server,evs')" ... *)
+by (REPEAT_FIRST (etac disjE));
+by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
+
+
+by (hyp_subst_tac 5);
+
+
+
+
+
+by (REPEAT (dtac spec 3));
+fe conjE;
+fe mp ;
+by (REPEAT (resolve_tac [refl, conjI] 3));
+by (REPEAT_FIRST (etac conjE));
+by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
+
+
+by (subgoal_tac "? evs'. Xa = Crypt {|Key (newK evs'), Agent Aa|} (serverKey Ba)" 2);
+by (Fast_tac 3);
+
+
+
+be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*)
+
+
+auto();
+by (ALLGOALS
+ (asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,de_Morgan_conj])));
+by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
+
+by (REPEAT (Safe_step_tac 1));
+
+qed "Says_Crypt_Nonce_imp_msg_Crypt";
+
+goal thy
+ "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
+\ : setOfList evs; \
+\ evs : traces \
+\ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
+
+
+YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
+
+
+WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
+
+(*If a message is sent, encrypted with a Friend's server key, then either
+ that Friend or the Server originally sent it.*)
+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)";
+be traces.induct 1;
+be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
+by (Step_tac 1);
+by (ALLGOALS Asm_full_simp_tac);
+(*Remaining cases are Fake, NS2 and NS3*)
+by (Fast_tac 2); (*Proves the NS2 case*)
+
+by (REPEAT (dtac spec 2));
+fe conjE;
+bd mp 2;
+
+by (REPEAT (resolve_tac [refl, conjI] 2));
+by (ALLGOALS Asm_full_simp_tac);
+
+
+
+
+by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
+be conjE 2;
+by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
+
+(*The NS3 case needs the induction hypothesis twice!
+ One application is to the X component of the most recent message.*)
+by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2);
+by (Fast_tac 3);
+by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
+be conjE 2;
+(*DELETE the first quantified formula: it's now useless*)
+by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
+by (fast_tac (!claset addss (!simpset)) 2);
+(*Now for the Fake case*)
+be disjE 1;
+(*The subcase of Fake, where the message in question is NOT the most recent*)
+by (Best_tac 2);
+
+by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
+be Crypt_synthesize 1;
+be Key_synthesize 2;
+
+(*Split up the possibilities of that message being synthesized...*)
+by (Step_tac 1);
+by (Best_tac 6);
+
+
+
+
+
+ (*The NS3 case needs the induction hypothesis twice!
+ One application is to the X component of the most recent message.*)
+
+????????????????????????????????????????????????????????????????
+by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 1);
+by (Fast_tac 2);
+
+by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
+
+be conjE 1;
+(*DELETE the first quantified formula: it's now useless*)
+by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 1);
+by (fast_tac (!claset addss (!simpset)) 1);
+
+
+(*Now for the Fake case*)
+be disjE 1;
+(*The subcase of Fake, where the message in question is NOT the most recent*)
+by (Best_tac 2);
+
+WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
+
+
+Addsimps [new_keys_not_seen];
+
+(*Crucial security property: Enemy does not see the keys sent in msg NS2
+ -- even if another friend's key is compromised*)
+goal thy
+ "!!evs. [| Says Server (Friend i) \
+\ (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \
+\ evs : traces; i~=j |] ==> \
+\ \
+\ K ~: analyze (insert (Key (serverKey (Friend j))) (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);
+(*The two simplifications cannot be combined -- they loop!*)
+by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
+(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
br conjI 3;
by (REPEAT_FIRST (resolve_tac [impI]));
by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
(*NS1, subgoal concerns "(Says A Server
- {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
+ {|Agent A, Agent B, Nonce (newN evsa)|}"*)
(*... thus it cannot equal any components of A's message above.*)
by (fast_tac (!claset addss (!simpset)) 2);
(*NS2, the subcase where that message was the most recently sent;
- it holds because here K' = serverKey(Friend i), which Enemies can't see*)
-by (fast_tac (!claset addss (!simpset)) 2);
-(*NS2, other subcase!*)
+ it holds because here K' = serverKey(Friend i), which Enemies can't see,
+ AND because nobody can know about a brand new key*)
+by (fast_tac (!claset addss (!simpset addsimps [not_parts_not_analyze])) 2);
+(*NS2, other subcase. K is an old key, and thus not in the latest message.*)
by (fast_tac
(!claset addSEs [less_irrefl]
- addDs [imp_of_subset analyze_insert_Crypt_subset]
- addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
+ addDs [impOfSubs analyze_insert_Crypt_subset]
+ addss (!simpset addsimps [not_parts_not_keysFor_analyze])) 2);
(*Now for the Fake case*)
be exE 1;
br notI 1;
by (REPEAT (etac conjE 1));
by (REPEAT (hyp_subst_tac 1));
-by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
-be (imp_of_subset analyze_mono) 2;
+by (subgoal_tac
+ "Key (newK evs') : \
+\ analyze (synthesize (analyze (insert (Key (serverKey (Friend j))) \
+\ (sees Enemy evsa))))" 1);
+be (impOfSubs analyze_mono) 2;
by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN
(2,rev_subsetD),
- imp_of_subset synthesize_increasing,
- imp_of_subset analyze_increasing]) 2);
+ impOfSubs synthesize_increasing,
+ impOfSubs analyze_increasing]) 2);
(*Proves the Fake goal*)
by (Auto_tac());
-qed "encrypted_key_not_seen";
+qed "Enemy_not_see_encrypted_key";
+
+
+goal thy
+ "!!evs. [| Says Server (Friend i) \
+\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
+\ evs : traces; i~=j \
+\ |] ==> K ~: analyze (sees (Friend j) evs)";
+br (sees_agent_subset_sees_Enemy RS analyze_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; \
+\ A ~: {Friend i, Server}; \
+\ evs : traces \
+\ |] ==> K ~: analyze (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;
+(* hyp_subst_tac would deletes the equality assumption... *)
+by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
+qed "Agent_not_see_encrypted_key";
+
+
+(*Neatly packaged, perhaps in a useless form*)
+goalw thy [knownBy_def]
+ "!!evs. [| Says Server (Friend i) \
+\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
+\ evs : traces \
+\ |] ==> knownBy evs K <= {Friend i, Server}";
+
+by (Step_tac 1);
+br ccontr 1;
+by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
+qed "knownBy_encrypted_key";
+
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The length comparison, and Union over C, are essential for the
- induction! *)
-goal thy "!!evs. evs : traces ==> \
-\ length evs <= length evs' --> \
-\ Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
-be traces.induct 1;
-be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
-by (ALLGOALS (asm_full_simp_tac
- (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
-(*Initial state? New keys cannot clash*)
-by (Fast_tac 1);
-(*Rule NS1 in protocol*)
-by (fast_tac (!claset addDs [less_imp_le]) 2);
-(*Rule NS2 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 [imp_of_subset analyze_subset_parts,
- imp_of_subset parts_insert_subset_Un,
- less_imp_le]
- addss (!simpset)) 1);
-val lemma = result();
+
goal thy
- "!!evs. [| evs : traces; i~=j |] ==> \
-\ Says Server (Friend i) \
-\ (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs \
-\ --> K ~: analyze (initState (Friend j) Un sees Enemy evs)";
+ "!!evs. evs : traces ==> \
+\ Says Server A \
+\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \
+\ --> (EX evs'. N = Nonce (newN evs'))";
be traces.induct 1;
-be subst 4; (*simply DISCARD evsa = Says A Server... as irrelevant!*)
-by (ALLGOALS Asm_full_simp_tac);
-(*We infer that K has the form "Key (newK(Server,evs')" ... *)
-br conjI 3;
-by (REPEAT_FIRST (resolve_tac [impI]));
-by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
-(*NS1, subgoal concerns "(Says A Server
- {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
-(*... thus it cannot equal any components of A's message above.*)
-
-by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
-
-by (fast_tac (!claset addss (!simpset)) 2);
-(*NS2, the subcase where that message was the most recently sent;
- it holds because here K' = serverKey(Friend i), which Enemies can't see*)
-by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
-by (Safe_step_tac 2);
-
-by (stac analyze_insert_Crypt 2);
-
-by (fast_tac (!claset addss (!simpset)) 2);
-(*NS2, other subcase!*)
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
+val Says_Server_lemma = result();
-by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
-by (fast_tac
- (!claset addSEs [less_irrefl]
- addDs [imp_of_subset analyze_insert_Crypt_subset]
- addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
-(*Now for the Fake case*)
-be exE 1;
-br notI 1;
-by (REPEAT (etac conjE 1));
-by (REPEAT (hyp_subst_tac 1));
-by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
-be (imp_of_subset analyze_mono) 2;
-by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN
- (2,rev_subsetD),
- imp_of_subset synthesize_increasing,
- imp_of_subset analyze_increasing]) 2);
-(*Proves the Fake goal*)
-by (Auto_tac());
-qed "encrypted_key_not_seen";
-
-
-
-
-(*Bet this requires the premise A = Friend i *)
-goal thy "[| evs : traces; \
-\ (Says Server A (Crypt {|Agent A, Agent B, K, N|} K')) \
-\ : setOfList evs \
-\ |] ==> knownBy evs K <= {A,Server}";
-
-
-XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
(*NEEDED??*)
@@ -419,20 +645,11 @@
by (asm_simp_tac (!simpset addsimps [parts_Un]) 1);
qed "in_parts_sees_Says";
-goal thy "!!evs. length evs < length evs' ==> newK (A,evs) ~= newK (A',evs')";
+goal thy "!!evs. length evs < length evs' ==> newK evs ~= newK (A',evs')";
by (fast_tac (!claset addSEs [less_irrefl]) 1);
qed "length_less_newK_neq";
-(*Initially
-goal thy "knownBy [] X = \
-\ {A. X = Key (invKey (serverKey A)) | (? i. X = Key (serverKey i))}";
-by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
-qed "knownBy_Nil";
-
-goal thy "!!X. knownBy (x#l) X = ?F(knownBy l X)";
-by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
-********************)
goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \
\ insert {|X,Y|} (insert (Crypt x) evs)";
@@ -441,39 +658,6 @@
-WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
-
-goal thy
- "!!evs. evs : traces ==> \
-\ Says Server A \
-\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \
-\ --> (EX evs'. K = Key (newK(Server,evs')))";
-be traces.induct 1;
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-val Says_Server_lemma = result();
-
-goal thy
- "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
-\ : setOfList evs; \
-\ evs : traces \
-\ |] ==> (EX evs'. K = Key (newK(Server,evs')))";
-bd Says_Server_lemma 1;
-by (Fast_tac 1);
-qed "Says_Server_imp_Key_newK";
-
-
-goal thy
- "!!evs. evs : traces ==> \
-\ Says Server A \
-\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \
-\ --> (EX evs'. N = Nonce (newN(A,evs')))";
-be traces.induct 1;
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-val Says_Server_lemma = result();
-
-
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
goalw thy [keysFor_def]
--- a/src/HOL/Auth/Event.thy Thu Jul 11 15:28:10 1996 +0200
+++ b/src/HOL/Auth/Event.thy Thu Jul 11 15:30:22 1996 +0200
@@ -6,6 +6,8 @@
Datatype of events;
inductive relation "traces" for Needham-Schroeder (shared keys)
+INTERLEAVING? See defn of "traces"
+
WHAT ABOUT ASYMMETRIC KEYS? NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
PUBLIC KEY...
*)
@@ -14,16 +16,16 @@
consts
publicKey :: agent => key
- serverKey :: agent => key (*symmetric keys*)
+ serverKey :: agent => key (*symmetric keys*)
rules
isSym_serverKey "isSymKey (serverKey A)"
-consts (*Initial states of agents -- parameter of the construction*)
+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*)
+ (*Server knows all keys; other agents know only their own*)
initState_Server "initState Server = range (Key o serverKey)"
initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}"
initState_Enemy "initState Enemy = {Key (serverKey Enemy)}"
@@ -51,7 +53,7 @@
sees :: [agent, event list] => msg set
primrec sees list
- (*Initial knowledge includes all public keys and own private key*)
+ (*Initial knowledge includes all public keys and own private key*)
sees_Nil "sees A [] = initState A"
sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
@@ -61,25 +63,29 @@
"knownBy evs X == {A. X: analyze (sees A evs)}"
-(*Agents generate "random" nonces. Different agents always generate
- different nonces. Different traces also yield different nonces. Same
- applies for keys.*)
-(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS. REMOVE AGENT ARGUMENT?
+(*Agents generate "random" nonces. Different traces always yield
+ different nonces. Same applies for keys.*)
+(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
consts
- newN :: "agent * event list => nat"
- newK :: "agent * event list => key"
+ newN :: "event list => nat"
+ newK :: "event list => key"
rules
inj_serverKey "inj serverKey"
inj_newN "inj(newN)"
- fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)"
+ fresh_newN "Nonce (newN evs) ~: parts (initState B)"
inj_newK "inj(newK)"
- fresh_newK "Key (newK(A,evs)) ~: parts (initState B)"
- isSym_newK "isSymKey (newK(A,evs))"
+ fresh_newK "Key (newK evs) ~: parts (initState B)"
+ isSym_newK "isSymKey (newK evs)"
+
+(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
+ MOST RECENT message. Does this mean we can't model middleperson attacks?
+ We don't need the most recent restriction in order to handle interception
+ by the Enemy, as agents are not forced to respond anyway.*)
consts traces :: "event list set"
inductive traces
@@ -88,17 +94,39 @@
(*The enemy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1.*)
- Fake "[| evs: traces; X: synthesize(analyze(sees Enemy evs))
+ Fake "[| evs: traces; B ~= Enemy;
+ X: synthesize(analyze(sees Enemy evs))
|] ==> (Says Enemy B X) # evs : traces"
NS1 "[| evs: traces; A ~= Server
- |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|})
+ |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|})
# evs : traces"
- NS2 "[| evs: traces;
+ (*We can't trust the sender field: change that A to A'? *)
+ NS2 "[| evs: traces; A ~= B;
evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
|] ==> (Says Server A
- (Crypt {|Agent A, Agent B,
- Key (newK(Server,evs)), Nonce NA|}
- (serverKey A))) # evs : traces"
+ (Crypt {|Nonce NA, Agent B, Key (newK evs),
+ (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
+ (serverKey A))) # evs : traces"
+
+ (*We can't assume S=Server. Agent A "remembers" her nonce.
+ May assume WLOG that she is NOT the Enemy, as the Fake rule.
+ covers this case. Can inductively show A ~= Server*)
+ NS3 "[| evs: traces; A ~= B;
+ evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
+ (serverKey A)))
+ # evs';
+ A = Friend i;
+ (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
+ |] ==> (Says A B X) # evs : traces"
+
+(*Initial version of NS2 had
+
+ {|Agent A, Agent B, Key (newK evs), Nonce NA|}
+
+ for the encrypted part; the version above is LESS transparent, hence
+ maybe HARDER to prove. Also it is precisely as in the BAN paper.
+*)
+
end
--- a/src/HOL/Auth/Message.ML Thu Jul 11 15:28:10 1996 +0200
+++ b/src/HOL/Auth/Message.ML Thu Jul 11 15:30:22 1996 +0200
@@ -22,7 +22,7 @@
fun auto() = by (Auto_tac());
-fun imp_of_subset th = th RSN (2, rev_subsetD);
+fun impOfSubs th = th RSN (2, rev_subsetD);
(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
@@ -141,6 +141,13 @@
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
qed "parts_Un";
+(*TWO inserts to avoid looping. This rewrite is better than nothing...*)
+goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
+by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
+by (stac (read_instantiate [("A","{Y} Un H")] insert_is_Un) 1);
+by (simp_tac (HOL_ss addsimps [parts_Un, Un_assoc]) 1);
+qed "parts_insert2";
+
goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
val parts_UN_subset1 = result();
@@ -163,7 +170,7 @@
Addsimps [parts_Un, parts_UN, parts_UN1];
goal thy "insert X (parts H) <= parts(insert X H)";
-by (fast_tac (!claset addEs [imp_of_subset parts_mono]) 1);
+by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1);
qed "parts_insert_subset";
(*Especially for reasoning about the Fake rule in traces*)
@@ -304,7 +311,7 @@
qed "analyze_Un";
goal thy "insert X (analyze H) <= analyze(insert X H)";
-by (fast_tac (!claset addEs [imp_of_subset analyze_mono]) 1);
+by (fast_tac (!claset addEs [impOfSubs analyze_mono]) 1);
qed "analyze_insert";
(** Rewrite rules for pulling out atomic messages **)
@@ -400,7 +407,7 @@
\ insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))";
by (rtac equalityI 1);
by (best_tac (!claset addIs [analyze.Fst,
- imp_of_subset analyze_insert_subset_MPair2]) 2);
+ impOfSubs analyze_insert_subset_MPair2]) 2);
br subsetI 1;
be analyze.induct 1;
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -410,7 +417,7 @@
\ insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))";
by (rtac equalityI 1);
by (best_tac (!claset addIs [analyze.Fst,
- imp_of_subset analyze_insert_subset_MPair2]) 2);
+ impOfSubs analyze_insert_subset_MPair2]) 2);
br subsetI 1;
be analyze.induct 1;
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -423,7 +430,7 @@
\ insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))";
by (rtac equalityI 1);
by (best_tac (!claset addIs [analyze.Fst,
- imp_of_subset analyze_insert_subset_MPair2]) 2);
+ impOfSubs analyze_insert_subset_MPair2]) 2);
br subsetI 1;
be analyze.induct 1;
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -471,12 +478,12 @@
(*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 [imp_of_subset analyze_mono])));
+by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analyze_mono])));
val lemma = result();
goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)";
by (fast_tac (!claset addIs [lemma]
- addEs [imp_of_subset analyze_mono]) 1);
+ addEs [impOfSubs analyze_mono]) 1);
qed "analyze_UN_analyze";
Addsimps [analyze_UN_analyze];
@@ -595,8 +602,8 @@
br subsetI 1;
be analyze.induct 1;
by (best_tac
- (!claset addEs [imp_of_subset synthesize_increasing,
- imp_of_subset analyze_mono]) 5);
+ (!claset addEs [impOfSubs synthesize_increasing,
+ impOfSubs analyze_mono]) 5);
by (Best_tac 1);
by (deepen_tac (!claset addIs [analyze.Fst]) 0 1);
by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);