Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
authorpaulson
Thu Jun 19 11:28:55 1997 +0200 (1997-06-19)
changeset 3450cd73bc206d87
parent 3449 6b17f82bbf01
child 3451 d10f100676d8
Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jun 19 11:24:37 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Jun 19 11:28:55 1997 +0200
     1.3 @@ -10,12 +10,6 @@
     1.4    Proc. Royal Soc. 426 (1989)
     1.5  *)
     1.6  
     1.7 -(*to HOL/simpdata.ML ????????????????*)
     1.8 -fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]);
     1.9 -prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
    1.10 -prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
    1.11 -
    1.12 -
    1.13  open Yahalom;
    1.14  
    1.15  proof_timing:=true;
    1.16 @@ -184,10 +178,10 @@
    1.17  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    1.18  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    1.19  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    1.20 +(*Fake*) 
    1.21 +by (spy_analz_tac 2);
    1.22  (*Base*)
    1.23  by (Blast_tac 1);
    1.24 -(*YM4, Fake*) 
    1.25 -by (REPEAT (spy_analz_tac 1));
    1.26  qed_spec_mp "analz_image_freshK";
    1.27  
    1.28  goal thy
    1.29 @@ -202,10 +196,10 @@
    1.30  
    1.31  goal thy 
    1.32   "!!evs. evs : yahalom lost ==>                                     \
    1.33 -\      EX A' B' NA' NB' X'. ALL A B NA NB X.                             \
    1.34 +\      EX A' B' na' nb' X'. ALL A B na nb X.                             \
    1.35  \          Says Server A                                            \
    1.36 -\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
    1.37 -\          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
    1.38 +\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
    1.39 +\          : set_of_list evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
    1.40  by (etac yahalom.induct 1);
    1.41  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.42  by (Step_tac 1);
    1.43 @@ -221,13 +215,13 @@
    1.44  
    1.45  goal thy 
    1.46  "!!evs. [| Says Server A                                            \
    1.47 -\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
    1.48 +\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
    1.49  \           : set_of_list evs;                                      \
    1.50  \          Says Server A'                                           \
    1.51 -\           {|Crypt (shrK A') {|Agent B', Key K, NA', NB'|}, X'|}   \
    1.52 +\           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
    1.53  \           : set_of_list evs;                                      \
    1.54  \          evs : yahalom lost |]                                    \
    1.55 -\       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    1.56 +\       ==> A=A' & B=B' & na=na' & nb=nb'";
    1.57  by (prove_unique_tac lemma 1);
    1.58  qed "unique_session_keys";
    1.59  
    1.60 @@ -237,35 +231,36 @@
    1.61  goal thy 
    1.62   "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
    1.63  \        ==> Says Server A                                        \
    1.64 -\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
    1.65 +\              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.66  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.67  \             : set_of_list evs -->                               \
    1.68 -\            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
    1.69 +\            Says A Spy {|na, nb, Key K|} ~: set_of_list evs -->  \
    1.70  \            Key K ~: analz (sees lost Spy evs)";
    1.71  by (etac yahalom.induct 1);
    1.72  by analz_sees_tac;
    1.73  by (ALLGOALS
    1.74      (asm_simp_tac 
    1.75 -     (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
    1.76 +     (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
    1.77 +			 analz_insert_freshK]
    1.78                 setloop split_tac [expand_if])));
    1.79 +(*Oops*)
    1.80 +by (blast_tac (!claset addDs [unique_session_keys]) 3);
    1.81  (*YM3*)
    1.82  by (blast_tac (!claset delrules [impCE]
    1.83                         addSEs sees_Spy_partsEs
    1.84                         addIs [impOfSubs analz_subset_parts]) 2);
    1.85 -(*OR4, Fake*) 
    1.86 -by (REPEAT_FIRST spy_analz_tac);
    1.87 -(*Oops*)
    1.88 -by (blast_tac (!claset addDs [unique_session_keys]) 1);
    1.89 +(*Fake*) 
    1.90 +by (spy_analz_tac 1);
    1.91  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    1.92  
    1.93  
    1.94  (*Final version*)
    1.95  goal thy 
    1.96   "!!evs. [| Says Server A                                         \
    1.97 -\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
    1.98 +\              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.99  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.100  \             : set_of_list evs;                                  \
   1.101 -\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   1.102 +\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   1.103  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.104  \        ==> Key K ~: analz (sees lost Spy evs)";
   1.105  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.106 @@ -277,10 +272,10 @@
   1.107  goal thy 
   1.108   "!!evs. [| C ~: {A,B,Server};                                    \
   1.109  \           Says Server A                                         \
   1.110 -\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
   1.111 +\              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   1.112  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.113  \             : set_of_list evs;                                  \
   1.114 -\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   1.115 +\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   1.116  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.117  \        ==> Key K ~: analz (sees lost C evs)";
   1.118  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.119 @@ -308,11 +303,11 @@
   1.120  
   1.121  (*If the encrypted message appears then it originated with the Server*)
   1.122  goal thy
   1.123 - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA, NB|}                  \
   1.124 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
   1.125  \            : parts (sees lost Spy evs);                              \
   1.126  \           A ~: lost;  evs : yahalom lost |]                          \
   1.127  \         ==> Says Server A                                            \
   1.128 -\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},            \
   1.129 +\              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   1.130  \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   1.131  \             : set_of_list evs";
   1.132  by (etac rev_mp 1);
   1.133 @@ -443,10 +438,6 @@
   1.134  (*Fake*) 
   1.135  by (spy_analz_tac 1);
   1.136  (*YM4*)  (** LEVEL 7 **)
   1.137 -by (asm_simp_tac    (*X contributes nothing to the result of analz*)
   1.138 -    (analz_image_freshK_ss addsimps
   1.139 -     ([ball_conj_distrib, analz_image_freshK, 
   1.140 -       analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono)])) 1);
   1.141  by (not_lost_tac "A" 1);
   1.142  by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.143      THEN REPEAT (assume_tac 1));
   1.144 @@ -561,18 +552,18 @@
   1.145       (!simpset addsimps ([analz_insert_eq, not_parts_not_analz,
   1.146                            analz_insert_freshK] @ pushes)
   1.147                 setloop split_tac [expand_if])));
   1.148 -(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.149 -by (blast_tac (!claset addSIs [parts_insertI]
   1.150 -                       addSEs sees_Spy_partsEs) 2);
   1.151 +(*Prove YM3 by showing that no NB can also be an NA*)
   1.152 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   1.153 +	               addSEs [MPair_parts]
   1.154 +		       addDs  [no_nonce_YM1_YM2, Says_unique_NB']) 4
   1.155 +    THEN flexflex_tac);
   1.156  (*YM2: similar freshness reasoning*) 
   1.157  by (blast_tac (!claset addSEs partsEs
   1.158  		       addDs  [Says_imp_sees_Spy' RS analz.Inj,
   1.159 -			       impOfSubs analz_subset_parts]) 2);
   1.160 -(*Prove YM3 by showing that no NB can also be an NA*)
   1.161 -by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   1.162 -	               addSEs [MPair_parts]
   1.163 -		       addDs  [no_nonce_YM1_YM2, Says_unique_NB']) 2
   1.164 -    THEN flexflex_tac);
   1.165 +			       impOfSubs analz_subset_parts]) 3);
   1.166 +(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.167 +by (blast_tac (!claset addSIs [parts_insertI]
   1.168 +                       addSEs sees_Spy_partsEs) 2);
   1.169  (*Fake*)
   1.170  by (spy_analz_tac 1);
   1.171  (** LEVEL 7: YM4 and Oops remain **)
     2.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Jun 19 11:24:37 1997 +0200
     2.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Jun 19 11:28:55 1997 +0200
     2.3 @@ -179,10 +179,10 @@
     2.4  by (REPEAT_FIRST (resolve_tac [allI, impI]));
     2.5  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     2.6  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     2.7 +(*Fake*) 
     2.8 +by (spy_analz_tac 2);
     2.9  (*Base*)
    2.10 -by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
    2.11 -(*YM4, Fake*) 
    2.12 -by (REPEAT (spy_analz_tac 1));
    2.13 +by (Blast_tac 1);
    2.14  qed_spec_mp "analz_image_freshK";
    2.15  
    2.16  goal thy
    2.17 @@ -197,10 +197,10 @@
    2.18  
    2.19  goal thy 
    2.20   "!!evs. evs : yahalom lost ==>                                     \
    2.21 -\      EX A' B' NA' NB' X'. ALL A B NA NB X.                        \
    2.22 +\      EX A' B' na' nb' X'. ALL A B na nb X.                        \
    2.23  \          Says Server A                                            \
    2.24 -\           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
    2.25 -\          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
    2.26 +\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
    2.27 +\          : set_of_list evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
    2.28  by (etac yahalom.induct 1);
    2.29  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    2.30  by (Step_tac 1);
    2.31 @@ -215,13 +215,13 @@
    2.32  
    2.33  goal thy 
    2.34  "!!evs. [| Says Server A                                            \
    2.35 -\           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
    2.36 +\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
    2.37  \           : set_of_list evs;                                      \
    2.38  \          Says Server A'                                           \
    2.39 -\           {|NB', Crypt (shrK A') {|Agent B', Key K, NA'|}, X'|}   \
    2.40 +\           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|}   \
    2.41  \           : set_of_list evs;                                      \
    2.42  \          evs : yahalom lost |]                                    \
    2.43 -\       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    2.44 +\       ==> A=A' & B=B' & na=na' & nb=nb'";
    2.45  by (prove_unique_tac lemma 1);
    2.46  qed "unique_session_keys";
    2.47  
    2.48 @@ -232,35 +232,36 @@
    2.49   "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
    2.50  \           evs : yahalom lost |]                                    \
    2.51  \        ==> Says Server A                                           \
    2.52 -\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},          \
    2.53 -\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}         \
    2.54 +\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},          \
    2.55 +\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}         \
    2.56  \             : set_of_list evs -->                                  \
    2.57 -\            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->     \
    2.58 +\            Says A Spy {|na, nb, Key K|} ~: set_of_list evs -->     \
    2.59  \            Key K ~: analz (sees lost Spy evs)";
    2.60  by (etac yahalom.induct 1);
    2.61  by analz_sees_tac;
    2.62  by (ALLGOALS
    2.63      (asm_simp_tac 
    2.64 -     (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
    2.65 +     (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
    2.66 +			 analz_insert_freshK]
    2.67                 setloop split_tac [expand_if])));
    2.68 +(*Oops*)
    2.69 +by (blast_tac (!claset addDs [unique_session_keys]) 3);
    2.70  (*YM3*)
    2.71  by (blast_tac (!claset delrules [impCE]
    2.72                         addSEs sees_Spy_partsEs
    2.73                         addIs [impOfSubs analz_subset_parts]) 2);
    2.74 -(*OR4, Fake*) 
    2.75 -by (REPEAT_FIRST spy_analz_tac);
    2.76 -(*Oops*)
    2.77 -by (blast_tac (!claset addDs [unique_session_keys]) 1);
    2.78 +(*Fake*) 
    2.79 +by (spy_analz_tac 1);
    2.80  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    2.81  
    2.82  
    2.83  (*Final version*)
    2.84  goal thy 
    2.85   "!!evs. [| Says Server A                                         \
    2.86 -\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},       \
    2.87 -\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}      \
    2.88 +\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
    2.89 +\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
    2.90  \           : set_of_list evs;                                    \
    2.91 -\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
    2.92 +\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
    2.93  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
    2.94  \        ==> Key K ~: analz (sees lost Spy evs)";
    2.95  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    2.96 @@ -272,10 +273,10 @@
    2.97  goal thy 
    2.98   "!!evs. [| C ~: {A,B,Server};                                    \
    2.99  \           Says Server A                                         \
   2.100 -\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},       \
   2.101 -\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}      \
   2.102 +\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
   2.103 +\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
   2.104  \           : set_of_list evs;                                    \
   2.105 -\           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   2.106 +\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   2.107  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   2.108  \        ==> Key K ~: analz (sees lost C evs)";
   2.109  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   2.110 @@ -285,17 +286,17 @@
   2.111  qed "Agent_not_see_encrypted_key";
   2.112  
   2.113  
   2.114 -(*** Security Guarantees for A and B ***)
   2.115 +(** Security Guarantee for A upon receiving YM3 **)
   2.116  
   2.117  (*If the encrypted message appears then it originated with the Server.
   2.118    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   2.119  goal thy
   2.120 - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA|}                \
   2.121 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
   2.122  \            : parts (sees lost Spy evs);                              \
   2.123  \           A ~: lost;  evs : yahalom lost |]                          \
   2.124 -\         ==> EX NB. Says Server A                                     \
   2.125 -\                      {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},    \
   2.126 -\                            Crypt (shrK B) {|NB, Key K, Agent A|}|}   \
   2.127 +\         ==> EX nb. Says Server A                                     \
   2.128 +\                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
   2.129 +\                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
   2.130  \                    : set_of_list evs";
   2.131  by (etac rev_mp 1);
   2.132  by parts_induct_tac;
   2.133 @@ -304,8 +305,10 @@
   2.134  qed "A_trusts_YM3";
   2.135  
   2.136  
   2.137 +(** Security Guarantee for B upon receiving YM4 **)
   2.138 +
   2.139  (*B knows, by the first part of A's message, that the Server distributed 
   2.140 -  the key for A and B. *)
   2.141 +  the key for A and B, and has associated it with NB. *)
   2.142  goal thy 
   2.143   "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|}              \
   2.144  \            : parts (sees lost Spy evs);                            \
   2.145 @@ -322,20 +325,20 @@
   2.146  by (Blast_tac 1);
   2.147  qed "B_trusts_YM4_shrK";
   2.148  
   2.149 -(*With this variant we don't bother to use the 2nd part of YM4 at all, since
   2.150 -  Nonce NB is available in the first part.  However, the 2nd part does assure B
   2.151 -  of A's existence.*)
   2.152 +
   2.153 +(*With this protocol variant, we don't need the 2nd part of YM4 at all:
   2.154 +  Nonce NB is available in the first part.*)
   2.155  
   2.156  (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   2.157    because we do not have to show that NB is secret. *)
   2.158  goal thy 
   2.159 - "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   2.160 -\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   2.161 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   2.162 -\        ==> EX NA. Says Server A                                       \
   2.163 -\                    {|Nonce NB,                                        \
   2.164 -\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},     \
   2.165 -\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}    \
   2.166 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
   2.167 +\             : set_of_list evs;                                         \
   2.168 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                \
   2.169 +\        ==> EX NA. Says Server A                                        \
   2.170 +\                    {|Nonce NB,                                         \
   2.171 +\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
   2.172 +\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
   2.173  \                   : set_of_list evs";
   2.174  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   2.175  by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
   2.176 @@ -349,7 +352,7 @@
   2.177  goal thy 
   2.178   "!!evs. evs : yahalom lost                                            \
   2.179  \  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees lost Spy evs) -->  \
   2.180 -\      B ~: lost --> \
   2.181 +\      B ~: lost -->                                                   \
   2.182  \      (EX NB. Says B Server {|Agent B, Nonce NB,                      \
   2.183  \                              Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
   2.184  \         : set_of_list evs)";
   2.185 @@ -376,21 +379,23 @@
   2.186  		       addDs [Says_imp_sees_Spy' RS parts.Inj]) 3);
   2.187  (*Fake, YM2*)
   2.188  by (ALLGOALS Blast_tac);
   2.189 -bind_thm ("Says_Server_imp_B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   2.190 +val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   2.191  
   2.192  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   2.193  goal thy
   2.194 - "!!evs. [| Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
   2.195 -\                                X|}  : set_of_list evs;               \
   2.196 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]              \
   2.197 -\         ==> EX nb. Says B Server                                     \
   2.198 -\                     {|Agent B, nb, Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   2.199 -\                    : set_of_list evs";
   2.200 -by (blast_tac (!claset addSDs [A_trusts_YM3, Says_Server_imp_B_Said_YM2]
   2.201 + "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   2.202 +\             : set_of_list evs;                                            \
   2.203 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
   2.204 +\   ==> EX nb'. Says B Server                                               \
   2.205 +\                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   2.206 +\                 : set_of_list evs";
   2.207 +by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   2.208  		       addEs sees_Spy_partsEs) 1);
   2.209  qed "YM3_auth_B_to_A";
   2.210  
   2.211  
   2.212 +(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   2.213 +
   2.214  (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   2.215    It simplifies the proof by discarding needless information about
   2.216  	analz (insert X (sees lost Spy evs)) 
   2.217 @@ -404,18 +409,7 @@
   2.218         mp_tac)  
   2.219      THEN  parts_sees_tac;
   2.220  
   2.221 -fun lost_tac s =
   2.222 -    case_tac ("(" ^ s ^ ") : lost") THEN'
   2.223 -    SELECT_GOAL 
   2.224 -      (REPEAT_DETERM (dtac (Says_imp_sees_Spy' RS analz.Inj) 1) THEN
   2.225 -       REPEAT_DETERM (etac MPair_analz 1) THEN
   2.226 -       THEN_BEST_FIRST 
   2.227 -         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   2.228 -         (has_fewer_prems 1, size_of_thm)
   2.229 -         (Step_tac 1));
   2.230 -
   2.231 -
   2.232 -(*Assuming the session key is secure, if it is used to encrypt NB then
   2.233 +(*Assuming the session key is secure, if both certificates are present then
   2.234    A has said NB.  We can't be sure about the rest of A's message, but only
   2.235    NB matters for freshness.*)  
   2.236  goal thy 
   2.237 @@ -424,24 +418,25 @@
   2.238  \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   2.239  \            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}                \
   2.240  \              : parts (sees lost Spy evs) -->                          \
   2.241 -\             B ~: lost -->                                             \
   2.242 +\            B ~: lost -->                                              \
   2.243  \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
   2.244  by analz_mono_parts_induct_tac;
   2.245  (*Fake*)
   2.246  by (Fake_parts_insert_tac 1);
   2.247  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   2.248  by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   2.249 -(*YM4*)
   2.250 -by(Step_tac 1);
   2.251 -by (REPEAT (Blast_tac 2));
   2.252 -by (lost_tac "Aa" 1);
   2.253 +(*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   2.254 +by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   2.255 +(*yes: apply unicity of session keys*)
   2.256 +by (not_lost_tac "Aa" 1);
   2.257  by (blast_tac (!claset addSEs [MPair_parts]
   2.258                         addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   2.259  		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
   2.260  			       unique_session_keys]) 1);
   2.261 -val lemma = normalize_thm [RSspec, RSmp] (result());
   2.262 +val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   2.263  
   2.264  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   2.265 +  Moreover, A associates K with NB (thus is talking about the same run).
   2.266    Other premises guarantee secrecy of K.*)
   2.267  goal thy 
   2.268   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   2.269 @@ -450,12 +445,12 @@
   2.270  \               ~: set_of_list evs);                                    \
   2.271  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   2.272  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
   2.273 -be (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1;
   2.274 -bd (B_trusts_YM4_shrK) 1;
   2.275 +by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   2.276 +by (dtac B_trusts_YM4_shrK 1);
   2.277  by (safe_tac (!claset));
   2.278 -br lemma 1;
   2.279 -br Spy_not_see_encrypted_key 2;
   2.280 +by (rtac lemma 1);
   2.281 +by (rtac Spy_not_see_encrypted_key 2);
   2.282  by (REPEAT_FIRST assume_tac);
   2.283  by (ALLGOALS (blast_tac (!claset addSEs [MPair_parts]
   2.284 -			 addDs [Says_imp_sees_Spy' RS parts.Inj])));
   2.285 +			         addDs [Says_imp_sees_Spy' RS parts.Inj])));
   2.286  qed_spec_mp "YM4_imp_A_Said_YM3";