src/HOL/Auth/Yahalom.ML

-(*  Title:      HOL/Auth/OtwayRees
+(*  Title:      HOL/Auth/Yahalom
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
 Inductive relation "otway" for the Yahalom protocol.

 From page 257 of
   Burrows, Abadi and Needham.  A Logic of Authentication.
   Proc. Royal Soc. 426 (1989)
 *)
 
-open OtwayRees;
+open Yahalom;
 
 proof_timing:=true;
 HOL_quantifiers := false;
+
+
+(** Weak liveness: there are traces that reach the end **)
+
+goal thy 
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
+\        ==> EX X NB K. EX evs: yahalom.          \
+\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
+by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
+by (ALLGOALS Fast_tac);
+qed "weak_liveness";
+
 
 (**** Inductive proofs about yahalom ****)
 
 (*The Enemy can see more than anybody else, except for their initial state*)
 goal thy 

 AddSEs   [not_Notes RSN (2, rev_notE)];
 
 
 (** For reasoning about the encrypted portion of messages **)
 
-goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
-\                X : analz (sees Enemy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
-qed "YM2_analz_sees_Enemy";
-
-goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
+(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
 \                X : analz (sees Enemy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
 qed "YM4_analz_sees_Enemy";
 
-goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
+\                  : set_of_list evs ==> \
 \                K : parts (sees Enemy evs)";
 by (fast_tac (!claset addSEs partsEs
 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
-qed "YM5_parts_sees_Enemy";
-
-(*YM2_analz... and YM4_analz... let us treat those cases using the same 
-  argument as for the Fake case.  This is possible for most, but not all,
-  proofs: Fake does not invent new nonces (as in YM2), and of course Fake
-  messages originate from the Enemy. *)
-
-val YM2_YM4_tac = 
-    dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
-    dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
+qed "YM4_parts_sees_Enemy";
+
 
 
 (*** Shared keys are not betrayed ***)
 
 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
 goal thy 
  "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
 \        Key (shrK A) ~: parts (sees Enemy evs)";
 be yahalom.induct 1;
-by YM2_YM4_tac;
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+by (ALLGOALS Asm_simp_tac);
+by (stac insert_commute 3);
 by (Auto_tac());
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-			     impOfSubs Fake_parts_insert]) 1);
+(*Fake and YM4 are similar*)
+by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
+					impOfSubs Fake_parts_insert])));
 qed "Enemy_not_see_shrK";
 
 bind_thm ("Enemy_not_analz_shrK",
 	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
 

 
 (*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 Enemy evs);       \
-\             evs : yahalom;                                 \
+\             evs : yahalom;                               \
 \             A:bad ==> R                                  \
 \           |] ==> R";
 br ccontr 1;
 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
 by (swap_res_tac prems 2);

   induction! *)
 goal thy "!!evs. evs : yahalom ==> \
 \                length evs <= length evs' --> \
 \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
 be yahalom.induct 1;
-by YM2_YM4_tac;
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS Asm_simp_tac);
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-				       impOfSubs parts_insert_subset_Un,
-				       Suc_leD]
-			        addss (!simpset))));
+					   impOfSubs parts_insert_subset_Un,
+					   Suc_leD]
+			            addss (!simpset))));
 val lemma = result();
 
 (*Variant needed for the main theorem below*)
 goal thy 
  "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \

   ...very like new_keys_not_seen*)
 goal thy "!!evs. evs : yahalom ==> \
 \                length evs <= length evs' --> \
 \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
 be yahalom.induct 1;
-by YM2_YM4_tac;
-bd YM5_parts_sees_Enemy 7;
-by (ALLGOALS Asm_simp_tac);
-(*YM1 and YM3*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
-(*Fake, YM2, YM4: these messages send unknown (X) components*)
-by (EVERY 
-    (map
+by (forward_tac [YM4_parts_sees_Enemy] 6);
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+by (ALLGOALS Asm_full_simp_tac);
+(*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*)
+by (stac insert_commute 2);
+by (Simp_tac 2);
+(*YM4: the only way K could have been used is if it had been seen,
+  contradicting new_keys_not_seen*)
+by (ALLGOALS
      (best_tac
-      (!claset addSDs [newK_invKey]
-	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
 		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
 		      Suc_leD]
-	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
-	       addss (!simpset)))
-     [3,2,1]));
-(*YM5: dummy message*)
-by (best_tac (!claset addSDs [newK_invKey]
-		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
-			addIs  [less_SucI, impOfSubs keysFor_mono]
-			addss (!simpset addsimps [le_def])) 1);
+	       addDs [impOfSubs analz_subset_parts]
+	       addEs [new_keys_not_seen RSN(2,rev_notE)]
+	       addss (!simpset))));
 val lemma = result();
 
 goal thy 
  "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
 \        newK evs' ~: keysFor (parts (sees C evs))";

 goal thy 
  "!!evs. evs : yahalom ==> \
 \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
 \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
 be yahalom.induct 1;
-by YM2_YM4_tac;
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
 (*Deals with Faked messages*)
-by (best_tac (!claset addSEs partsEs
-		      addDs [impOfSubs analz_subset_parts,
-                             impOfSubs parts_insert_subset_Un]
-                      addss (!simpset)) 2);
-(*Base case and YM5*)
+by (EVERY 
+    (map (best_tac (!claset addSEs partsEs
+			    addDs [impOfSubs analz_subset_parts,
+				   impOfSubs parts_insert_subset_Un]
+			    addss (!simpset)))
+     [3,2]));
+(*Base case*)
 by (Auto_tac());
 result();
 
 
 (** Specialized rewriting for this proof **)

 
 
 
 (** Session keys are not used to encrypt other session keys **)
 
-(*Could generalize this so that the X component doesn't have to be first
-  in the message?*)
-val enemy_analz_tac =
-  SELECT_GOAL 
-   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
-	   dtac (impOfSubs Fake_analz_insert) 1,
-	   eresolve_tac [asm_rl, synth.Inj] 1,
-	   Fast_tac 1,
-	   Asm_full_simp_tac 1,
-	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
-	   ]);
-
-
 (*Lemma for the trivial direction of the if-and-only-if*)
 goal thy  
  "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
 \         (K : nE | Key K : analz sEe)  ==>     \
 \        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";

 goal thy  
  "!!evs. evs : yahalom ==> \
 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
 \           (K : newK``E | Key K : analz (sees Enemy evs))";
 be yahalom.induct 1;
-bd YM2_analz_sees_Enemy 4;
 bd YM4_analz_sees_Enemy 6;
 by (REPEAT_FIRST (resolve_tac [allI, lemma]));
-by (ALLGOALS (*Takes 35 secs*)
+by (ALLGOALS 
     (asm_simp_tac 
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
 			 @ pushes)
                setloop split_tac [expand_if])));
 (*YM4*) 
-by (enemy_analz_tac 5);
+by (enemy_analz_tac 4);
 (*YM3*)
-by (Fast_tac 4);
-(*YM2*) (** LEVEL 7 **)
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
-    (insert_commute RS ssubst) 3);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
-    (insert_commute RS ssubst) 3);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
-by (enemy_analz_tac 3);
-(*Fake case*) (** LEVEL 11 **)
-by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
-    (insert_commute RS ssubst) 2);
+by (Fast_tac 3);
+(*Fake case*)
 by (enemy_analz_tac 2);
 (*Base case*)
 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
 qed_spec_mp "analz_image_newK";
-
 
 goal thy
  "!!evs. evs : yahalom ==>                               \
 \        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
 \        (K = newK evt | Key K : analz (sees Enemy evs))";

 qed "analz_insert_Key_newK";
 
 
 (*Describes the form *and age* of K when the following message is sent*)
 goal thy 
- "!!evs. [| Says Server B \
-\            {|NA, Crypt {|NA, K|} (shrK A),                      \
-\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
+ "!!evs. [| Says Server A                                           \
+\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
+\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
 \           evs : yahalom |]                                        \
-\        ==> (EX evt:yahalom. K = Key(newK evt) & \
-\                           length evt < length evs) &            \
-\            (EX i. NA = Nonce i)";
+\        ==> (EX evt:yahalom. K = Key(newK evt) &                   \
+\                           length evt < length evs)";
 be rev_mp 1;
 be yahalom.induct 1;
 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
 qed "Says_Server_message_form";
 
 
-(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
+(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3
+  As with Otway-Rees, proof does not need uniqueness of session keys.*)
 goal thy 
  "!!evs. [| Says Server A \
-\            {|NA, Crypt {|NA, K|} (shrK B),                      \
-\                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
-\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>              \
+\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
+\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
+\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>                  \
 \     K ~: analz (sees Enemy evs)";
 be rev_mp 1;
 be yahalom.induct 1;
-bd YM2_analz_sees_Enemy 4;
 bd YM4_analz_sees_Enemy 6;
 by (ALLGOALS Asm_simp_tac);
 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
 by (REPEAT_FIRST (resolve_tac [conjI, impI]));
 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));

 by (ALLGOALS
     (asm_full_simp_tac 
      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
 			  analz_insert_Key_newK] @ pushes)
                setloop split_tac [expand_if])));
+(*YM4*)
+by (enemy_analz_tac 3);
 (*YM3*)
-by (fast_tac (!claset addSEs [less_irrefl]) 3);
+by (fast_tac (!claset addSEs [less_irrefl]) 2);
 (*Fake*) (** LEVEL 10 **)
-by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
-by (enemy_analz_tac 1);
-(*YM4*)
-by (mp_tac 2);
-by (enemy_analz_tac 2);
-(*YM2*)
-by (mp_tac 1);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
-    (insert_commute RS ssubst) 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (enemy_analz_tac 1);
 qed "Enemy_not_see_encrypted_key";
-
-
-
-(*** Session keys are issued at most once, and identify the principals ***)
-
-(** First, two lemmas for the Fake, YM2 and YM4 cases **)
-
-goal thy 
- "!!evs. [| X : synth (analz (sees Enemy evs));                \
-\           Crypt X' (shrK C) : parts{X};                      \
-\           C ~: bad;  evs : yahalom |]  \
-\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
-by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
-	              addDs [impOfSubs parts_insert_subset_Un]
-                      addss (!simpset)) 1);
-qed "Crypt_Fake_parts";
-
-goal thy 
- "!!evs. [| Crypt X' K : parts (sees A evs);  evs : yahalom |]  \
-\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
-\            Crypt X' K : parts {Y}";
-bd parts_singleton 1;
-by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
-qed "Crypt_parts_singleton";
-
-fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
-
-(*The Key K uniquely identifies a pair of senders in the message encrypted by
-  C, but if C=Enemy then he could send all sorts of nonsense.*)
-goal thy 
- "!!evs. evs : yahalom ==>                                     \
-\      EX A B. ALL C.                                        \
-\         C ~: bad -->                                       \
-\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
-\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
-by (Simp_tac 1);
-be yahalom.induct 1;
-bd YM2_analz_sees_Enemy 4;
-bd YM4_analz_sees_Enemy 6;
-by (ALLGOALS 
-    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
-by (REPEAT_FIRST (etac exE));
-(*YM4*)
-by (ex_strip_tac 4);
-by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
-			      Crypt_parts_singleton]) 4);
-(*YM3: Case split propagates some context to other subgoal...*)
-	(** LEVEL 8 **)
-by (excluded_middle_tac "K = newK evsa" 3);
-by (Asm_simp_tac 3);
-by (REPEAT (ares_tac [exI] 3));
-(*...we prove this case by contradiction: the key is too new!*)
-by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
-		      addSEs partsEs
-		      addEs [Says_imp_old_keys RS less_irrefl]
-	              addss (!simpset)) 3);
-(*YM2*) (** LEVEL 12 **)
-by (ex_strip_tac 2);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
-    (insert_commute RS ssubst) 2);
-by (Simp_tac 2);
-by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
-			      Crypt_parts_singleton]) 2);
-(*Fake*) (** LEVEL 16 **)
-by (ex_strip_tac 1);
-by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
-qed "unique_session_keys";
-
-(*It seems strange but this theorem is NOT needed to prove the main result!*)