src/HOL/Auth/OtwayRees.ML

 
 From page 244 of
   Burrows, Abadi and Needham.  A Logic of Authentication.
   Proc. Royal Soc. 426 (1989)
 *)
-
 
 open OtwayRees;
 
 proof_timing:=true;
 HOL_quantifiers := false;

     in  tac OR2_parts_sees_Spy 4 THEN 
         tac OR4_parts_sees_Spy 6 THEN
         tac Reveal_parts_sees_Spy 7
     end;
 
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
+fun parts_induct_tac i = SELECT_GOAL
+    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
+	     (*Fake message*)
+	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+					   impOfSubs Fake_parts_insert]
+                                    addss (!simpset)) 2)) THEN
+     (*Base case*)
+     fast_tac (!claset addss (!simpset)) 1 THEN
+     ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
     sends messages containing X! **)
 
-(*Spy never sees lost 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 : otway lost;  A ~: lost |]    \
 \        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
+by (parts_induct_tac 1);
 by (Auto_tac());
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                             impOfSubs Fake_parts_insert]) 1);
 qed "Spy_not_see_shrK";
 
 bind_thm ("Spy_not_analz_shrK",
           [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
 

   standard Fake rule.  
       The Union over C is essential for the induction! *)
 goal thy "!!evs. evs : otway lost ==> \
 \                length evs <= length evs' --> \
 \                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS Asm_simp_tac);
+by (parts_induct_tac 1);
 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));
 val lemma = result();

 (*Nobody can have USED keys that will be generated in the future.
   ...very like new_keys_not_seen*)
 goal thy "!!evs. evs : otway lost ==> \
 \                length evs <= length evs' --> \
 \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
+by (parts_induct_tac 1);
 (*OR1 and OR3*)
 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
 (*Fake, OR2, OR4: these messages send unknown (X) components*)
 by (EVERY 
     (map

            new_keys_not_used] MRS contra_subsetD);
 
 Addsimps [new_keys_not_used, new_keys_not_analzd];
 
 
-(** Lemmas concerning the form of items passed in messages **)
+
+(*** Proofs involving analz ***)
+
+(*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: otway lost ==>                                           \
+\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) &   \
+\          A ~: lost -->                                               \
+\        (EX evt: otway 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.*)
+
+goal thy 
+ "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
+\           evs : otway lost |]                      \
+\        ==> (EX evt: otway 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]
+                      addss (!simpset)) 1);
+qed "Reveal_message_form";
+
+
+(*For proofs involving analz.  We again instantiate the variable to "lost".*)
+val analz_Fake_tac = 
+    dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
+    dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
+    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
 
 
 (****
  The following is to prove theorems of the form
 

 result();
 
 
 (** Session keys are not used to encrypt other session keys **)
 
-(*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
-  assumptions on A are needed to prevent its being a Faked message.  (Based
-  on NS_Shared/Says_S_message_form) *)
-goal thy
- "!!evs. evs: otway lost ==>                                           \
-\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
-\          A ~: lost -->                                           \
-\        (EX evt: otway lost. K = newK evt)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-                             impOfSubs Fake_parts_insert]) 2);
-by (Auto_tac());
-val lemma = result() RS mp;
-
-
-(*EITHER describes the form of Key K when the following message is sent, 
-  OR     reduces it to the Fake case.*)
-goal thy 
- "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
-\           evs : otway lost |]                      \
-\        ==> (EX evt: otway lost. K = newK evt)          \
-\          | Key K : analz (sees lost Spy evs)";
-by (excluded_middle_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      addss (!simpset)) 2);
-by (forward_tac [lemma] 1);
-by (fast_tac (!claset addEs  partsEs
-                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
-by (Fast_tac 1);
-qed "Reveal_message_form";
-
-
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
  "!!evs. evs : otway lost ==> \
 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
-by (dtac OR2_analz_sees_Spy 4);
-by (dtac OR4_analz_sees_Spy 6);
-by (dtac Reveal_message_form 7);
+by analz_Fake_tac;
 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
 by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
 by (ALLGOALS (*Takes 28 secs*)
     (asm_simp_tac 
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]

                setloop split_tac [expand_if])));
 (** LEVEL 7 **)
 (*Reveal case 2, OR4, OR2, Fake*) 
 by (EVERY (map spy_analz_tac [7,5,3,2]));
 (*Reveal case 1, OR3, Base*)
-by (Auto_tac());
+by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
 qed_spec_mp "analz_image_newK";
 
 
 goal thy
  "!!evs. evs : otway lost ==>                               \

 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
 by (Step_tac 1);
 (*Remaining cases: OR3 and OR4*)
 by (ex_strip_tac 2);
 by (Fast_tac 2);
-by (excluded_middle_tac "K = Key(newK evsa)" 1);
-by (Asm_simp_tac 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
+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);
 val lemma = result();

 
 (**** Authenticity properties relating to NA ****)
 
 (*Only OR1 can have caused such a part of a message to appear.*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : otway lost |]               \
-\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
-\             : parts (sees lost Spy evs) -->                  \
-\            Says A B {|NA, Agent A, Agent B,               \
+ "!!evs. [| A ~: lost;  evs : otway lost |]                        \
+\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)               \
+\             : parts (sees lost Spy evs) -->                      \
+\            Says A B {|NA, Agent A, Agent B,                      \
 \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
 \             : set_of_list evs";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-by (Auto_tac());
+by (parts_induct_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
 
 
-(** The Nonce NA uniquely identifies A's  message. **)
+(** The Nonce NA uniquely identifies A's message. **)
 
 goal thy 
  "!!evs. [| evs : otway lost; A ~: lost |]               \
 \ ==> EX B'. ALL B.    \
 \        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
 \        --> B = B'";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-(*Base case*)
-by (fast_tac (!claset addss (!simpset)) 1);
-by (Step_tac 1);
+by (parts_induct_tac 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR1: creation of new Nonce.  Move assertion into global context*)
-by (excluded_middle_tac "NA = Nonce (newN evsa)" 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by (expand_case_tac "NA = ?y" 1);
 by (best_tac (!claset addSEs partsEs
                       addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
 val lemma = result();
 
 goal thy 

 \            (EX NB. Says Server B                                     \
 \                 {|NA,                                                \
 \                   Crypt {|NA, Key K|} (shrK A),                      \
 \                   Crypt {|NB, Key K|} (shrK B)|}                     \
 \                   : set_of_list evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 1);
+by (parts_induct_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (fast_tac (!claset addSIs [parts_insertI]
                       addSEs partsEs
                       addEs [Says_imp_old_nonces RS less_irrefl]
                       addss (!simpset)) 1);
-(*OR3 and OR4*)  (** LEVEL 5 **)
+(*OR3 and OR4*) 
 (*OR4*)
 by (REPEAT (Safe_step_tac 2));
 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
                       addEs  partsEs
                       addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
-(*OR3*)  (** LEVEL 8 **)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
+(*OR3*)  (** LEVEL 5 **)
+by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
 by (step_tac (!claset delrules [disjCI, impCE]) 1);
 by (fast_tac (!claset addSEs [MPair_parts]
                       addSDs [Says_imp_sees_Spy RS parts.Inj]
                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);

 \                       Crypt {|NB, Key K|} (shrK B)|}             \
 \                       : set_of_list evs";
 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "A_can_trust";
+qed "A_trust_OR4";
 
 
 (*Describes the form of K and NA when the Server sends this message.*)
 goal thy 
  "!!evs. [| Says Server B \

 \              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
 \                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
 \            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
-by (dtac OR2_analz_sees_Spy 4);
-by (dtac OR4_analz_sees_Spy 6);
-by (forward_tac [Reveal_message_form] 7);
+by analz_Fake_tac;
 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
 by (ALLGOALS
     (asm_full_simp_tac 
      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
                           analz_insert_Key_newK] @ pushes)

 by (excluded_middle_tac "Aa : lost" 1);
 (*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
 by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
 (*So now we have  Aa ~: lost *)
-by (dtac A_can_trust 1);
+by (dtac A_trust_OR4 1);
 by (REPEAT (assume_tac 1));
 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 goal thy 

 \             : parts (sees lost Spy evs) -->                  \
 \            (EX X'. Says B Server                             \
 \             {|NA, Agent A, Agent B, X',                      \
 \               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
 \             : set_of_list evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-by (Auto_tac());
+by (parts_induct_tac 1);
+by (auto_tac (!claset, !simpset addcongs [conj_cong]));
 qed_spec_mp "Crypt_imp_OR2";
 
 
 (** The Nonce NB uniquely identifies B's  message. **)
 
 goal thy 
  "!!evs. [| evs : otway lost; B ~: lost |]               \
-\ ==> EX NA' A'. ALL NA A.                              \
+\ ==> EX NA' A'. ALL NA A.                               \
 \      Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
 \      --> NA = NA' & A = A'";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset delrules [conjI,conjE]
-		      addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 2);
-(*Base case*)
-by (fast_tac (!claset addss (!simpset)) 1);
-by (Step_tac 1);
+by (parts_induct_tac 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*OR2: creation of new Nonce.  Move assertion into global context*)
-by (excluded_middle_tac "NB = Nonce (newN evsa)" 1);
-by (Asm_simp_tac 1);
-by (fast_tac (!claset addSIs [exI]) 1);
+by (expand_case_tac "NB = ?y" 1);
 by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
 val lemma = result();
 
 goal thy 
  "!!evs.[| Crypt {|NA, NB, Agent A, Agent B|} (shrK B) \

 \             : set_of_list evs                                          \
 \             --> Says Server B                                          \
 \                  {|NA, Crypt {|NA, Key K|} (shrK A),                   \
 \                        Crypt {|NB, Key K|} (shrK B)|}                  \
 \                   : set_of_list evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
-                              impOfSubs Fake_parts_insert]) 1);
+by (parts_induct_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
 by (fast_tac (!claset addSIs [parts_insertI]
                       addSEs partsEs
                       addEs [Says_imp_old_nonces RS less_irrefl]
                       addss (!simpset)) 1);

 \                   Crypt {|NB, Key K|} (shrK B)|}                 \
 \                   : set_of_list evs";
 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "B_can_trust";
-
-
-B_can_trust RS Spy_not_see_encrypted_key;
+qed "B_trust_OR3";
+
+
+B_trust_OR3 RS Spy_not_see_encrypted_key;
 
 
 (** A session key uniquely identifies a pair of senders in the message
     encrypted by a good agent C.  NEEDED?  INTERESTING?**)
 goal thy 

 \         C ~: lost -->                                             \
 \         Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) --> \
 \         C=A | C=B";
 by (Simp_tac 1);        (*Miniscoping*)
 by (etac otway.induct 1);
-by (dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4);
-by (dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6);
+by analz_Fake_tac;
 (*spy_analz_tac just does not work here: it is an entirely different proof!*)
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
                                       imp_conj_distrib, parts_insert_sees,
                                       parts_insert2])));
 by (REPEAT_FIRST (etac exE));
 (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
-by (excluded_middle_tac "K = newK evsa" 4);
-by (Asm_simp_tac 4);
-by (REPEAT (ares_tac [exI] 4));
+by (expand_case_tac "K = ?y" 4);
+by (REPEAT (ares_tac [exI] 5));
 (*...we prove this case by contradiction: the key is too new!*)
 by (fast_tac (!claset addSEs partsEs
                       addEs [Says_imp_old_keys RS less_irrefl]
                       addss (!simpset)) 4);
 (*Base, Fake, OR2, OR4*)