--- a/src/HOL/Auth/Yahalom.ML Mon Oct 28 13:01:25 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML Mon Oct 28 13:02:37 1996 +0100
@@ -14,6 +14,7 @@
proof_timing:=true;
HOL_quantifiers := false;
+Pretty.setdepth 20;
(*Weak liveness: there are traces that reach the end*)
@@ -61,7 +62,7 @@
bind_thm ("YM4_parts_sees_Spy",
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-(*Relates to both YM4 and Revl*)
+(*Relates to both YM4 and Oops*)
goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
\ : set_of_list evs ==> \
\ K : parts (sees lost Spy evs)";
@@ -90,36 +91,29 @@
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
+(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. [| evs : yahalom lost; A ~: lost |] \
-\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
+ "!!evs. evs : yahalom lost \
+\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
by (parts_induct_tac 1);
by (Auto_tac());
-qed "Spy_not_see_shrK";
-
-bind_thm ("Spy_not_analz_shrK",
- [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
-
-Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
+qed "Spy_see_shrK";
+Addsimps [Spy_see_shrK];
-(*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*)
-val major::prems =
-goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \
-\ evs : yahalom lost; \
-\ A:lost ==> R \
-\ |] ==> R";
-by (rtac ccontr 1);
-by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
-by (swap_res_tac prems 2);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
-qed "Spy_see_shrK_E";
+goal thy
+ "!!evs. evs : yahalom lost \
+\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
+qed "Spy_analz_shrK";
+Addsimps [Spy_analz_shrK];
-bind_thm ("Spy_analz_shrK_E",
- analz_subset_parts RS subsetD RS Spy_see_shrK_E);
+goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
+\ evs : yahalom lost |] ==> A:lost";
+by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+qed "Spy_see_shrK_D";
-AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
+bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
+AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
(*** Future keys can't be seen or used! ***)
@@ -160,6 +154,16 @@
qed "Says_imp_old_keys";
+(*Ready-made for the classical reasoner*)
+goal thy "!!evs. [| Says A B {|Crypt {|b, Key (newK evs), na, nb|} K, X|} \
+\ : set_of_list evs; evs : yahalom lost |] \
+\ ==> R";
+by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset addsimps [parts_insertI])) 1);
+qed "Says_too_new_key";
+AddSEs [Says_too_new_key];
+
+
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
goal thy "!!evs. evs : yahalom lost ==> \
@@ -167,7 +171,6 @@
\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
by (parts_induct_tac 1);
by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
-
(*YM1, YM2 and YM3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
(*Fake and YM4: these messages send unknown (X) components*)
@@ -198,40 +201,25 @@
Addsimps [new_keys_not_used, new_keys_not_analzd];
-(*Describes the form of Key K when the following message is sent. The use of
- "parts" strengthens the induction hyp for proving the Fake case. The
- assumption A ~: lost prevents its being a Faked message. (Based
- on NS_Shared/Says_S_message_form) *)
-goal thy
- "!!evs. evs: yahalom lost ==> \
-\ Crypt {|B, Key K, NA, NB|} (shrK A) : parts (sees lost Spy evs) \
-\ --> A ~: lost --> (EX evt: yahalom lost. K = newK evt)";
-by (parts_induct_tac 1);
-by (Auto_tac());
-qed_spec_mp "Reveal_message_lemma";
-
-(*EITHER describes the form of Key K when the following message is sent,
- OR reduces it to the Fake case.*)
-
+(*Describes the form of K when the Server sends this message. Useful for
+ Oops as well as main secrecy property.*)
goal thy
- "!!evs. [| Says S A {|Crypt {|B, Key K, NA, NB|} (shrK A), X|} \
-\ : set_of_list evs; \
-\ evs : yahalom lost |] \
-\ ==> (EX evt: yahalom lost. K = newK evt) \
-\ | Key K : analz (sees lost Spy evs)";
-br (Reveal_message_lemma RS disjCI) 1;
-ba 1;
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addDs [impOfSubs analz_subset_parts]) 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
-qed "Reveal_message_form";
+ "!!evs. [| Says Server A \
+\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), X|} : set_of_list evs; \
+\ evs : yahalom lost |] \
+\ ==> (EX evt: yahalom lost. K = Key(newK evt))";
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "Says_Server_message_form";
(*For proofs involving analz. We again instantiate the variable to "lost".*)
val analz_Fake_tac =
- dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Reveal_message_form 7;
+ forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
+ forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+ assume_tac 7 THEN Full_simp_tac 7 THEN
+ REPEAT ((etac bexE ORELSE' hyp_subst_tac) 7);
(****
@@ -273,16 +261,15 @@
by (etac yahalom.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 8));
by (ALLGOALS (*Takes 26 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
setloop split_tac [expand_if])));
(** LEVEL 5 **)
-(*Reveal case 2, YM4, Fake*)
-by (EVERY (map spy_analz_tac [6, 4, 2]));
-(*Reveal case 1, YM3, Base*)
+(*YM4, Fake*)
+by (EVERY (map spy_analz_tac [4, 2]));
+(*Oops, YM3, Base*)
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
qed_spec_mp "analz_image_newK";
@@ -290,7 +277,7 @@
"!!evs. evs : yahalom lost ==> \
\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
\ (K = newK evt | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
+by (asm_simp_tac (HOL_ss addsimps [analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
qed "analz_insert_Key_newK";
@@ -300,31 +287,28 @@
goal thy
"!!evs. evs : yahalom lost ==> \
-\ EX A' B' NA' NB'. ALL A B NA NB. \
+\ EX A' B' NA' NB' X'. ALL A B NA NB X. \
\ Says Server A \
-\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
-\ : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB'";
+\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|} \
+\ : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
by (etac yahalom.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (Step_tac 1);
+by (ex_strip_tac 2);
+by (Fast_tac 2);
(*Remaining case: YM3*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a very new message, and handle this case by contradiction*)
-by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
- delrules [conjI] (*prevent split-up into 4 subgoals*)
- addss (!simpset addsimps [parts_insertI])) 1);
+by (Fast_tac 1); (*uses Says_too_new_key*)
val lemma = result();
goal thy
"!!evs. [| Says Server A \
-\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|} \
\ : set_of_list evs; \
\ Says Server A' \
-\ {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), \
-\ Crypt {|Agent A', Key K|} (shrK B')|} \
+\ {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), X'|} \
\ : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
@@ -350,24 +334,10 @@
qed "A_trust_YM3";
-(*Describes the form of K when the Server sends this message.*)
-goal thy
- "!!evs. [| Says Server A \
-\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
-\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
-\ evs : yahalom lost |] \
-\ ==> (EX evt: yahalom lost. K = Key(newK evt))";
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "Says_Server_message_form";
-
-
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; \
-\ evs : yahalom lost; evt : yahalom lost |] \
+ "!!evs. [| A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Says Server A \
\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), \
\ Crypt {|Agent A, Key K|} (shrK B)|} \
@@ -376,28 +346,18 @@
\ Key K ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([analz_subset_parts RS contra_subsetD,
analz_insert_Key_newK] @ pushes)
setloop split_tac [expand_if])));
(*YM3*)
-by (fast_tac (!claset addIs [parts_insertI]
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 2);
-(*Reveal case 2, OR4, Fake*)
+by (Fast_tac 2); (*uses Says_too_new_key*)
+(*OR4, Fake*)
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
-(*Reveal case 1*) (** LEVEL 6 **)
-by (case_tac "Aa : lost" 1);
-(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
-by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
-by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
-(*So now we have Aa ~: lost *)
-bd (Says_imp_sees_Spy RS parts.Inj) 1;
+(*Oops*) (** LEVEL 6 **)
by (fast_tac (!claset delrules [disjE]
- addSEs [MPair_parts]
- addDs [A_trust_YM3, unique_session_keys]
+ addDs [unique_session_keys]
addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -448,12 +408,175 @@
by (Fast_tac 1);
qed "B_trusts_YM4_shrK";
-(*B knows, by the second part of A's message, that the Server distributed
- the key quoting nonce NB. This part says nothing about agent names.*)
+
+(*** General properties of nonces ***)
+
+goal thy "!!evs. evs : yahalom lost ==> \
+\ length evs <= length evt --> \
+\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
+by (etac yahalom.induct 1);
+(*auto_tac does not work here, as it performs safe_tac first*)
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
+ addcongs [disj_cong])));
+by (REPEAT_FIRST
+ (fast_tac (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un, Suc_leD]
+ addss (!simpset))));
+val lemma = result();
+
+(*Variant needed for the main theorem below*)
+goal thy
+ "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
+\ ==> Nonce (newN evs') ~: parts (sees lost C evs)";
+by (fast_tac (!claset addDs [lemma]) 1);
+qed "new_nonces_not_seen";
+Addsimps [new_nonces_not_seen];
+
+(*Another variant: old messages must contain old nonces!*)
+goal thy
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Nonce (newN evt) : parts {X}; \
+\ evs : yahalom lost \
+\ |] ==> length evt < length evs";
+by (rtac ccontr 1);
+by (dtac leI 1);
+by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
+ addIs [impOfSubs parts_mono]) 1);
+qed "Says_imp_old_nonces";
+
+
+(** The Nonce NB uniquely identifies B's message. **)
+
+val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
+
+goal thy
+ "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
+\ Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
+\ --> B ~: lost --> NA = NA' & A = A' & B = B'";
+by (parts_induct_tac 1); (*TWO MINUTES*)
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
+(*YM2: creation of new Nonce. Move assertion into global context*)
+by (expand_case_tac "NB = ?y" 1);
+by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
+val lemma = result();
+
goal thy
- "!!evs. evs : yahalom lost \
-\ ==> Key K ~: analz (sees lost Spy evs) --> \
-\ Crypt (Nonce NB) K : parts (sees lost Spy evs) --> \
+ "!!evs.[| Crypt {|Agent A, Nonce NA, NB|} (shrK B) \
+\ : parts (sees lost Spy evs); \
+\ Crypt {|Agent A', Nonce NA', NB|} (shrK B') \
+\ : parts (sees lost Spy evs); \
+\ evs : yahalom lost; B ~: lost; B' ~: lost |] \
+\ ==> NA' = NA & A' = A & B' = B";
+by (dtac lemma 1);
+by (REPEAT (etac exE 1));
+(*Duplicate the assumption*)
+by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
+by (fast_tac (!claset addSDs [spec]) 1);
+qed "unique_NB";
+
+fun lost_tac s =
+ case_tac ("(" ^ s ^ ") : lost") THEN'
+ SELECT_GOAL
+ (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+ REPEAT_DETERM (etac MPair_analz 1) THEN
+ dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
+ assume_tac 1 THEN Fast_tac 1);
+
+fun lost_tac s =
+ case_tac ("(" ^ s ^ ") : lost") THEN'
+ SELECT_GOAL
+ (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+ REPEAT_DETERM (etac MPair_analz 1) THEN
+ THEN_BEST_FIRST
+ (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
+ (has_fewer_prems 1, size_of_thm)
+ (Step_tac 1));
+
+
+(*Variant useful for proving secrecy of NB*)
+goal thy
+ "!!evs.[| Says C D {|X, Crypt {|Agent A, Nonce NA, NB|} (shrK B)|} \
+\ : set_of_list evs; B ~: lost; \
+\ Says C' D' {|X', Crypt {|Agent A', Nonce NA', NB|} (shrK B')|} \
+\ : set_of_list evs; \
+\ NB ~: analz (sees lost Spy evs); \
+\ evs : yahalom lost |] \
+\ ==> NA' = NA & A' = A & B' = B";
+by (lost_tac "B'" 1);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addSEs [MPair_parts]
+ addDs [unique_NB]) 1);
+qed "Says_unique_NB";
+
+goal thy
+ "!!evs. [| B ~: lost; evs : yahalom lost |] \
+\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
+\ Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B) : parts (sees lost Spy evs) \
+\ --> Crypt {|Agent A', Nonce NB, NB'|} (shrK B') ~: parts (sees lost Spy evs)";
+by (etac yahalom.induct 1);
+by parts_Fake_tac;
+by (REPEAT_FIRST
+ (rtac impI THEN'
+ dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
+ mp_tac));
+by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
+ addss (!simpset)) 2);
+by (ALLGOALS Asm_simp_tac);
+by (fast_tac (!claset addss (!simpset)) 1);
+by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
+ addSIs [parts_insertI]
+ addSEs partsEs
+ addEs [Says_imp_old_nonces RS less_irrefl]
+ addss (!simpset)) 1);
+val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
+
+
+
+(**** Towards proving secrecy of Nonce NB ****)
+
+(*B knows, by the second part of A's message, that the Server distributed
+ the key quoting nonce NB. This part says nothing about agent names.
+ Secrecy of NB is crucial.*)
+goal thy
+ "!!evs. evs : yahalom lost \
+\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
+\ Crypt (Nonce NB) K : parts (sees lost Spy evs) --> \
+\ (EX A B NA. Says Server A \
+\ {|Crypt {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|} (shrK A), \
+\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ : set_of_list evs)";
+by (etac yahalom.induct 1);
+by parts_Fake_tac;
+by (fast_tac (!claset addss (!simpset)) 1);
+by (REPEAT_FIRST
+ (rtac impI THEN'
+ dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
+by (ALLGOALS Asm_simp_tac);
+(*Fake, YM3, YM4*)
+by (Fast_tac 2);
+by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 1);
+(*YM4*)
+by (Step_tac 1);
+by (lost_tac "A" 1);
+by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
+ A_trust_YM3]) 1);
+val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
+
+
+(*This is the original version of the result above. But it is of little
+ value because it assumes secrecy of K, which we cannot be assured of
+ until we know that K is fresh -- which we do not know at the point this
+ result is applied.*)
+goal thy
+ "!!evs. evs : yahalom lost \
+\ ==> Key K ~: analz (sees lost Spy evs) --> \
+\ Crypt (Nonce NB) K : parts (sees lost Spy evs) --> \
\ (EX A B NA. Says Server A \
\ {|Crypt {|Agent B, Key K, \
\ Nonce NA, Nonce NB|} (shrK A), \
@@ -468,37 +591,216 @@
by (ALLGOALS Asm_simp_tac);
(*Fake, YM3, YM4*)
by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
+ addDs [impOfSubs analz_subset_parts]) 1);
by (Fast_tac 1);
(*YM4*)
by (Step_tac 1);
-by (case_tac "A : lost" 1);
-(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
-by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
-by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
+by (lost_tac "A" 1);
by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
A_trust_YM3]) 1);
-val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
+result() RS mp RSN (2, rev_mp);
+
+
+(*YM3 can only be triggered by YM2*)
+goal thy
+ "!!evs. [| Says Server A \
+\ {|Crypt {|Agent B, k, na, nb|} (shrK A), X|} : set_of_list evs; \
+\ evs : yahalom lost |] \
+\ ==> EX B'. Says B' Server \
+\ {| Agent B, Crypt {|Agent A, na, nb|} (shrK B) |} \
+\ : set_of_list evs";
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS Fast_tac);
+qed "Says_Server_imp_YM2";
+
+
+(** Dedicated tactics for the nonce secrecy proofs **)
+
+val no_nonce_tac = SELECT_GOAL
+ (REPEAT (resolve_tac [impI, notI] 1) THEN
+ REPEAT (hyp_subst_tac 1) THEN
+ etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
+ THEN
+ etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
+ THEN
+ REPEAT_FIRST assume_tac);
+
+val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
+
+fun grind_tac i =
+ SELECT_GOAL
+ (REPEAT_FIRST
+ (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
+ assume_tac ORELSE'
+ depth_tac (!claset delrules [conjI]
+ addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
+ impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
+
+(*The only nonces that can be found with the help of session keys are
+ those distributed as nonce NB by the Server. The form of the theorem
+ recalls analz_image_newK, but it is much more complicated.*)
+goal thy
+ "!!evs. evs : yahalom lost ==> \
+\ ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
+\ (EX K: newK``E. EX A B na X. \
+\ Says Server A \
+\ {|Crypt {|Agent B, Key K, na, Nonce NB|} (shrK A), X|} \
+\ : set_of_list evs) | Nonce NB : analz (sees lost Spy evs)";
+by (etac yahalom.induct 1);
+by analz_Fake_tac;
+by (ALLGOALS (*45 SECONDS*)
+ (asm_simp_tac
+ (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
+ analz_image_newK,
+ insert_Key_singleton, insert_Key_image]
+ @ pushes)
+ setloop split_tac [expand_if])));
+(*Base*)
+by (fast_tac (!claset addss (!simpset)) 1);
+(*Fake*) (** LEVEL 4 **)
+by (spy_analz_tac 1);
+(*YM1-YM3*)
+by (EVERY (map grind_tac [3,2,1]));
+(*Oops*)
+by (Full_simp_tac 2);
+by (REPEAT ((eresolve_tac [bexE] ORELSE' hyp_subst_tac) 2));
+by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
+by (grind_tac 2);
+by (fast_tac (!claset delrules [bexI]
+ addDs [unique_session_keys]
+ addss (!simpset)) 2);
+(*YM4*)
+(** LEVEL 11 **)
+br (impI RS allI) 1;
+by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1 THEN
+ Fast_tac 1);
+by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
+by (asm_simp_tac (!simpset addsimps [analz_image_newK]
+ setloop split_tac [expand_if]) 1);
+(** LEVEL 15 **)
+by (grind_tac 1);
+by (REPEAT (dtac not_analz_insert 1));
+by (lost_tac "A" 1);
+by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1
+ THEN REPEAT (assume_tac 1));
+by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
+by (fast_tac (!claset delrules [conjI]
+ addIs [impOfSubs (subset_insertI RS analz_mono)]
+ addss (!simpset)) 1);
+val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
+
+
+(*Version required below: if NB can be decrypted using a session key then it
+ was distributed with that key. The more general form above is required
+ for the induction to carry through.*)
+goal thy
+ "!!evs. [| Says Server A \
+\ {|Crypt {|Agent B, Key (newK evt), na, Nonce NB'|} (shrK A), X|} \
+\ : set_of_list evs; \
+\ Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs)); \
+\ evs : yahalom lost |] \
+\ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
+by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
+by (dtac Nonce_secrecy 1 THEN assume_tac 1);
+by (fast_tac (!claset addDs [unique_session_keys]
+ addss (!simpset)) 1);
+val single_Nonce_secrecy = result();
+
+
+goal thy
+ "!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
+\ ==> Says B Server \
+\ {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
+\ : set_of_list evs --> \
+\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) --> \
+\ Nonce NB ~: analz (sees lost Spy evs)";
+by (etac yahalom.induct 1);
+by analz_Fake_tac;
+by (ALLGOALS
+ (asm_simp_tac
+ (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
+ analz_insert_Key_newK] @ pushes)
+ setloop split_tac [expand_if])));
+by (fast_tac (!claset addSIs [parts_insertI]
+ addSEs partsEs
+ addEs [Says_imp_old_nonces RS less_irrefl]
+ addss (!simpset)) 2);
+(*Proof of YM2*) (** LEVEL 5 **)
+by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2));
+by (fast_tac (!claset addIs [parts_insertI]
+ addSEs partsEs
+ addEs [Says_imp_old_nonces RS less_irrefl]
+ addss (!simpset)) 3);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2);
+(*Prove YM3 by showing that no NB can also be an NA*)
+by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
+by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
+(*Fake*) (** LEVEL 10 **)
+by (SELECT_GOAL (REPEAT (Safe_step_tac 1 ORELSE spy_analz_tac 1)) 1);
+(*YM4*)
+by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1);
+(** LEVEL 14 **)
+by (lost_tac "Aa" 1);
+bd (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1;
+by (forward_tac [Says_Server_message_form] 3);
+by (forward_tac [Says_Server_imp_YM2] 4);
+by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
+by (Full_simp_tac 1);
+(** LEVEL 20 **)
+by (REPEAT_FIRST hyp_subst_tac);
+by (lost_tac "Ba" 1);
+bd (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1;
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addSEs [MPair_parts]) 1);
+by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1));
+bd Spy_not_see_encrypted_key 1;
+by (REPEAT (assume_tac 1 ORELSE Fast_tac 1));
+by (spy_analz_tac 1);
+(*Oops case*) (** LEVEL 28 **)
+by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
+by (step_tac (!claset delrules [disjE, conjI]) 1);
+by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
+by (expand_case_tac "NB = NBa" 1);
+by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
+br conjI 1;
+by (no_nonce_tac 1);
+(** LEVEL 35 **)
+by (thin_tac "?PP|?QQ" 1); (*subsumption!*)
+by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
+val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
+
(*What can B deduce from receipt of YM4? Note how the two components of
the message contribute to a single conclusion about the Server's message.
It's annoying that the "Says A Spy" assumption must quantify over
- ALL POSSIBLE nonces instead of our particular NB. Perhaps a different
- proof of B_trusts_YM4_newK could eliminate this problem.*)
+ ALL POSSIBLE keys instead of our particular K (though at least the
+ nonces are forced to agree with NA and NB). *)
goal thy
- "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \
+ "!!evs. [| Says B Server \
+\ {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
+\ : set_of_list evs; \
+\ Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \
\ Crypt (Nonce NB) K|} : set_of_list evs; \
-\ ALL N N'. Says A Spy {|N,N', Key K|} ~: set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> EX NA. Says Server A \
+\ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
+\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
+\ ==> Says Server A \
\ {|Crypt {|Agent B, Key K, \
\ Nonce NA, Nonce NB|} (shrK A), \
\ Crypt {|Agent A, Key K|} (shrK B)|} \
\ : set_of_list evs";
-be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
-bd B_trusts_YM4_shrK 1;
+by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
+by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
+ dtac B_trusts_YM4_shrK 1);
bd B_trusts_YM4_newK 3;
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
-by (fast_tac (!claset addDs [unique_session_keys]) 2);
-by (fast_tac (!claset addDs [Spy_not_see_encrypted_key]) 1);
+by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
+by (dresolve_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1));
+by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
qed "B_trust_YM4";
+
+
+