src/HOL/Auth/Recur.ML

 	ONE theorem would be more elegant and faster!
 	By induction on a list of agents (no repetitions)
 **)
 
 (*Simplest case: Alice goes directly to the server*)
-goal thy 
+goal thy
  "!!A. A ~= Server   \
 \ ==> EX K NA. EX evs: recur lost.          \
 \     Says Server A {|Agent A,              \
 \                     Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
 \                       Agent Server|}      \
 \         : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (recur.Nil RS recur.RA1 RS 
 	  (respond.One RSN (4,recur.RA3))) 2);
-by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]));
+by (REPEAT
+    (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
+     THEN
+     REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])));
 result();
 
 
 (*Case two: Alice, Bob and the server*)
-goal thy 
+goal thy
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \ ==> EX K. EX NA. EX evs: recur lost.          \
 \       Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
 \                       Agent Server|}                          \
 \         : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
 	  (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
 	  recur.RA4) 2);
+bw HPair_def;
 by (REPEAT
     (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
      THEN
      ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
 result();
 
 
 (*Case three: Alice, Bob, Charlie and the server*)
-goal thy 
+goal thy
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \ ==> EX K. EX NA. EX evs: recur lost.          \
 \       Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
 \                       Agent Server|}                          \
 \         : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
 	  (respond.One RS respond.Cons RS respond.Cons RSN
 	   (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
+bw HPair_def;
 by (REPEAT	(*SLOW: 37 seconds*)
     (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
      THEN
      ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
 by (ALLGOALS 

     dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
     forward_tac [respond_imp_responses] 5                THEN
     dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
 
 
+Delsimps [image_insert];
+
 (** Session keys are not used to encrypt other session keys **)
 
 (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
   Note that it holds for *any* set H (not just "sees lost Spy evs")
   satisfying the inductive hypothesis.*)

 goal thy  
  "!!evs. evs : recur lost ==>                                            \
 \  ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \
 \           (K : newK``I | Key K : analz (sees lost Spy evs))";
 by (etac recur.induct 1);
+be subst 4;	(*RA2: DELETE needless definition of PA!*)
 by analz_Fake_tac;
-be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
 (*Base*)
 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
 (*RA4, RA2, Fake*) 

 goal thy "!!i. evs : recur lost ==>              \
 \                length evs <= i -->             \
 \                (Nonce (newN i) : parts {X} --> \
 \                 Hash X ~: parts (sees lost Spy evs))";
 be recur.induct 1;
-be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
+be subst 4;	(*RA2: DELETE needless definition of PA!*)
 by parts_Fake_tac;
 (*RA3 requires a further induction*)
 be responses.induct 5;
 by (ALLGOALS Asm_simp_tac);
 (*RA2*)

  "!!evs. [| evs : recur lost; A ~: lost |]               \
 \ ==> EX B' P'. ALL B P.    \
 \        Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
 \          : parts (sees lost Spy evs)  -->  B=B' & P=P'";
 be recur.induct 1;
-be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
+be subst 4;	(*RA2: DELETE needless definition of PA!*)
 (*For better simplification of RA2*)
 by (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 4);
 by parts_Fake_tac;
 (*RA3 requires a further induction*)
 be responses.induct 5;

 (*Fake*)
 by (best_tac (!claset addSIs [exI]
                       addDs [impOfSubs analz_subset_parts,
 			     impOfSubs Fake_parts_insert]
 		      addss (!simpset)) 2);
-(*Base*)
+(*Base*) (** LEVEL 9 **)
 by (fast_tac (!claset addss (!simpset)) 1);
-
 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
 (*RA1: creation of new Nonce.  Move assertion into global context*)
 by (expand_case_tac "NA = ?y" 1);
 by (best_tac (!claset addSIs [exI]
                       addEs  [Hash_new_nonces_not_seen]

 		      addEs  [Hash_new_nonces_not_seen]
 		      addss  (!simpset)) 1);
 by (best_tac (!claset addss  (!simpset)) 1);
 val lemma = result();
 
-goal thy 
- "!!evs.[| Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|}   \
+goalw thy [HPair_def]
+ "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|}   \
 \            : parts (sees lost Spy evs);                        \
-\          Hash {|Key(shrK A), Agent A, Agent B', Nonce NA, P'|} \
+\          HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \
 \            : parts (sees lost Spy evs);                        \
 \          evs : recur lost;  A ~: lost |]                      \
 \        ==> B=B' & P=P'";
+by (REPEAT (eresolve_tac partsEs 1));
 by (prove_unique_tac lemma 1);
 qed "unique_NA";
 
 
 (*** Lemmas concerning the Server's response
       (relations "respond" and "responses") 
 ***)
-
-(*The response never contains Hashes*)
-(*NEEDED????????????????*)
-goal thy
- "!!evs. (j,PB,RB) : respond i \
-\        ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
-\            Hash {|Key (shrK B), M|} : parts H";
-be (respond_imp_responses RS responses.induct) 1;
-by (Auto_tac());
-bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
-
 
 goal thy
  "!!evs. [| RB : responses i;  evs : recur lost |] \
 \ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
 be responses.induct 1;

 goal thy 
  "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};    \
 \          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
 \          (j,PB,RB) : respond i |]               \
 \ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
-by (prove_unique_tac lemma 1);	(*33 seconds, due to the disjunctions*)
+by (prove_unique_tac lemma 1);	(*50 seconds??, due to the disjunctions*)
 qed "unique_session_keys";
 
 
 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3
     Does not in itself guarantee security: an attack could violate 
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!j. (j, {|Hash {|Key(shrK A), Agent A, B, NA, P|}, X|}, RA) : respond i \
+ "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \
 \ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}";
 be respond.elim 1;
 by (ALLGOALS Asm_full_simp_tac);
 qed "newK2_respond_lemma";
 

 \        ==> ALL A A' N. A ~: lost & A' ~: lost -->  \
 \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
 \            Key K ~: analz (insert RB (sees lost Spy evs))";
 be respond.induct 1;
 by (forward_tac [respond_imp_responses] 2);
-by (ALLGOALS
+by (ALLGOALS (*4 MINUTES???*)
     (asm_simp_tac 
      (!simpset addsimps 
 	  ([analz_image_newK, not_parts_not_analz,
 	    read_instantiate [("H", "?ff``?xx")] parts_insert,
 	    Un_assoc RS sym, resp_analz_image_newK,

  "!!evs. [| A ~: lost;  A' ~: lost;  evs : recur lost |]            \
 \        ==> Says Server B RB : set_of_list evs -->                 \
 \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac recur.induct 1);
+be subst 4;	(*RA2: DELETE needless definition of PA!*)
 by analz_Fake_tac;
-be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
 by (ALLGOALS
     (asm_simp_tac
      (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] 
                setloop split_tac [expand_if])));
 (*RA4*)

 qed "Agent_not_see_encrypted_key";
 
 
 (**** Authenticity properties for Agents ****)
 
+(*The response never contains Hashes*)
+(*NEEDED????????????????*)
+goal thy
+ "!!evs. (j,PB,RB) : respond i \
+\        ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
+\            Hash {|Key (shrK B), M|} : parts H";
+be (respond_imp_responses RS responses.induct) 1;
+by (Auto_tac());
+bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
+
 (*NEEDED????????????????*)
 (*Only RA1 or RA2 can have caused such a part of a message to appear.*)
-goal thy 
+goalw thy [HPair_def]
  "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
 \             : parts (sees lost Spy evs);                        \
 \            A ~: lost;  evs : recur lost |]                        \
-\        ==> Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|},  \
-\                       Agent A, Agent B, NA, P|}  \
+\        ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|})  \
 \             : set_of_list evs";
 be rev_mp 1;
 by (parts_induct_tac 1);
 (*RA3*)
 by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 2);

     (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1));
 by (best_tac (!claset addSEs partsEs 
                       addDs [parts_cut]
                       addss  (!simpset)) 1);
 qed_spec_mp "Hash_auth_sender";
-
-
-(*NEEDED????????????????*)
-goal thy "!!i. {|Hash {|Key (shrK Server), M|}, M|} : responses i ==> R";
-be setup_induction 1;
-be responses.induct 1;
-by (ALLGOALS Asm_simp_tac); 
-qed "responses_no_Hash_Server";
 
 
 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);