Simplified new_keys_not_seen, etc.: replaced the
authorpaulson
Tue Nov 05 11:20:52 1996 +0100 (1996-11-05)
changeset 2160ad4382e546fc
parent 2159 e650a3f6f600
child 2161 c25714ca1c19
Simplified new_keys_not_seen, etc.: replaced the
union over all
agents by the Spy alone. Proofs run faster and they do not have to be
set up in terms of a previous lemma.
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Mon Nov 04 17:23:37 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Nov 05 11:20:52 1996 +0100
     1.3 @@ -109,35 +109,23 @@
     1.4  
     1.5  (*** Future keys can't be seen or used! ***)
     1.6  
     1.7 -(*Nobody can have SEEN keys that will be generated in the future.
     1.8 -  This has to be proved anew for each protocol description,
     1.9 -  but should go by similar reasoning every time.  Hardest case is the
    1.10 -  standard Fake rule.  
    1.11 -      The length comparison, and Union over C, are essential for the 
    1.12 -  induction! *)
    1.13 -goal thy "!!evs. evs : ns_shared lost ==> \
    1.14 +(*Nobody can have SEEN keys that will be generated in the future. *)
    1.15 +goal thy "!!evs. evs : ns_shared lost ==>      \
    1.16  \                length evs <= length evs' --> \
    1.17 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    1.18 +\                Key (newK evs') ~: parts (sees lost Spy evs)";
    1.19  by (parts_induct_tac 1);
    1.20  by (ALLGOALS (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.21                                         impOfSubs parts_insert_subset_Un,
    1.22                                         Suc_leD]
    1.23                                  addss (!simpset))));
    1.24 -val lemma = result();
    1.25 -
    1.26 -(*Variant needed for the main theorem below*)
    1.27 -goal thy 
    1.28 - "!!evs. [| evs : ns_shared lost;  length evs <= length evs' |]    \
    1.29 -\        ==> Key (newK evs') ~: parts (sees lost C evs)";
    1.30 -by (fast_tac (!claset addDs [lemma]) 1);
    1.31 -qed "new_keys_not_seen";
    1.32 +qed_spec_mp "new_keys_not_seen";
    1.33  Addsimps [new_keys_not_seen];
    1.34  
    1.35 -(*Another variant: old messages must contain old keys!*)
    1.36 +(*Variant: old messages must contain old keys!*)
    1.37  goal thy 
    1.38   "!!evs. [| Says A B X : set_of_list evs;  \
    1.39  \           Key (newK evt) : parts {X};    \
    1.40 -\           evs : ns_shared lost                 \
    1.41 +\           evs : ns_shared lost           \
    1.42  \        |] ==> length evt < length evs";
    1.43  by (rtac ccontr 1);
    1.44  by (dtac leI 1);
    1.45 @@ -147,38 +135,27 @@
    1.46  
    1.47  
    1.48  
    1.49 -(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
    1.50 +(*** Future nonces can't be seen or used! ***)
    1.51  
    1.52 -goal thy "!!evs. evs : ns_shared lost ==> \
    1.53 +goal thy "!!evs. evs : ns_shared lost ==>     \
    1.54  \                length evs <= length evt --> \
    1.55 -\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
    1.56 -by (etac ns_shared.induct 1);
    1.57 -(*auto_tac does not work here, as it performs safe_tac first*)
    1.58 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    1.59 -                                     addcongs [disj_cong])));
    1.60 -by (REPEAT_FIRST (fast_tac (!claset 
    1.61 -                              addSEs partsEs
    1.62 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.63 -                              addDs  [impOfSubs analz_subset_parts,
    1.64 -                                      impOfSubs parts_insert_subset_Un,
    1.65 -                                      Suc_leD]
    1.66 -                              addss (!simpset))));
    1.67 -val lemma = result();
    1.68 -
    1.69 -(*Variant needed below*)
    1.70 -goal thy 
    1.71 - "!!evs. [| evs : ns_shared lost;  length evs <= length evs' |]    \
    1.72 -\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
    1.73 -by (fast_tac (!claset addDs [lemma]) 1);
    1.74 -qed "new_nonces_not_seen";
    1.75 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    1.76 +by (parts_induct_tac 1);
    1.77 +by (REPEAT_FIRST
    1.78 +    (fast_tac (!claset addSEs partsEs
    1.79 +	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.80 +		       addDs  [impOfSubs analz_subset_parts,
    1.81 +			       impOfSubs parts_insert_subset_Un, Suc_leD]
    1.82 +		       addss (!simpset))));
    1.83 +qed_spec_mp "new_nonces_not_seen";
    1.84  Addsimps [new_nonces_not_seen];
    1.85  
    1.86  
    1.87  (*Nobody can have USED keys that will be generated in the future.
    1.88    ...very like new_keys_not_seen*)
    1.89 -goal thy "!!evs. evs : ns_shared lost ==> \
    1.90 +goal thy "!!evs. evs : ns_shared lost ==>      \
    1.91  \                length evs <= length evs' --> \
    1.92 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    1.93 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    1.94  by (parts_induct_tac 1);
    1.95  (*NS1 and NS2*)
    1.96  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]));
    1.97 @@ -196,13 +173,7 @@
    1.98  by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
    1.99                                    addIs  [less_SucI, impOfSubs keysFor_mono]
   1.100                                    addss (!simpset addsimps [le_def])) 1));
   1.101 -val lemma = result();
   1.102 -
   1.103 -goal thy 
   1.104 - "!!evs. [| evs : ns_shared lost;  length evs <= length evs' |]    \
   1.105 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   1.106 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.107 -qed "new_keys_not_used";
   1.108 +qed_spec_mp "new_keys_not_used";
   1.109  
   1.110  bind_thm ("new_keys_not_analzd",
   1.111            [analz_subset_parts RS keysFor_mono,
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Nov 04 17:23:37 1996 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Nov 05 11:20:52 1996 +0100
     2.3 @@ -131,30 +131,19 @@
     2.4  
     2.5  (*** Future keys can't be seen or used! ***)
     2.6  
     2.7 -(*Nobody can have SEEN keys that will be generated in the future.
     2.8 -  This has to be proved anew for each protocol description,
     2.9 -  but should go by similar reasoning every time.  Hardest case is the
    2.10 -  standard Fake rule.  
    2.11 -      The Union over C is essential for the induction! *)
    2.12 +(*Nobody can have SEEN keys that will be generated in the future. *)
    2.13  goal thy "!!evs. evs : otway lost ==> \
    2.14  \                length evs <= length evs' --> \
    2.15 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    2.16 +\                Key (newK evs') ~: parts (sees lost Spy evs)";
    2.17  by (parts_induct_tac 1);
    2.18  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    2.19                                             impOfSubs parts_insert_subset_Un,
    2.20                                             Suc_leD]
    2.21                                      addss (!simpset))));
    2.22 -val lemma = result();
    2.23 -
    2.24 -(*Variant needed for the main theorem below*)
    2.25 -goal thy 
    2.26 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
    2.27 -\        ==> Key (newK evs') ~: parts (sees lost C evs)";
    2.28 -by (fast_tac (!claset addDs [lemma]) 1);
    2.29 -qed "new_keys_not_seen";
    2.30 +qed_spec_mp "new_keys_not_seen";
    2.31  Addsimps [new_keys_not_seen];
    2.32  
    2.33 -(*Another variant: old messages must contain old keys!*)
    2.34 +(*Variant: old messages must contain old keys!*)
    2.35  goal thy 
    2.36   "!!evs. [| Says A B X : set_of_list evs;  \
    2.37  \           Key (newK evt) : parts {X};    \
    2.38 @@ -167,15 +156,12 @@
    2.39  qed "Says_imp_old_keys";
    2.40  
    2.41  
    2.42 -(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
    2.43 +(*** Future nonces can't be seen or used! ***)
    2.44  
    2.45  goal thy "!!evs. evs : otway lost ==> \
    2.46  \                length evs <= length evt --> \
    2.47 -\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
    2.48 -by (etac otway.induct 1);
    2.49 -(*auto_tac does not work here, as it performs safe_tac first*)
    2.50 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    2.51 -                                     addcongs [disj_cong])));
    2.52 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    2.53 +by (parts_induct_tac 1);
    2.54  by (REPEAT_FIRST (fast_tac (!claset 
    2.55                                addSEs partsEs
    2.56                                addSDs  [Says_imp_sees_Spy RS parts.Inj]
    2.57 @@ -183,22 +169,14 @@
    2.58                                        impOfSubs parts_insert_subset_Un,
    2.59                                        Suc_leD]
    2.60                                addss (!simpset))));
    2.61 -val lemma = result();
    2.62 -
    2.63 -(*Variant needed for the main theorem below*)
    2.64 -goal thy 
    2.65 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
    2.66 -\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
    2.67 -by (fast_tac (!claset addDs [lemma]) 1);
    2.68 -qed "new_nonces_not_seen";
    2.69 +qed_spec_mp "new_nonces_not_seen";
    2.70  Addsimps [new_nonces_not_seen];
    2.71  
    2.72 -(*Another variant: old messages must contain old nonces!*)
    2.73 -goal thy 
    2.74 - "!!evs. [| Says A B X : set_of_list evs;  \
    2.75 -\           Nonce (newN evt) : parts {X};    \
    2.76 -\           evs : otway lost                 \
    2.77 -\        |] ==> length evt < length evs";
    2.78 +(*Variant: old messages must contain old nonces!*)
    2.79 +goal thy "!!evs. [| Says A B X : set_of_list evs;    \
    2.80 +\                   Nonce (newN evt) : parts {X};    \
    2.81 +\                   evs : otway lost                 \
    2.82 +\                |] ==> length evt < length evs";
    2.83  by (rtac ccontr 1);
    2.84  by (dtac leI 1);
    2.85  by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
    2.86 @@ -208,9 +186,9 @@
    2.87  
    2.88  (*Nobody can have USED keys that will be generated in the future.
    2.89    ...very like new_keys_not_seen*)
    2.90 -goal thy "!!evs. evs : otway lost ==> \
    2.91 +goal thy "!!evs. evs : otway lost ==>          \
    2.92  \                length evs <= length evs' --> \
    2.93 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    2.94 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    2.95  by (parts_induct_tac 1);
    2.96  (*OR1 and OR3*)
    2.97  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    2.98 @@ -222,13 +200,7 @@
    2.99                        Suc_leD]
   2.100                 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   2.101                 addss (!simpset)) 1));
   2.102 -val lemma = result();
   2.103 -
   2.104 -goal thy 
   2.105 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   2.106 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   2.107 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   2.108 -qed "new_keys_not_used";
   2.109 +qed_spec_mp "new_keys_not_used";
   2.110  
   2.111  bind_thm ("new_keys_not_analzd",
   2.112            [analz_subset_parts RS keysFor_mono,
   2.113 @@ -283,12 +255,11 @@
   2.114  by (etac otway.induct 1);
   2.115  by analz_Fake_tac;
   2.116  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   2.117 -by (ALLGOALS (*Takes 22 secs*)
   2.118 +by (ALLGOALS (*Takes 14 secs*)
   2.119      (asm_simp_tac 
   2.120       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   2.121                           @ pushes)
   2.122                 setloop split_tac [expand_if])));
   2.123 -(** LEVEL 5 **)
   2.124  (*OR4, OR2, Fake*) 
   2.125  by (EVERY (map spy_analz_tac [5,3,2]));
   2.126  (*Oops, OR3, Base*)
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Nov 04 17:23:37 1996 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Nov 05 11:20:52 1996 +0100
     3.3 @@ -119,30 +119,19 @@
     3.4  
     3.5  (*** Future keys can't be seen or used! ***)
     3.6  
     3.7 -(*Nobody can have SEEN keys that will be generated in the future.
     3.8 -  This has to be proved anew for each protocol description,
     3.9 -  but should go by similar reasoning every time.  Hardest case is the
    3.10 -  standard Fake rule.  
    3.11 -      The Union over C is essential for the induction! *)
    3.12 +(*Nobody can have SEEN keys that will be generated in the future. *)
    3.13  goal thy "!!evs. evs : otway lost ==> \
    3.14  \                length evs <= length evs' --> \
    3.15 -\                Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    3.16 +\                Key (newK evs') ~: parts (sees lost Spy evs)";
    3.17  by (parts_induct_tac 1);
    3.18  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    3.19                                             impOfSubs parts_insert_subset_Un,
    3.20                                             Suc_leD]
    3.21                                      addss (!simpset))));
    3.22 -val lemma = result();
    3.23 -
    3.24 -(*Variant needed for the main theorem below*)
    3.25 -goal thy 
    3.26 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
    3.27 -\        ==> Key (newK evs') ~: parts (sees lost C evs)";
    3.28 -by (fast_tac (!claset addDs [lemma]) 1);
    3.29 -qed "new_keys_not_seen";
    3.30 +qed_spec_mp "new_keys_not_seen";
    3.31  Addsimps [new_keys_not_seen];
    3.32  
    3.33 -(*Another variant: old messages must contain old keys!*)
    3.34 +(*Variant: old messages must contain old keys!*)
    3.35  goal thy 
    3.36   "!!evs. [| Says A B X : set_of_list evs;  \
    3.37  \           Key (newK evt) : parts {X};    \
    3.38 @@ -155,15 +144,12 @@
    3.39  qed "Says_imp_old_keys";
    3.40  
    3.41  
    3.42 -(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
    3.43 +(*** Future nonces can't be seen or used! ***)
    3.44  
    3.45  goal thy "!!evs. evs : otway lost ==> \
    3.46  \                length evs <= length evt --> \
    3.47 -\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
    3.48 -by (etac otway.induct 1);
    3.49 -(*auto_tac does not work here, as it performs safe_tac first*)
    3.50 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    3.51 -                                     addcongs [disj_cong])));
    3.52 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    3.53 +by (parts_induct_tac 1);
    3.54  by (REPEAT_FIRST (fast_tac (!claset 
    3.55                                addSEs partsEs
    3.56                                addSDs  [Says_imp_sees_Spy RS parts.Inj]
    3.57 @@ -171,14 +157,7 @@
    3.58                                        impOfSubs parts_insert_subset_Un,
    3.59                                        Suc_leD]
    3.60                                addss (!simpset))));
    3.61 -val lemma = result();
    3.62 -
    3.63 -(*Variant needed for the main theorem below*)
    3.64 -goal thy 
    3.65 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
    3.66 -\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
    3.67 -by (fast_tac (!claset addDs [lemma]) 1);
    3.68 -qed "new_nonces_not_seen";
    3.69 +qed_spec_mp "new_nonces_not_seen";
    3.70  Addsimps [new_nonces_not_seen];
    3.71  
    3.72  
    3.73 @@ -186,7 +165,7 @@
    3.74    ...very like new_keys_not_seen*)
    3.75  goal thy "!!evs. evs : otway lost ==> \
    3.76  \                length evs <= length evs' --> \
    3.77 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    3.78 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    3.79  by (parts_induct_tac 1);
    3.80  (*OR1 and OR3*)
    3.81  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    3.82 @@ -198,13 +177,7 @@
    3.83                        Suc_leD]
    3.84                 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
    3.85                 addss (!simpset)) 1));
    3.86 -val lemma = result();
    3.87 -
    3.88 -goal thy 
    3.89 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
    3.90 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
    3.91 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
    3.92 -qed "new_keys_not_used";
    3.93 +qed_spec_mp "new_keys_not_used";
    3.94  
    3.95  bind_thm ("new_keys_not_analzd",
    3.96            [analz_subset_parts RS keysFor_mono,
     4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Nov 04 17:23:37 1996 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Nov 05 11:20:52 1996 +0100
     4.3 @@ -131,30 +131,19 @@
     4.4  
     4.5  (*** Future keys can't be seen or used! ***)
     4.6  
     4.7 -(*Nobody can have SEEN keys that will be generated in the future.
     4.8 -  This has to be proved anew for each protocol description,
     4.9 -  but should go by similar reasoning every time.  Hardest case is the
    4.10 -  standard Fake rule.  
    4.11 -      The Union over C is essential for the induction! *)
    4.12 -goal thy "!!evs. evs : otway ==> \
    4.13 +(*Nobody can have SEEN keys that will be generated in the future. *)
    4.14 +goal thy "!!evs. evs : otway ==>               \
    4.15  \                length evs <= length evs' --> \
    4.16 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    4.17 +\                Key (newK evs') ~: parts (sees lost Spy evs)";
    4.18  by (parts_induct_tac 1);
    4.19  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    4.20 -                                       impOfSubs parts_insert_subset_Un,
    4.21 -                                       Suc_leD]
    4.22 +					   impOfSubs parts_insert_subset_Un,
    4.23 +					   Suc_leD]
    4.24                                  addss (!simpset))));
    4.25 -val lemma = result();
    4.26 -
    4.27 -(*Variant needed for the main theorem below*)
    4.28 -goal thy 
    4.29 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
    4.30 -\        ==> Key (newK evs') ~: parts (sees lost C evs)";
    4.31 -by (fast_tac (!claset addDs [lemma]) 1);
    4.32 -qed "new_keys_not_seen";
    4.33 +qed_spec_mp "new_keys_not_seen";
    4.34  Addsimps [new_keys_not_seen];
    4.35  
    4.36 -(*Another variant: old messages must contain old keys!*)
    4.37 +(*Variant: old messages must contain old keys!*)
    4.38  goal thy 
    4.39   "!!evs. [| Says A B X : set_of_list evs;  \
    4.40  \           Key (newK evt) : parts {X};    \
    4.41 @@ -167,35 +156,24 @@
    4.42  qed "Says_imp_old_keys";
    4.43  
    4.44  
    4.45 -(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
    4.46 +(*** Future nonces can't be seen or used! ***)
    4.47  
    4.48  goal thy "!!evs. evs : otway ==> \
    4.49  \                length evs <= length evs' --> \
    4.50 -\                      Nonce (newN evs') ~: (UN C. parts (sees lost C evs))";
    4.51 -by (etac otway.induct 1);
    4.52 -(*auto_tac does not work here, as it performs safe_tac first*)
    4.53 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    4.54 -                                     addcongs [disj_cong])));
    4.55 -by (REPEAT_FIRST (fast_tac (!claset 
    4.56 -                              addSEs partsEs
    4.57 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
    4.58 -                              addDs  [impOfSubs analz_subset_parts,
    4.59 -                                      impOfSubs parts_insert_subset_Un,
    4.60 -                                      Suc_leD]
    4.61 -                              addss (!simpset))));
    4.62 -val lemma = result();
    4.63 -
    4.64 -(*Variant needed for the main theorem below*)
    4.65 -goal thy 
    4.66 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
    4.67 -\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
    4.68 -by (fast_tac (!claset addDs [lemma]) 1);
    4.69 -qed "new_nonces_not_seen";
    4.70 +\                Nonce (newN evs') ~: parts (sees lost Spy evs)";
    4.71 +by (parts_induct_tac 1);
    4.72 +by (REPEAT_FIRST
    4.73 +    (fast_tac (!claset addSEs partsEs
    4.74 +	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
    4.75 +		       addDs  [impOfSubs analz_subset_parts,
    4.76 +			       impOfSubs parts_insert_subset_Un, Suc_leD]
    4.77 +		       addss (!simpset))));
    4.78 +qed_spec_mp "new_nonces_not_seen";
    4.79  Addsimps [new_nonces_not_seen];
    4.80  
    4.81 -(*Another variant: old messages must contain old nonces!*)
    4.82 +(*Variant: old messages must contain old nonces!*)
    4.83  goal thy 
    4.84 - "!!evs. [| Says A B X : set_of_list evs;  \
    4.85 + "!!evs. [| Says A B X : set_of_list evs;    \
    4.86  \           Nonce (newN evt) : parts {X};    \
    4.87  \           evs : otway                 \
    4.88  \        |] ==> length evt < length evs";
    4.89 @@ -210,7 +188,7 @@
    4.90    ...very like new_keys_not_seen*)
    4.91  goal thy "!!evs. evs : otway ==> \
    4.92  \                length evs <= length evs' --> \
    4.93 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    4.94 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    4.95  by (parts_induct_tac 1);
    4.96  (*OR1 and OR3*)
    4.97  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    4.98 @@ -222,13 +200,7 @@
    4.99                        Suc_leD]
   4.100                 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   4.101                 addss (!simpset)) 1));
   4.102 -val lemma = result();
   4.103 -
   4.104 -goal thy 
   4.105 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   4.106 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   4.107 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   4.108 -qed "new_keys_not_used";
   4.109 +qed_spec_mp "new_keys_not_used";
   4.110  
   4.111  bind_thm ("new_keys_not_analzd",
   4.112            [analz_subset_parts RS keysFor_mono,
     5.1 --- a/src/HOL/Auth/Shared.ML	Mon Nov 04 17:23:37 1996 +0100
     5.2 +++ b/src/HOL/Auth/Shared.ML	Tue Nov 05 11:20:52 1996 +0100
     5.3 @@ -155,7 +155,7 @@
     5.4  qed "sees_subset_sees_Says";
     5.5  
     5.6  (*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
     5.7 -  Used to prove new_keys_not_seen.*)
     5.8 +  Once used to prove new_keys_not_seen; now obsolete.*)
     5.9  goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
    5.10  \         parts {Y} Un (UN A. parts (sees lost A evs))";
    5.11  by (Step_tac 1);
    5.12 @@ -202,7 +202,7 @@
    5.13  by (ALLGOALS Fast_tac);
    5.14  qed_spec_mp "seesD";
    5.15  
    5.16 -Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy];
    5.17 +Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
    5.18  Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
    5.19  
    5.20  
     6.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Nov 04 17:23:37 1996 +0100
     6.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Nov 05 11:20:52 1996 +0100
     6.3 @@ -118,30 +118,19 @@
     6.4  
     6.5  (*** Future keys can't be seen or used! ***)
     6.6  
     6.7 -(*Nobody can have SEEN keys that will be generated in the future.
     6.8 -  This has to be proved anew for each protocol description,
     6.9 -  but should go by similar reasoning every time.  Hardest case is the
    6.10 -  standard Fake rule.  
    6.11 -      The Union over C is essential for the induction! *)
    6.12 +(*Nobody can have SEEN keys that will be generated in the future. *)
    6.13  goal thy "!!evs. evs : yahalom lost ==> \
    6.14  \                length evs <= length evs' --> \
    6.15 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    6.16 +\                Key (newK evs') ~: parts (sees lost Spy evs)";
    6.17  by (parts_induct_tac 1);
    6.18  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    6.19                                             impOfSubs parts_insert_subset_Un,
    6.20                                             Suc_leD]
    6.21                                      addss (!simpset))));
    6.22 -val lemma = result();
    6.23 -
    6.24 -(*Variant needed for the main theorem below*)
    6.25 -goal thy 
    6.26 - "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
    6.27 -\        ==> Key (newK evs') ~: parts (sees lost C evs)";
    6.28 -by (fast_tac (!claset addDs [lemma]) 1);
    6.29 -qed "new_keys_not_seen";
    6.30 +qed_spec_mp "new_keys_not_seen";
    6.31  Addsimps [new_keys_not_seen];
    6.32  
    6.33 -(*Another variant: old messages must contain old keys!*)
    6.34 +(*Variant: old messages must contain old keys!*)
    6.35  goal thy 
    6.36   "!!evs. [| Says A B X : set_of_list evs;  \
    6.37  \           Key (newK evt) : parts {X};    \
    6.38 @@ -168,31 +157,25 @@
    6.39    ...very like new_keys_not_seen*)
    6.40  goal thy "!!evs. evs : yahalom lost ==> \
    6.41  \                length evs <= length evs' --> \
    6.42 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    6.43 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    6.44  by (parts_induct_tac 1);
    6.45 -by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
    6.46  (*YM1, YM2 and YM3*)
    6.47  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
    6.48 -(*Fake and YM4: these messages send unknown (X) components*)
    6.49 -by (stac insert_commute 2);
    6.50 -by (Simp_tac 2);
    6.51 -(*YM4: the only way K could have been used is if it had been seen,
    6.52 -  contradicting new_keys_not_seen*)
    6.53 -by (REPEAT
    6.54 -     (best_tac
    6.55 -      (!claset addDs [impOfSubs analz_subset_parts,
    6.56 -                      impOfSubs (analz_subset_parts RS keysFor_mono),
    6.57 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    6.58 -                      Suc_leD]
    6.59 +(*Fake and Oops: these messages send unknown (X) components*)
    6.60 +by (EVERY
    6.61 +    (map (fast_tac
    6.62 +	  (!claset addDs [impOfSubs analz_subset_parts,
    6.63 +			  impOfSubs (analz_subset_parts RS keysFor_mono),
    6.64 +			  impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    6.65 +			  Suc_leD]
    6.66 +                   addss (!simpset))) [3,1]));
    6.67 +(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
    6.68 +by (fast_tac
    6.69 +      (!claset addSEs partsEs
    6.70 +               addSDs [Says_imp_sees_Spy RS parts.Inj]
    6.71                 addEs [new_keys_not_seen RSN(2,rev_notE)]
    6.72 -               addss (!simpset)) 1));
    6.73 -val lemma = result();
    6.74 -
    6.75 -goal thy 
    6.76 - "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
    6.77 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
    6.78 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
    6.79 -qed "new_keys_not_used";
    6.80 +               addDs [Suc_leD]) 1);
    6.81 +qed_spec_mp "new_keys_not_used";
    6.82  
    6.83  bind_thm ("new_keys_not_analzd",
    6.84            [analz_subset_parts RS keysFor_mono,
    6.85 @@ -413,31 +396,22 @@
    6.86  
    6.87  goal thy "!!evs. evs : yahalom lost ==> \
    6.88  \                length evs <= length evt --> \
    6.89 -\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
    6.90 -by (etac yahalom.induct 1);
    6.91 -(*auto_tac does not work here, as it performs safe_tac first*)
    6.92 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    6.93 -                                     addcongs [disj_cong])));
    6.94 -by (REPEAT_FIRST
    6.95 -    (fast_tac (!claset addSEs partsEs
    6.96 -	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
    6.97 -		       addDs  [impOfSubs analz_subset_parts,
    6.98 -			       impOfSubs parts_insert_subset_Un, Suc_leD]
    6.99 -		       addss (!simpset))));
   6.100 -val lemma = result();
   6.101 -
   6.102 -(*Variant needed for the main theorem below*)
   6.103 -goal thy 
   6.104 - "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   6.105 -\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
   6.106 -by (fast_tac (!claset addDs [lemma]) 1);
   6.107 -qed "new_nonces_not_seen";
   6.108 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   6.109 +by (parts_induct_tac 1);
   6.110 +by (REPEAT_FIRST (fast_tac (!claset 
   6.111 +                              addSEs partsEs
   6.112 +                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
   6.113 +                              addDs  [impOfSubs analz_subset_parts,
   6.114 +                                      impOfSubs parts_insert_subset_Un,
   6.115 +                                      Suc_leD]
   6.116 +                              addss (!simpset))));
   6.117 +qed_spec_mp "new_nonces_not_seen";
   6.118  Addsimps [new_nonces_not_seen];
   6.119  
   6.120 -(*Another variant: old messages must contain old nonces!*)
   6.121 +(*Variant: old messages must contain old nonces!*)
   6.122  goal thy 
   6.123 - "!!evs. [| Says A B X : set_of_list evs;  \
   6.124 -\           Nonce (newN evt) : parts {X};    \
   6.125 + "!!evs. [| Says A B X : set_of_list evs;      \
   6.126 +\           Nonce (newN evt) : parts {X};      \
   6.127  \           evs : yahalom lost                 \
   6.128  \        |] ==> length evt < length evs";
   6.129  by (rtac ccontr 1);
     7.1 --- a/src/HOL/Auth/Yahalom2.ML	Mon Nov 04 17:23:37 1996 +0100
     7.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Nov 05 11:20:52 1996 +0100
     7.3 @@ -126,30 +126,19 @@
     7.4  
     7.5  (*** Future keys can't be seen or used! ***)
     7.6  
     7.7 -(*Nobody can have SEEN keys that will be generated in the future.
     7.8 -  This has to be proved anew for each protocol description,
     7.9 -  but should go by similar reasoning every time.  Hardest case is the
    7.10 -  standard Fake rule.  
    7.11 -      The Union over C is essential for the induction! *)
    7.12 +(*Nobody can have SEEN keys that will be generated in the future. *)
    7.13  goal thy "!!evs. evs : yahalom lost ==> \
    7.14  \                length evs <= length evs' --> \
    7.15 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    7.16 +\                Key (newK evs') ~: parts (sees lost Spy evs)";
    7.17  by (parts_induct_tac 1);
    7.18  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    7.19                                             impOfSubs parts_insert_subset_Un,
    7.20                                             Suc_leD]
    7.21                                      addss (!simpset))));
    7.22 -val lemma = result();
    7.23 -
    7.24 -(*Variant needed for the main theorem below*)
    7.25 -goal thy 
    7.26 - "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
    7.27 -\        ==> Key (newK evs') ~: parts (sees lost C evs)";
    7.28 -by (fast_tac (!claset addDs [lemma]) 1);
    7.29 -qed "new_keys_not_seen";
    7.30 +qed_spec_mp "new_keys_not_seen";
    7.31  Addsimps [new_keys_not_seen];
    7.32  
    7.33 -(*Another variant: old messages must contain old keys!*)
    7.34 +(*Variant: old messages must contain old keys!*)
    7.35  goal thy 
    7.36   "!!evs. [| Says A B X : set_of_list evs;  \
    7.37  \           Key (newK evt) : parts {X};    \
    7.38 @@ -166,31 +155,26 @@
    7.39    ...very like new_keys_not_seen*)
    7.40  goal thy "!!evs. evs : yahalom lost ==> \
    7.41  \                length evs <= length evs' --> \
    7.42 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    7.43 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    7.44  by (parts_induct_tac 1);
    7.45  by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
    7.46  (*YM1, YM2 and YM3*)
    7.47  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
    7.48 -(*Fake and YM4: these messages send unknown (X) components*)
    7.49 -by (stac insert_commute 2);
    7.50 -by (Simp_tac 2);
    7.51 -(*YM4: the only way K could have been used is if it had been seen,
    7.52 -  contradicting new_keys_not_seen*)
    7.53 -by (REPEAT
    7.54 -     (best_tac
    7.55 -      (!claset addDs [impOfSubs analz_subset_parts,
    7.56 -                      impOfSubs (analz_subset_parts RS keysFor_mono),
    7.57 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    7.58 -                      Suc_leD]
    7.59 +(*Fake and Oops: these messages send unknown (X) components*)
    7.60 +by (EVERY
    7.61 +    (map (fast_tac
    7.62 +	  (!claset addDs [impOfSubs analz_subset_parts,
    7.63 +			  impOfSubs (analz_subset_parts RS keysFor_mono),
    7.64 +			  impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    7.65 +			  Suc_leD]
    7.66 +                   addss (!simpset))) [3,1]));
    7.67 +(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
    7.68 +by (fast_tac
    7.69 +      (!claset addSEs partsEs
    7.70 +               addSDs [Says_imp_sees_Spy RS parts.Inj]
    7.71                 addEs [new_keys_not_seen RSN(2,rev_notE)]
    7.72 -               addss (!simpset)) 1));
    7.73 -val lemma = result();
    7.74 -
    7.75 -goal thy 
    7.76 - "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
    7.77 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
    7.78 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
    7.79 -qed "new_keys_not_used";
    7.80 +               addDs [Suc_leD]) 1);
    7.81 +qed_spec_mp "new_keys_not_used";
    7.82  
    7.83  bind_thm ("new_keys_not_analzd",
    7.84            [analz_subset_parts RS keysFor_mono,