updating both Yahalom protocols to the Gets model
authorpaulson
Wed Mar 10 10:42:57 1999 +0100 (1999-03-10)
changeset 63357e4bffaa2a3e
parent 6334 e53457213857
child 6336 f523a7c91c37
updating both Yahalom protocols to the Gets model
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Mar 10 10:42:40 1999 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Mar 10 10:42:57 1999 +0100
     1.3 @@ -18,11 +18,28 @@
     1.4  \     ==> EX X NB K. EX evs: yahalom.          \
     1.5  \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
     1.6  by (REPEAT (resolve_tac [exI,bexI] 1));
     1.7 -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
     1.8 -          yahalom.YM4) 2);
     1.9 +by (rtac (yahalom.Nil RS 
    1.10 +          yahalom.YM1 RS yahalom.Reception RS
    1.11 +          yahalom.YM2 RS yahalom.Reception RS 
    1.12 +          yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
    1.13  by possibility_tac;
    1.14  result();
    1.15  
    1.16 +Goal "[| Gets B X : set evs; evs : yahalom |] ==> EX A. Says A B X : set evs";
    1.17 +by (etac rev_mp 1);
    1.18 +by (etac yahalom.induct 1);
    1.19 +by Auto_tac;
    1.20 +qed "Gets_imp_Says";
    1.21 +
    1.22 +(*Must be proved separately for each protocol*)
    1.23 +Goal "[| Gets B X : set evs; evs : yahalom |]  ==> X : knows Spy evs";
    1.24 +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    1.25 +qed"Gets_imp_knows_Spy";
    1.26 +AddDs [Gets_imp_knows_Spy RS parts.Inj];
    1.27 +
    1.28 +fun g_not_bad_tac s = 
    1.29 +  forward_tac [Gets_imp_Says] THEN' assume_tac THEN' not_bad_tac s;
    1.30 +
    1.31  
    1.32  (**** Inductive proofs about yahalom ****)
    1.33  
    1.34 @@ -30,49 +47,50 @@
    1.35  (** For reasoning about the encrypted portion of messages **)
    1.36  
    1.37  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.38 -Goal "Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
    1.39 -\             X : analz (spies evs)";
    1.40 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.41 -qed "YM4_analz_spies";
    1.42 +Goal "[| Gets A {|Crypt (shrK A) Y, X|} : set evs;  evs : yahalom |]  \
    1.43 +\     ==> X : analz (knows Spy evs)";
    1.44 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    1.45 +qed "YM4_analz_knows_Spy";
    1.46  
    1.47 -bind_thm ("YM4_parts_spies",
    1.48 -          YM4_analz_spies RS (impOfSubs analz_subset_parts));
    1.49 +bind_thm ("YM4_parts_knows_Spy",
    1.50 +          YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    1.51  
    1.52 -(*Relates to both YM4 and Oops*)
    1.53 -Goal "Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
    1.54 -\             K : parts (spies evs)";
    1.55 +(*For Oops*)
    1.56 +Goal "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs \
    1.57 +\     ==> K : parts (knows Spy evs)";
    1.58  by (blast_tac (claset() addSEs partsEs
    1.59 -                        addSDs [Says_imp_spies RS parts.Inj]) 1);
    1.60 -qed "YM4_Key_parts_spies";
    1.61 +                        addSDs [Says_imp_knows_Spy RS parts.Inj]) 1);
    1.62 +qed "YM4_Key_parts_knows_Spy";
    1.63  
    1.64 -(*For proving the easier theorems about X ~: parts (spies evs).*)
    1.65 -fun parts_spies_tac i = 
    1.66 -    forward_tac [YM4_Key_parts_spies] (i+6) THEN
    1.67 -    forward_tac [YM4_parts_spies] (i+5)     THEN
    1.68 -    prove_simple_subgoals_tac  i;
    1.69 +(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    1.70 +fun parts_knows_Spy_tac i = 
    1.71 +  EVERY
    1.72 +   [forward_tac [YM4_Key_parts_knows_Spy] (i+7),
    1.73 +    forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6),
    1.74 +    prove_simple_subgoals_tac i];
    1.75  
    1.76  (*Induction for regularity theorems.  If induction formula has the form
    1.77 -   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    1.78 -   needless information about analz (insert X (spies evs))  *)
    1.79 +   X ~: analz (knows Spy evs) --> ... then it shortens the proof by discarding
    1.80 +   needless information about analz (insert X (knows Spy evs))  *)
    1.81  fun parts_induct_tac i = 
    1.82      etac yahalom.induct i
    1.83      THEN 
    1.84      REPEAT (FIRSTGOAL analz_mono_contra_tac)
    1.85 -    THEN  parts_spies_tac i;
    1.86 +    THEN  parts_knows_Spy_tac i;
    1.87  
    1.88  
    1.89 -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.90 +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    1.91      sends messages containing X! **)
    1.92  
    1.93  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.94 -Goal "evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.95 +Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
    1.96  by (parts_induct_tac 1);
    1.97  by (Fake_parts_insert_tac 1);
    1.98  by (ALLGOALS Blast_tac);
    1.99  qed "Spy_see_shrK";
   1.100  Addsimps [Spy_see_shrK];
   1.101  
   1.102 -Goal "evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   1.103 +Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
   1.104  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   1.105  qed "Spy_analz_shrK";
   1.106  Addsimps [Spy_analz_shrK];
   1.107 @@ -83,12 +101,12 @@
   1.108  
   1.109  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   1.110  Goal "evs : yahalom ==>          \
   1.111 -\      Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   1.112 +\      Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
   1.113  by (parts_induct_tac 1);
   1.114  (*Fake*)
   1.115  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   1.116  (*YM2-4: Because Key K is not fresh, etc.*)
   1.117 -by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
   1.118 +by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
   1.119  qed_spec_mp "new_keys_not_used";
   1.120  
   1.121  bind_thm ("new_keys_not_analzd",
   1.122 @@ -113,13 +131,14 @@
   1.123  
   1.124  
   1.125  (*For proofs involving analz.*)
   1.126 -val analz_spies_tac = forward_tac [YM4_analz_spies] 6;
   1.127 +val analz_knows_Spy_tac = 
   1.128 +    forward_tac [YM4_analz_knows_Spy] 7 THEN assume_tac 7;
   1.129  
   1.130  (****
   1.131   The following is to prove theorems of the form
   1.132  
   1.133 -  Key K : analz (insert (Key KAB) (spies evs)) ==>
   1.134 -  Key K : analz (spies evs)
   1.135 +  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   1.136 +  Key K : analz (knows Spy evs)
   1.137  
   1.138   A more general formula must be proved inductively.
   1.139  ****)
   1.140 @@ -128,10 +147,10 @@
   1.141  
   1.142  Goal "evs : yahalom ==>                              \
   1.143  \  ALL K KK. KK <= - (range shrK) -->                \
   1.144 -\         (Key K : analz (Key``KK Un (spies evs))) = \
   1.145 -\         (K : KK | Key K : analz (spies evs))";
   1.146 +\         (Key K : analz (Key``KK Un (knows Spy evs))) = \
   1.147 +\         (K : KK | Key K : analz (knows Spy evs))";
   1.148  by (etac yahalom.induct 1);
   1.149 -by analz_spies_tac;
   1.150 +by analz_knows_Spy_tac;
   1.151  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.152  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   1.153  by (ALLGOALS (asm_simp_tac
   1.154 @@ -141,8 +160,8 @@
   1.155  qed_spec_mp "analz_image_freshK";
   1.156  
   1.157  Goal "[| evs : yahalom;  KAB ~: range shrK |]              \
   1.158 -\      ==> Key K : analz (insert (Key KAB) (spies evs)) =  \
   1.159 -\          (K = KAB | Key K : analz (spies evs))";
   1.160 +\      ==> Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   1.161 +\          (K = KAB | Key K : analz (knows Spy evs))";
   1.162  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.163  qed "analz_insert_freshK";
   1.164  
   1.165 @@ -163,7 +182,7 @@
   1.166  by (expand_case_tac "K = ?y" 1);
   1.167  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.168  (*...we assume X is a recent message and handle this case by contradiction*)
   1.169 -by (blast_tac (claset() addSEs spies_partsEs
   1.170 +by (blast_tac (claset() addSEs knows_Spy_partsEs
   1.171                          delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   1.172  val lemma = result();
   1.173  
   1.174 @@ -185,9 +204,9 @@
   1.175  \             Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.176  \          : set evs -->                                       \
   1.177  \         Notes Spy {|na, nb, Key K|} ~: set evs -->           \
   1.178 -\         Key K ~: analz (spies evs)";
   1.179 +\         Key K ~: analz (knows Spy evs)";
   1.180  by (etac yahalom.induct 1);
   1.181 -by analz_spies_tac;
   1.182 +by analz_knows_Spy_tac;
   1.183  by (ALLGOALS
   1.184      (asm_simp_tac 
   1.185       (simpset() addsimps split_ifs @ pushes @
   1.186 @@ -196,7 +215,7 @@
   1.187  by (blast_tac (claset() addDs [unique_session_keys]) 3);
   1.188  (*YM3*)
   1.189  by (blast_tac (claset() delrules [impCE]
   1.190 -                        addSEs spies_partsEs
   1.191 +                        addSEs knows_Spy_partsEs
   1.192                          addIs [impOfSubs analz_subset_parts]) 2);
   1.193  (*Fake*) 
   1.194  by (spy_analz_tac 1);
   1.195 @@ -210,7 +229,7 @@
   1.196  \          : set evs;                                          \
   1.197  \        Notes Spy {|na, nb, Key K|} ~: set evs;               \
   1.198  \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   1.199 -\     ==> Key K ~: analz (spies evs)";
   1.200 +\     ==> Key K ~: analz (knows Spy evs)";
   1.201  by (blast_tac (claset() addSEs [lemma]) 1);
   1.202  qed "Spy_not_see_encrypted_key";
   1.203  
   1.204 @@ -218,7 +237,7 @@
   1.205  (** Security Guarantee for A upon receiving YM3 **)
   1.206  
   1.207  (*If the encrypted message appears then it originated with the Server*)
   1.208 -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
   1.209 +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   1.210  \        A ~: bad;  evs : yahalom |]                          \
   1.211  \      ==> Says Server A                                            \
   1.212  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   1.213 @@ -230,10 +249,10 @@
   1.214  qed "A_trusts_YM3";
   1.215  
   1.216  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   1.217 -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
   1.218 +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   1.219  \        Notes Spy {|na, nb, Key K|} ~: set evs;               \
   1.220  \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   1.221 -\     ==> Key K ~: analz (spies evs)";
   1.222 +\     ==> Key K ~: analz (knows Spy evs)";
   1.223  by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
   1.224  qed "A_gets_good_key";
   1.225  
   1.226 @@ -241,7 +260,7 @@
   1.227  
   1.228  (*B knows, by the first part of A's message, that the Server distributed 
   1.229    the key for A and B.  But this part says nothing about nonces.*)
   1.230 -Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);      \
   1.231 +Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs);      \
   1.232  \        B ~: bad;  evs : yahalom |]                                 \
   1.233  \     ==> EX NA NB. Says Server A                                    \
   1.234  \                     {|Crypt (shrK A) {|Agent B, Key K,             \
   1.235 @@ -257,11 +276,11 @@
   1.236  
   1.237  (*B knows, by the second part of A's message, that the Server distributed 
   1.238    the key quoting nonce NB.  This part says nothing about agent names. 
   1.239 -  Secrecy of NB is crucial.  Note that  Nonce NB  ~: analz (spies evs)  must
   1.240 +  Secrecy of NB is crucial.  Note that  Nonce NB ~: analz(knows Spy evs)  must
   1.241    be the FIRST antecedent of the induction formula.*)
   1.242  Goal "evs : yahalom                                          \
   1.243 -\     ==> Nonce NB ~: analz (spies evs) -->                  \
   1.244 -\         Crypt K (Nonce NB) : parts (spies evs) -->         \
   1.245 +\     ==> Nonce NB ~: analz (knows Spy evs) -->                  \
   1.246 +\         Crypt K (Nonce NB) : parts (knows Spy evs) -->         \
   1.247  \         (EX A B NA. Says Server A                          \
   1.248  \                     {|Crypt (shrK A) {|Agent B, Key K,     \
   1.249  \                               Nonce NA, Nonce NB|},        \
   1.250 @@ -274,9 +293,9 @@
   1.251  by (Fake_parts_insert_tac 1);
   1.252  (*YM4*)
   1.253  (*A is uncompromised because NB is secure*)
   1.254 -by (not_bad_tac "A" 1);
   1.255 +by (g_not_bad_tac "A" 1);
   1.256  (*A's certificate guarantees the existence of the Server message*)
   1.257 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
   1.258 +by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj RS parts.Fst RS
   1.259  			       A_trusts_YM3]) 1);
   1.260  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   1.261  
   1.262 @@ -308,11 +327,17 @@
   1.263  qed "KeyWithNonce_Notes";
   1.264  Addsimps [KeyWithNonce_Notes];
   1.265  
   1.266 +Goalw [KeyWithNonce_def]
   1.267 +   "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs";
   1.268 +by (Simp_tac 1);
   1.269 +qed "KeyWithNonce_Gets";
   1.270 +Addsimps [KeyWithNonce_Gets];
   1.271 +
   1.272  (*A fresh key cannot be associated with any nonce 
   1.273    (with respect to a given trace). *)
   1.274  Goalw [KeyWithNonce_def]
   1.275   "Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   1.276 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.277 +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
   1.278  qed "fresh_not_KeyWithNonce";
   1.279  
   1.280  (*The Server message associates K with NB' and therefore not with any 
   1.281 @@ -342,10 +367,10 @@
   1.282  Goal "evs : yahalom ==>                                      \
   1.283  \     (ALL KK. KK <= - (range shrK) -->                      \
   1.284  \          (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
   1.285 -\          (Nonce NB : analz (Key``KK Un (spies evs))) =     \
   1.286 -\          (Nonce NB : analz (spies evs)))";
   1.287 +\          (Nonce NB : analz (Key``KK Un (knows Spy evs))) =     \
   1.288 +\          (Nonce NB : analz (knows Spy evs)))";
   1.289  by (etac yahalom.induct 1);
   1.290 -by analz_spies_tac;
   1.291 +by analz_knows_Spy_tac;
   1.292  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   1.293  by (REPEAT_FIRST (rtac Nonce_secrecy_lemma));
   1.294  (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   1.295 @@ -356,15 +381,15 @@
   1.296       (analz_image_freshK_ss 
   1.297         addsimps split_ifs
   1.298         addsimps [all_conj_distrib, analz_image_freshK,
   1.299 -		 KeyWithNonce_Says, KeyWithNonce_Notes,
   1.300 +		 KeyWithNonce_Says, KeyWithNonce_Notes, KeyWithNonce_Gets,
   1.301  		 fresh_not_KeyWithNonce, Says_Server_not_range,
   1.302  		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
   1.303  		 Says_Server_KeyWithNonce])));
   1.304  (*Fake*) 
   1.305  by (spy_analz_tac 1);
   1.306  (*YM4*)  (** LEVEL 6 **)
   1.307 -by (not_bad_tac "A" 1);
   1.308 -by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.309 +by (g_not_bad_tac "A" 1);
   1.310 +by (dtac (Gets_imp_knows_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.311      THEN REPEAT (assume_tac 1));
   1.312  by (blast_tac (claset() addIs [KeyWithNonceI]) 1);
   1.313  qed_spec_mp "Nonce_secrecy";
   1.314 @@ -377,8 +402,8 @@
   1.315  \         {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}  \
   1.316  \        : set evs;                                                  \
   1.317  \        NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]            \
   1.318 -\     ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) =        \
   1.319 -\         (Nonce NB : analz (spies evs))";
   1.320 +\     ==> (Nonce NB : analz (insert (Key KAB) (knows Spy evs))) =        \
   1.321 +\         (Nonce NB : analz (knows Spy evs))";
   1.322  by (asm_simp_tac (analz_image_freshK_ss addsimps 
   1.323  		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   1.324  qed "single_Nonce_secrecy";
   1.325 @@ -388,7 +413,7 @@
   1.326  
   1.327  Goal "evs : yahalom ==>                                         \
   1.328  \EX NA' A' B'. ALL NA A B.                                      \
   1.329 -\   Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
   1.330 +\   Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(knows Spy evs) \
   1.331  \   --> B ~: bad --> NA = NA' & A = A' & B = B'";
   1.332  by (parts_induct_tac 1);
   1.333  (*Fake*)
   1.334 @@ -398,11 +423,11 @@
   1.335  (*YM2: creation of new Nonce.  Move assertion into global context*)
   1.336  by (expand_case_tac "nb = ?y" 1);
   1.337  by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   1.338 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.339 +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
   1.340  val lemma = result();
   1.341  
   1.342 -Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs);    \
   1.343 -\       Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
   1.344 +Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (knows Spy evs);    \
   1.345 +\        Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (knows Spy evs); \
   1.346  \       evs : yahalom;  B ~: bad;  B' ~: bad |]  \
   1.347  \     ==> NA' = NA & A' = A & B' = B";
   1.348  by (prove_unique_tac lemma 1);
   1.349 @@ -411,14 +436,14 @@
   1.350  
   1.351  (*Variant useful for proving secrecy of NB: the Says... form allows 
   1.352    not_bad_tac to remove the assumption B' ~: bad.*)
   1.353 -Goal "[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
   1.354 -\         : set evs;          B ~: bad;                                \
   1.355 -\       Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
   1.356 -\         : set evs;                                                   \
   1.357 -\       nb ~: analz (spies evs);  evs : yahalom |]                     \
   1.358 +Goal "[| Says C S   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
   1.359 +\          : set evs;          B ~: bad;                                \
   1.360 +\        Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}    \
   1.361 +\          : set evs;                                                   \
   1.362 +\        nb ~: analz (knows Spy evs);  evs : yahalom |]                 \
   1.363  \     ==> NA' = NA & A' = A & B' = B";
   1.364 -by (not_bad_tac "B'" 1);
   1.365 -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   1.366 +by (g_not_bad_tac "B'" 1);
   1.367 +by (blast_tac (claset() addSDs [Says_imp_knows_Spy RS parts.Inj]
   1.368                          addSEs [MPair_parts]
   1.369                          addDs  [unique_NB]) 1);
   1.370  qed "Says_unique_NB";
   1.371 @@ -427,12 +452,12 @@
   1.372  (** A nonce value is never used both as NA and as NB **)
   1.373  
   1.374  Goal "evs : yahalom                     \
   1.375 -\ ==> Nonce NB ~: analz (spies evs) -->    \
   1.376 -\  Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
   1.377 -\  Crypt (shrK B)  {|Agent A, na, Nonce NB|} ~: parts(spies evs)";
   1.378 +\ ==> Nonce NB ~: analz (knows Spy evs) -->    \
   1.379 +\  Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(knows Spy evs) --> \
   1.380 +\  Crypt (shrK B)  {|Agent A, na, Nonce NB|} ~: parts(knows Spy evs)";
   1.381  by (parts_induct_tac 1);
   1.382  by (Fake_parts_insert_tac 1);
   1.383 -by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
   1.384 +by (blast_tac (claset() addDs [Gets_imp_knows_Spy RS analz.Inj]
   1.385                          addSIs [parts_insertI]
   1.386                          addSEs partsEs) 1);
   1.387  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   1.388 @@ -444,9 +469,8 @@
   1.389  Goal "[| Says Server A                                                \
   1.390  \         {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
   1.391  \        evs : yahalom |]                                             \
   1.392 -\     ==> EX B'. Says B' Server                                       \
   1.393 -\                   {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.394 -\                : set evs";
   1.395 +\     ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.396 +\            : set evs";
   1.397  by (etac rev_mp 1);
   1.398  by (etac yahalom.induct 1);
   1.399  by Auto_tac;
   1.400 @@ -459,40 +483,44 @@
   1.401  \       {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   1.402  \  : set evs -->                                                    \
   1.403  \  (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->      \
   1.404 -\  Nonce NB ~: analz (spies evs)";
   1.405 +\  Nonce NB ~: analz (knows Spy evs)";
   1.406  by (etac yahalom.induct 1);
   1.407 -by analz_spies_tac;
   1.408 +by analz_knows_Spy_tac;
   1.409  by (ALLGOALS
   1.410      (asm_simp_tac 
   1.411       (simpset() addsimps split_ifs @ pushes @
   1.412  	                 [analz_insert_eq, analz_insert_freshK])));
   1.413  (*Prove YM3 by showing that no NB can also be an NA*)
   1.414 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
   1.415 +by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj]
   1.416  	                addSEs [MPair_parts]
   1.417 -		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4);
   1.418 +		        addDs  [no_nonce_YM1_YM2, Gets_imp_Says,
   1.419 +				Says_unique_NB]) 4);
   1.420  (*YM2: similar freshness reasoning*) 
   1.421  by (blast_tac (claset() addSEs partsEs
   1.422 -		        addDs  [Says_imp_spies RS analz.Inj,
   1.423 +		        addDs  [Gets_imp_Says,
   1.424 +				Says_imp_knows_Spy RS analz.Inj,
   1.425  				impOfSubs analz_subset_parts]) 3);
   1.426  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.427  by (blast_tac (claset() addSIs [parts_insertI]
   1.428 -                        addSEs spies_partsEs) 2);
   1.429 +                        addSEs knows_Spy_partsEs) 2);
   1.430  (*Fake*)
   1.431  by (spy_analz_tac 1);
   1.432  (** LEVEL 7: YM4 and Oops remain **)
   1.433  by (ALLGOALS (Clarify_tac THEN' 
   1.434  	      full_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.435  (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   1.436 -by (not_bad_tac "Aa" 1);
   1.437 -by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.438 +by (g_not_bad_tac "Aa" 1);
   1.439 +by (dtac (Gets_imp_knows_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.440 +    THEN assume_tac 1);
   1.441  by (forward_tac [Says_Server_imp_YM2] 3);
   1.442  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.443  (*  use Says_unique_NB to identify message components: Aa=A, Ba=B*)
   1.444 -by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key]) 1);
   1.445 +by (blast_tac (claset() addDs [Says_unique_NB, 
   1.446 +			       Spy_not_see_encrypted_key]) 1);
   1.447  (** LEVEL 13 **)
   1.448  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   1.449    covered by the quantified Oops assumption.*)
   1.450 -by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   1.451 +by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   1.452  by (expand_case_tac "NB = NBa" 1);
   1.453  (*If NB=NBa then all other components of the Oops message agree*)
   1.454  by (blast_tac (claset() addDs [Says_unique_NB]) 1);
   1.455 @@ -500,7 +528,7 @@
   1.456  by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
   1.457  by (Clarify_tac 1);
   1.458  by (blast_tac (claset() addSEs [MPair_parts]
   1.459 -		        addDs  [Says_imp_spies RS parts.Inj, 
   1.460 +		        addDs  [Says_imp_knows_Spy RS parts.Inj, 
   1.461  			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   1.462  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.463  
   1.464 @@ -510,7 +538,7 @@
   1.465    assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   1.466    If this run is broken and the spy substitutes a certificate containing an
   1.467    old key, B has no means of telling.*)
   1.468 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.469 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.470  \                    Crypt K (Nonce NB)|} : set evs;                     \
   1.471  \        Says B Server                                                   \
   1.472  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.473 @@ -523,8 +551,8 @@
   1.474  \                    Crypt (shrK B) {|Agent A, Key K|}|}                 \
   1.475  \            : set evs";
   1.476  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.477 -by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN
   1.478 -    dtac B_trusts_YM4_shrK 1);
   1.479 +by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN
   1.480 +    assume_tac 1 THEN dtac B_trusts_YM4_shrK 1);
   1.481  by (dtac B_trusts_YM4_newK 3);
   1.482  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.483  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   1.484 @@ -534,14 +562,14 @@
   1.485  
   1.486  
   1.487  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   1.488 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.489 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.490  \                    Crypt K (Nonce NB)|} : set evs;                     \
   1.491  \        Says B Server                                                   \
   1.492  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.493  \          : set evs;                                                    \
   1.494  \        ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
   1.495  \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   1.496 -\     ==> Key K ~: analz (spies evs)";
   1.497 +\     ==> Key K ~: analz (knows Spy evs)";
   1.498  by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
   1.499  qed "B_gets_good_key";
   1.500  
   1.501 @@ -550,7 +578,7 @@
   1.502  
   1.503  (*The encryption in message YM2 tells us it cannot be faked.*)
   1.504  Goal "evs : yahalom                                            \
   1.505 -\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
   1.506 +\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (knows Spy evs) --> \
   1.507  \   B ~: bad -->                                              \
   1.508  \   Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.509  \      : set evs";
   1.510 @@ -570,18 +598,18 @@
   1.511  (*YM4*)
   1.512  by (Blast_tac 2);
   1.513  (*YM3 [blast_tac is 50% slower] *)
   1.514 -by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   1.515 +by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_knows_Spy RS parts.Inj]
   1.516  		       addSEs [MPair_parts]) 1);
   1.517  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   1.518  
   1.519  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.520 -Goal "[| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.521 +Goal "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.522  \          : set evs;                                                    \
   1.523  \        A ~: bad;  B ~: bad;  evs : yahalom |]                        \
   1.524  \==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.525  \      : set evs";
   1.526  by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   1.527 -		        addEs spies_partsEs) 1);
   1.528 +		        addEs knows_Spy_partsEs) 1);
   1.529  qed "YM3_auth_B_to_A";
   1.530  
   1.531  
   1.532 @@ -591,9 +619,9 @@
   1.533    A has said NB.  We can't be sure about the rest of A's message, but only
   1.534    NB matters for freshness.*)  
   1.535  Goal "evs : yahalom                                             \
   1.536 -\     ==> Key K ~: analz (spies evs) -->                     \
   1.537 -\         Crypt K (Nonce NB) : parts (spies evs) -->         \
   1.538 -\         Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \
   1.539 +\     ==> Key K ~: analz (knows Spy evs) -->                     \
   1.540 +\         Crypt K (Nonce NB) : parts (knows Spy evs) -->         \
   1.541 +\         Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs) --> \
   1.542  \         B ~: bad -->                                         \
   1.543  \         (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.544  by (parts_induct_tac 1);
   1.545 @@ -604,18 +632,18 @@
   1.546  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   1.547  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   1.548  (*yes: apply unicity of session keys*)
   1.549 -by (not_bad_tac "Aa" 1);
   1.550 +by (g_not_bad_tac "Aa" 1);
   1.551  by (blast_tac (claset() addSEs [MPair_parts]
   1.552                          addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.553 -		        addDs  [Says_imp_spies RS parts.Inj,
   1.554 +		        addDs  [Says_imp_knows_Spy RS parts.Inj,
   1.555  				unique_session_keys]) 1);
   1.556 -val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   1.557 +qed_spec_mp "A_Said_YM3_lemma";
   1.558  
   1.559  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   1.560    Moreover, A associates K with NB (thus is talking about the same run).
   1.561    Other premises guarantee secrecy of K.*)
   1.562 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.563 -\                    Crypt K (Nonce NB)|} : set evs;                     \
   1.564 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.565 +\                 Crypt K (Nonce NB)|} : set evs;                     \
   1.566  \        Says B Server                                                   \
   1.567  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.568  \          : set evs;                                                    \
   1.569 @@ -624,10 +652,10 @@
   1.570  \     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.571  by (forward_tac [B_trusts_YM4] 1);
   1.572  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   1.573 -by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   1.574 -by (rtac lemma 1);
   1.575 +by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1);
   1.576 +by (rtac A_Said_YM3_lemma 1);
   1.577  by (rtac Spy_not_see_encrypted_key 2);
   1.578  by (REPEAT_FIRST assume_tac);
   1.579  by (blast_tac (claset() addSEs [MPair_parts]
   1.580 -	       	        addDs [Says_imp_spies RS parts.Inj]) 1);
   1.581 +	       	        addDs [Says_imp_knows_Spy RS parts.Inj]) 1);
   1.582  qed_spec_mp "YM4_imp_A_Said_YM3";
     2.1 --- a/src/HOL/Auth/Yahalom.thy	Wed Mar 10 10:42:40 1999 +0100
     2.2 +++ b/src/HOL/Auth/Yahalom.thy	Wed Mar 10 10:42:57 1999 +0100
     2.3 @@ -21,17 +21,21 @@
     2.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     2.5             invent new nonces here, but he can also use NS1.  Common to
     2.6             all similar protocols.*)
     2.7 -    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
     2.8 +    Fake "[| evs: yahalom;  X: synth (analz (knows Spy evs)) |]
     2.9            ==> Says Spy B X  # evs : yahalom"
    2.10  
    2.11 +         (*A message that has been sent can be received by the
    2.12 +           intended recipient.*)
    2.13 +    Reception "[| evsr: yahalom;  Says A B X : set evsr |]
    2.14 +               ==> Gets B X # evsr : yahalom"
    2.15 +
    2.16           (*Alice initiates a protocol run*)
    2.17      YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
    2.18            ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    2.19  
    2.20 -         (*Bob's response to Alice's message.  Bob doesn't know who 
    2.21 -	   the sender is, hence the A' in the sender field.*)
    2.22 +         (*Bob's response to Alice's message.*)
    2.23      YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
    2.24 -             Says A' B {|Agent A, Nonce NA|} : set evs2 |]
    2.25 +             Gets B {|Agent A, Nonce NA|} : set evs2 |]
    2.26            ==> Says B Server 
    2.27                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    2.28                  # evs2 : yahalom"
    2.29 @@ -39,7 +43,7 @@
    2.30           (*The Server receives Bob's message.  He responds by sending a
    2.31              new session key to Alice, with a packet for forwarding to Bob.*)
    2.32      YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
    2.33 -             Says B' Server 
    2.34 +             Gets Server 
    2.35                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    2.36                 : set evs3 |]
    2.37            ==> Says Server A
    2.38 @@ -51,8 +55,8 @@
    2.39             uses the new session key to send Bob his Nonce.  The premise
    2.40             A ~= Server is needed to prove Says_Server_not_range.*)
    2.41      YM4  "[| evs4: yahalom;  A ~= Server;
    2.42 -             Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
    2.43 -                        X|}  : set evs4;
    2.44 +             Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
    2.45 +                : set evs4;
    2.46               Says A B {|Agent A, Nonce NA|} : set evs4 |]
    2.47            ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    2.48  
     3.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Mar 10 10:42:40 1999 +0100
     3.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Mar 10 10:42:57 1999 +0100
     3.3 @@ -12,7 +12,7 @@
     3.4    Proc. Royal Soc. 426 (1989)
     3.5  *)
     3.6  
     3.7 -AddEs spies_partsEs;
     3.8 +AddEs knows_Spy_partsEs;
     3.9  AddDs [impOfSubs analz_subset_parts];
    3.10  AddDs [impOfSubs Fake_parts_insert];
    3.11  
    3.12 @@ -21,58 +21,74 @@
    3.13  Goal "EX X NB K. EX evs: yahalom.          \
    3.14  \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    3.15  by (REPEAT (resolve_tac [exI,bexI] 1));
    3.16 -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    3.17 -          yahalom.YM4) 2);
    3.18 +by (rtac (yahalom.Nil RS 
    3.19 +          yahalom.YM1 RS yahalom.Reception RS
    3.20 +          yahalom.YM2 RS yahalom.Reception RS 
    3.21 +          yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
    3.22  by possibility_tac;
    3.23  result();
    3.24  
    3.25 +Goal "[| Gets B X : set evs; evs : yahalom |] ==> EX A. Says A B X : set evs";
    3.26 +by (etac rev_mp 1);
    3.27 +by (etac yahalom.induct 1);
    3.28 +by Auto_tac;
    3.29 +qed "Gets_imp_Says";
    3.30 +
    3.31 +(*Must be proved separately for each protocol*)
    3.32 +Goal "[| Gets B X : set evs; evs : yahalom |]  ==> X : knows Spy evs";
    3.33 +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    3.34 +qed"Gets_imp_knows_Spy";
    3.35 +AddDs [Gets_imp_knows_Spy RS parts.Inj];
    3.36 +
    3.37  
    3.38  (**** Inductive proofs about yahalom ****)
    3.39  
    3.40  (** For reasoning about the encrypted portion of messages **)
    3.41  
    3.42  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    3.43 -Goal "Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
    3.44 -\             X : analz (spies evs)";
    3.45 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    3.46 -qed "YM4_analz_spies";
    3.47 +Goal "[| Gets A {|NB, Crypt (shrK A) Y, X|} : set evs;  evs : yahalom |]  \
    3.48 +\     ==> X : analz (knows Spy evs)";
    3.49 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    3.50 +qed "YM4_analz_knows_Spy";
    3.51  
    3.52 -bind_thm ("YM4_parts_spies",
    3.53 -          YM4_analz_spies RS (impOfSubs analz_subset_parts));
    3.54 +bind_thm ("YM4_parts_knows_Spy",
    3.55 +          YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    3.56  
    3.57 -(*Relates to both YM4 and Oops*)
    3.58 -Goal "Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
    3.59 -\             K : parts (spies evs)";
    3.60 -by (Blast_tac 1);
    3.61 -qed "YM4_Key_parts_spies";
    3.62 +(*For Oops*)
    3.63 +Goal "Says Server A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs \
    3.64 +\     ==> K : parts (knows Spy evs)";
    3.65 +by (blast_tac (claset() addSEs partsEs
    3.66 +                        addSDs [Says_imp_knows_Spy RS parts.Inj]) 1);
    3.67 +qed "YM4_Key_parts_knows_Spy";
    3.68  
    3.69 -(*For proving the easier theorems about X ~: parts (spies evs).*)
    3.70 -fun parts_spies_tac i = 
    3.71 -    forward_tac [YM4_Key_parts_spies] (i+6) THEN
    3.72 -    forward_tac [YM4_parts_spies] (i+5)     THEN
    3.73 -    prove_simple_subgoals_tac  i;
    3.74 +(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    3.75 +fun parts_knows_Spy_tac i = 
    3.76 +  EVERY
    3.77 +   [forward_tac [YM4_Key_parts_knows_Spy] (i+7),
    3.78 +    forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6),
    3.79 +    prove_simple_subgoals_tac i];
    3.80  
    3.81  (*Induction for regularity theorems.  If induction formula has the form
    3.82 -   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    3.83 -   needless information about analz (insert X (spies evs))  *)
    3.84 +   X ~: analz (knows Spy evs) --> ... then it shortens the proof by discarding
    3.85 +   needless information about analz (insert X (knows Spy evs))  *)
    3.86  fun parts_induct_tac i = 
    3.87      etac yahalom.induct i
    3.88      THEN 
    3.89      REPEAT (FIRSTGOAL analz_mono_contra_tac)
    3.90 -    THEN  parts_spies_tac i;
    3.91 +    THEN  parts_knows_Spy_tac i;
    3.92  
    3.93  
    3.94 -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    3.95 +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    3.96      sends messages containing X! **)
    3.97  
    3.98  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    3.99 -Goal "evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   3.100 +Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
   3.101  by (parts_induct_tac 1);
   3.102  by (ALLGOALS Blast_tac);
   3.103  qed "Spy_see_shrK";
   3.104  Addsimps [Spy_see_shrK];
   3.105  
   3.106 -Goal "evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   3.107 +Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
   3.108  by Auto_tac;
   3.109  qed "Spy_analz_shrK";
   3.110  Addsimps [Spy_analz_shrK];
   3.111 @@ -83,7 +99,7 @@
   3.112  
   3.113  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   3.114  Goal "evs : yahalom ==>          \
   3.115 -\      Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   3.116 +\      Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
   3.117  by (parts_induct_tac 1);
   3.118  (*YM4: Key K is not fresh!*)
   3.119  by (Blast_tac 3);
   3.120 @@ -112,18 +128,18 @@
   3.121  
   3.122  
   3.123  (*For proofs involving analz.*)
   3.124 -val analz_spies_tac = 
   3.125 -    dtac YM4_analz_spies 6 THEN
   3.126 -    forward_tac [Says_Server_message_form] 7 THEN
   3.127 -    assume_tac 7 THEN
   3.128 -    REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
   3.129 +val analz_knows_Spy_tac = 
   3.130 +    dtac YM4_analz_knows_Spy 7 THEN assume_tac 7 THEN
   3.131 +    forward_tac [Says_Server_message_form] 8 THEN
   3.132 +    assume_tac 8 THEN
   3.133 +    REPEAT ((etac conjE ORELSE' hyp_subst_tac) 8);
   3.134  
   3.135  
   3.136  (****
   3.137   The following is to prove theorems of the form
   3.138  
   3.139 -          Key K : analz (insert (Key KAB) (spies evs)) ==>
   3.140 -          Key K : analz (spies evs)
   3.141 +          Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   3.142 +          Key K : analz (knows Spy evs)
   3.143  
   3.144   A more general formula must be proved inductively.
   3.145  
   3.146 @@ -133,10 +149,10 @@
   3.147  
   3.148  Goal "evs : yahalom ==>                               \
   3.149  \  ALL K KK. KK <= - (range shrK) -->                 \
   3.150 -\         (Key K : analz (Key``KK Un (spies evs))) =  \
   3.151 -\         (K : KK | Key K : analz (spies evs))";
   3.152 +\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
   3.153 +\         (K : KK | Key K : analz (knows Spy evs))";
   3.154  by (etac yahalom.induct 1);
   3.155 -by analz_spies_tac;
   3.156 +by analz_knows_Spy_tac;
   3.157  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   3.158  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   3.159  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   3.160 @@ -145,8 +161,8 @@
   3.161  qed_spec_mp "analz_image_freshK";
   3.162  
   3.163  Goal "[| evs : yahalom;  KAB ~: range shrK |] ==>     \
   3.164 -\     Key K : analz (insert (Key KAB) (spies evs)) =  \
   3.165 -\     (K = KAB | Key K : analz (spies evs))";
   3.166 +\     Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   3.167 +\     (K = KAB | Key K : analz (knows Spy evs))";
   3.168  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   3.169  qed "analz_insert_freshK";
   3.170  
   3.171 @@ -187,9 +203,9 @@
   3.172  \                 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
   3.173  \          : set evs -->                                     \
   3.174  \         Notes Spy {|na, nb, Key K|} ~: set evs -->         \
   3.175 -\         Key K ~: analz (spies evs)";
   3.176 +\         Key K ~: analz (knows Spy evs)";
   3.177  by (etac yahalom.induct 1);
   3.178 -by analz_spies_tac;
   3.179 +by analz_knows_Spy_tac;
   3.180  by (ALLGOALS
   3.181      (asm_simp_tac 
   3.182       (simpset() addsimps split_ifs
   3.183 @@ -211,7 +227,7 @@
   3.184  \        : set evs;                                       \
   3.185  \        Notes Spy {|na, nb, Key K|} ~: set evs;          \
   3.186  \        A ~: bad;  B ~: bad;  evs : yahalom |]           \
   3.187 -\     ==> Key K ~: analz (spies evs)";
   3.188 +\     ==> Key K ~: analz (knows Spy evs)";
   3.189  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   3.190  by (blast_tac (claset() addSEs [lemma]) 1);
   3.191  qed "Spy_not_see_encrypted_key";
   3.192 @@ -222,7 +238,7 @@
   3.193  (*If the encrypted message appears then it originated with the Server.
   3.194    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   3.195  Goal "[| Crypt (shrK A) {|Agent B, Key K, na|}                      \
   3.196 -\         : parts (spies evs);                                      \
   3.197 +\         : parts (knows Spy evs);                                      \
   3.198  \        A ~: bad;  evs : yahalom |]                                \
   3.199  \      ==> EX nb. Says Server A                                     \
   3.200  \                   {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
   3.201 @@ -234,10 +250,10 @@
   3.202  qed "A_trusts_YM3";
   3.203  
   3.204  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   3.205 -Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \
   3.206 +Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} : parts (knows Spy evs); \
   3.207  \        ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs;            \
   3.208  \        A ~: bad;  B ~: bad;  evs : yahalom |]                     \
   3.209 -\     ==> Key K ~: analz (spies evs)";
   3.210 +\     ==> Key K ~: analz (knows Spy evs)";
   3.211  by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
   3.212  qed "A_gets_good_key";
   3.213  
   3.214 @@ -247,7 +263,7 @@
   3.215  (*B knows, by the first part of A's message, that the Server distributed 
   3.216    the key for A and B, and has associated it with NB.*)
   3.217  Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \
   3.218 -\          : parts (spies evs);                               \
   3.219 +\          : parts (knows Spy evs);                               \
   3.220  \        B ~: bad;  evs : yahalom |]                          \
   3.221  \ ==> EX NA. Says Server A                                       \
   3.222  \            {|Nonce NB,                                      \
   3.223 @@ -265,7 +281,7 @@
   3.224  
   3.225  (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   3.226    because we do not have to show that NB is secret. *)
   3.227 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   3.228 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   3.229  \                    X|}                                         \
   3.230  \          : set evs;                                            \
   3.231  \        A ~: bad;  B ~: bad;  evs : yahalom |]                  \
   3.232 @@ -279,12 +295,12 @@
   3.233  
   3.234  
   3.235  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   3.236 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   3.237 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   3.238  \                    X|}                                         \
   3.239  \          : set evs;                                            \
   3.240  \        ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs;   \
   3.241  \        A ~: bad;  B ~: bad;  evs : yahalom |]                  \
   3.242 -\     ==> Key K ~: analz (spies evs)";
   3.243 +\     ==> Key K ~: analz (knows Spy evs)";
   3.244  by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
   3.245  qed "B_gets_good_key";
   3.246  
   3.247 @@ -293,7 +309,7 @@
   3.248  (*** Authenticating B to A ***)
   3.249  
   3.250  (*The encryption in message YM2 tells us it cannot be faked.*)
   3.251 -Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs);  \
   3.252 +Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (knows Spy evs);  \
   3.253  \        B ~: bad;  evs : yahalom                                   \
   3.254  \     |] ==> EX NB. Says B Server {|Agent B, Nonce NB,              \
   3.255  \                            Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   3.256 @@ -324,9 +340,9 @@
   3.257  val lemma = result();
   3.258  
   3.259  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   3.260 -Goal "[| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   3.261 +Goal "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}   \
   3.262  \          : set evs;                                                    \
   3.263 -\        A ~: bad;  B ~: bad;  evs : yahalom |]                   \
   3.264 +\        A ~: bad;  B ~: bad;  evs : yahalom |]                          \
   3.265  \==> EX nb'. Says B Server                                               \
   3.266  \                 {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   3.267  \              : set evs";
   3.268 @@ -338,13 +354,13 @@
   3.269  
   3.270  (*Assuming the session key is secure, if both certificates are present then
   3.271    A has said NB.  We can't be sure about the rest of A's message, but only
   3.272 -  NB matters for freshness.  Note that  Key K ~: analz (spies evs)  must be
   3.273 +  NB matters for freshness.  Note that  Key K ~: analz (knows Spy evs)  must be
   3.274    the FIRST antecedent of the induction formula.*)  
   3.275  Goal "evs : yahalom                                     \
   3.276 -\     ==> Key K ~: analz (spies evs) -->                \
   3.277 -\         Crypt K (Nonce NB) : parts (spies evs) -->    \
   3.278 +\     ==> Key K ~: analz (knows Spy evs) -->                \
   3.279 +\         Crypt K (Nonce NB) : parts (knows Spy evs) -->    \
   3.280  \         Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}      \
   3.281 -\           : parts (spies evs) -->                     \
   3.282 +\           : parts (knows Spy evs) -->                     \
   3.283  \         B ~: bad -->                                  \
   3.284  \         (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   3.285  by (parts_induct_tac 1);
   3.286 @@ -356,6 +372,7 @@
   3.287  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   3.288  (*yes: delete a useless induction hypothesis; apply unicity of session keys*)
   3.289  by (thin_tac "?P-->?Q" 1);
   3.290 +by (forward_tac [Gets_imp_Says] 1 THEN assume_tac 1);
   3.291  by (not_bad_tac "Aa" 1);
   3.292  by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   3.293  			addDs  [unique_session_keys]) 1);
   3.294 @@ -365,12 +382,12 @@
   3.295  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   3.296    Moreover, A associates K with NB (thus is talking about the same run).
   3.297    Other premises guarantee secrecy of K.*)
   3.298 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   3.299 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   3.300  \                    Crypt K (Nonce NB)|} : set evs;                 \
   3.301  \        (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
   3.302  \        A ~: bad;  B ~: bad;  evs : yahalom |]                    \
   3.303  \     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   3.304 -by (subgoal_tac "Key K ~: analz (spies evs)" 1);
   3.305 +by (subgoal_tac "Key K ~: analz (knows Spy evs)" 1);
   3.306  by (blast_tac (claset() addIs [Auth_A_to_B_lemma]) 1);
   3.307  by (blast_tac (claset() addDs  [Spy_not_see_encrypted_key,
   3.308  				B_trusts_YM4_shrK]) 1);
     4.1 --- a/src/HOL/Auth/Yahalom2.thy	Wed Mar 10 10:42:40 1999 +0100
     4.2 +++ b/src/HOL/Auth/Yahalom2.thy	Wed Mar 10 10:42:57 1999 +0100
     4.3 @@ -24,17 +24,21 @@
     4.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     4.5             invent new nonces here, but he can also use NS1.  Common to
     4.6             all similar protocols.*)
     4.7 -    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
     4.8 +    Fake "[| evs: yahalom;  X: synth (analz (knows Spy evs)) |]
     4.9            ==> Says Spy B X  # evs : yahalom"
    4.10  
    4.11 +         (*A message that has been sent can be received by the
    4.12 +           intended recipient.*)
    4.13 +    Reception "[| evsr: yahalom;  Says A B X : set evsr |]
    4.14 +               ==> Gets B X # evsr : yahalom"
    4.15 +
    4.16           (*Alice initiates a protocol run*)
    4.17      YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
    4.18            ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    4.19  
    4.20 -         (*Bob's response to Alice's message.  Bob doesn't know who 
    4.21 -	   the sender is, hence the A' in the sender field.*)
    4.22 +         (*Bob's response to Alice's message.*)
    4.23      YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
    4.24 -             Says A' B {|Agent A, Nonce NA|} : set evs2 |]
    4.25 +             Gets B {|Agent A, Nonce NA|} : set evs2 |]
    4.26            ==> Says B Server 
    4.27                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    4.28                  # evs2 : yahalom"
    4.29 @@ -43,8 +47,8 @@
    4.30             new session key to Alice, with a certificate for forwarding to Bob.
    4.31             Both agents are quoted in the 2nd certificate to prevent attacks!*)
    4.32      YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
    4.33 -             Says B' Server {|Agent B, Nonce NB,
    4.34 -			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    4.35 +             Gets Server {|Agent B, Nonce NB,
    4.36 +			   Crypt (shrK B) {|Agent A, Nonce NA|}|}
    4.37                 : set evs3 |]
    4.38            ==> Says Server A
    4.39                 {|Nonce NB, 
    4.40 @@ -55,8 +59,8 @@
    4.41           (*Alice receives the Server's (?) message, checks her Nonce, and
    4.42             uses the new session key to send Bob his Nonce.*)
    4.43      YM4  "[| evs4: yahalom;  
    4.44 -             Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    4.45 -                        X|}  : set evs4;
    4.46 +             Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    4.47 +                      X|}  : set evs4;
    4.48               Says A B {|Agent A, Nonce NA|} : set evs4 |]
    4.49            ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    4.50