sessionK now indexed by nat instead of bool.
authorpaulson
Wed Sep 24 12:27:53 1997 +0200 (1997-09-24)
changeset 37042f99d7a0dccc
parent 3703 c5ae2d63dbaa
child 3705 76f3b2803982
sessionK now indexed by nat instead of bool.
Weaker Oops conditions on final guarantees
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Wed Sep 24 12:26:14 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Wed Sep 24 12:27:53 1997 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    rollback attacks).
     1.5  *)
     1.6  
     1.7 +
     1.8  open TLS;
     1.9  
    1.10  proof_timing:=true;
    1.11 @@ -162,7 +163,7 @@
    1.12      REPEAT (FIRSTGOAL analz_mono_contra_tac)
    1.13      THEN 
    1.14      fast_tac (!claset addss (!simpset)) i THEN
    1.15 -    ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]));
    1.16 +    ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
    1.17  
    1.18  
    1.19  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.20 @@ -252,10 +253,10 @@
    1.21  \        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
    1.22  by (etac rev_mp 1);
    1.23  by (parts_induct_tac 1);
    1.24 +by clarify_tac;
    1.25  (*Fake*)
    1.26  by (blast_tac (!claset addIs [parts_insertI]) 1);
    1.27  (*Client, Server Accept*)
    1.28 -by (Step_tac 1);
    1.29  by (REPEAT (blast_tac (!claset addSEs spies_partsEs
    1.30                                 addSDs [Notes_Crypt_parts_spies]) 1));
    1.31  qed "Notes_master_imp_Crypt_PMS";
    1.32 @@ -424,16 +425,59 @@
    1.33  
    1.34  (** Some lemmas about session keys, comprising clientK and serverK **)
    1.35  
    1.36 -(*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
    1.37 -  Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
    1.38  
    1.39 +(*Lemma: session keys are never used if PMS is fresh.  
    1.40 +  Nonces don't have to agree, allowing session resumption.
    1.41 +  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
    1.42 +  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
    1.43 +goal thy 
    1.44 + "!!evs. [| Nonce PMS ~: parts (spies evs);  \
    1.45 +\           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
    1.46 +\           evs : tls |]             \
    1.47 +\  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
    1.48 +by (etac rev_mp 1);
    1.49 +by (hyp_subst_tac 1);
    1.50 +by (analz_induct_tac 1);
    1.51 +(*SpyKeys*)
    1.52 +by (blast_tac (!claset addSEs spies_partsEs) 3);
    1.53 +(*Fake*)
    1.54 +by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
    1.55 +by (Fake_parts_insert_tac 2);
    1.56 +(** LEVEL 6 **)
    1.57 +(*Oops*)
    1.58 +by (fast_tac (!claset addSEs [MPair_parts]
    1.59 +		       addDs  [Says_imp_spies RS parts.Inj]
    1.60 +		       addss (!simpset)) 6);
    1.61 +by (REPEAT 
    1.62 +    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
    1.63 +				Notes_master_imp_Crypt_PMS]
    1.64 +                        addSEs spies_partsEs) 1));
    1.65 +val lemma = result();
    1.66 +
    1.67 +goal thy 
    1.68 + "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
    1.69 +\  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
    1.70 +by (blast_tac (!claset addDs [lemma]) 1);
    1.71 +qed "PMS_sessionK_not_spied";
    1.72 +
    1.73 +goal thy 
    1.74 + "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
    1.75 +\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
    1.76 +by (blast_tac (!claset addDs [lemma]) 1);
    1.77 +qed "PMS_Crypt_sessionK_not_spied";
    1.78 +
    1.79 +
    1.80 +(*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
    1.81 +  Converse doesn't hold; betraying M doesn't force the keys to be sent!
    1.82 +  The strong Oops condition can be weakened later by unicity reasoning, 
    1.83 +	with some effort.*)
    1.84  goal thy 
    1.85   "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
    1.86  \           Nonce M ~: analz (spies evs);  evs : tls |]   \
    1.87  \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
    1.88  by (etac rev_mp 1);
    1.89  by (etac rev_mp 1);
    1.90 -by (analz_induct_tac 1);	(*30 seconds??*)
    1.91 +by (analz_induct_tac 1);        (*30 seconds??*)
    1.92  (*Oops*)
    1.93  by (Blast_tac 4);
    1.94  (*SpyKeys*)
    1.95 @@ -442,40 +486,8 @@
    1.96  by (spy_analz_tac 2);
    1.97  (*Base*)
    1.98  by (Blast_tac 1);
    1.99 -qed "sessionK_notin_parts";
   1.100 -bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE));
   1.101 -
   1.102 -Addsimps [sessionK_notin_parts];
   1.103 -AddSEs [sessionK_in_partsE, 
   1.104 -	impOfSubs analz_subset_parts RS sessionK_in_partsE];
   1.105 -
   1.106 -
   1.107 -(*Lemma: session keys are never used if PMS is fresh.  
   1.108 -  Nonces don't have to agree, allowing session resumption.
   1.109 -  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   1.110 -  They are NOT suitable as safe elim rules.*)
   1.111 -
   1.112 -goal thy 
   1.113 - "!!evs. [| ALL A. Says A Spy (Key (sessionK((Na, Nb, PRF(PMS,NA,NB)),b))) \
   1.114 -\                    ~: set evs; \
   1.115 -\           Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   1.116 -\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   1.117 -by (etac rev_mp 1);
   1.118 -by (etac rev_mp 1);
   1.119 -by (analz_induct_tac 1);
   1.120 -(*Fake*)
   1.121 -by (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]) 2);
   1.122 -by (Fake_parts_insert_tac 2);
   1.123 -(*Base, ClientFinished, ServerFinished, ClientResume: 
   1.124 -  trivial, e.g. by freshness*)
   1.125 -by (REPEAT 
   1.126 -    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
   1.127 -				Notes_master_imp_Crypt_PMS]
   1.128 -                        addSEs spies_partsEs) 1));
   1.129 -qed "Crypt_sessionK_notin_parts";
   1.130 -
   1.131 -Addsimps [Crypt_sessionK_notin_parts];
   1.132 -AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
   1.133 +qed "sessionK_not_spied";
   1.134 +Addsimps [sessionK_not_spied];
   1.135  
   1.136  
   1.137  (*NEEDED??*)
   1.138 @@ -511,20 +523,19 @@
   1.139  \           evs : tls |]                                          \
   1.140  \        ==> B=B'";
   1.141  by (prove_unique_tac lemma 1);
   1.142 -qed "unique_PMS";
   1.143 +qed "Crypt_unique_PMS";
   1.144 +
   1.145  
   1.146  (** It is frustrating that we need two versions of the unicity results.
   1.147 -    But Notes A {|Agent B, Nonce PMS|} determines both A and B, while
   1.148 -    Crypt(pubK B) (Nonce PMS) determines only B, and sometimes only
   1.149 -    this weaker item is available.
   1.150 +    But Notes A {|Agent B, Nonce PMS|} determines both A and B.  Sometimes
   1.151 +    we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which 
   1.152 +    determines B alone, and only if PMS is secret.
   1.153  **)
   1.154  
   1.155  (*In A's internal Note, PMS determines A and B.*)
   1.156 -goal thy 
   1.157 - "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]            \
   1.158 -\ ==> EX A' B'. ALL A B.                                                   \
   1.159 -\        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   1.160 -by (etac rev_mp 1);
   1.161 +goal thy "!!evs. evs : tls               \
   1.162 +\                ==> EX A' B'. ALL A B.  \
   1.163 +\                    Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   1.164  by (parts_induct_tac 1);
   1.165  by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.166  (*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
   1.167 @@ -535,7 +546,6 @@
   1.168  goal thy 
   1.169   "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   1.170  \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   1.171 -\           Nonce PMS ~: analz (spies evs);      \
   1.172  \           evs : tls |]                               \
   1.173  \        ==> A=A' & B=B'";
   1.174  by (prove_unique_tac lemma 1);
   1.175 @@ -564,17 +574,6 @@
   1.176  bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   1.177  
   1.178  
   1.179 -(*Another way of showing unicity*)
   1.180 -goal thy 
   1.181 - "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   1.182 -\           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   1.183 -\           A ~: bad;  B ~: bad;                         \
   1.184 -\           evs : tls |]                                 \
   1.185 -\        ==> A=A' & B=B'";
   1.186 -by (REPEAT (ares_tac [Notes_unique_PMS, Spy_not_see_PMS] 1));
   1.187 -qed "good_Notes_unique_PMS";
   1.188 -
   1.189 -
   1.190  (*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   1.191    will stay secret.*)
   1.192  goal thy
   1.193 @@ -601,6 +600,97 @@
   1.194  bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   1.195  
   1.196  
   1.197 +(*** Weakening the Oops conditions for leakage of clientK ***)
   1.198 +
   1.199 +(*If A created PMS then nobody other than the Spy would send a message
   1.200 +  using a clientK generated from that PMS.*)
   1.201 +goal thy
   1.202 + "!!evs. [| evs : tls;  A' ~= Spy |]                \
   1.203 +\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.204 +\      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   1.205 +\      A = A'";
   1.206 +by (analz_induct_tac 1);	(*17 seconds*)
   1.207 +by clarify_tac;
   1.208 +(*ClientFinished, ClientResume: by unicity of PMS*)
   1.209 +by (REPEAT 
   1.210 +    (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
   1.211 +     	 	        addIs  [Notes_unique_PMS RS conjunct1]) 2));
   1.212 +(*ClientCertKeyEx*)
   1.213 +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   1.214 +	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   1.215 +bind_thm ("Says_clientK_unique",
   1.216 +	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.217 +
   1.218 +
   1.219 +(*If A created PMS and has not leaked her clientK to the Spy, 
   1.220 +  then nobody has.*)
   1.221 +goal thy
   1.222 + "!!evs. evs : tls                         \
   1.223 +\  ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   1.224 +\      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   1.225 +\      (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   1.226 +by (etac tls.induct 1);
   1.227 +(*This roundabout proof sequence avoids looping in simplification*)
   1.228 +by (ALLGOALS Simp_tac);
   1.229 +by clarify_tac;
   1.230 +by (Fake_parts_insert_tac 1);
   1.231 +by (ALLGOALS Asm_simp_tac);
   1.232 +(*Oops*)
   1.233 +by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
   1.234 +(*ClientCertKeyEx*)
   1.235 +by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   1.236 +			       spies_partsEs)) 1);
   1.237 +qed_spec_mp "clientK_Oops_ALL";
   1.238 +
   1.239 +
   1.240 +
   1.241 +(*** Weakening the Oops conditions for leakage of serverK ***)
   1.242 +
   1.243 +(*If A created PMS for B, then nobody other than B or the Spy would
   1.244 +  send a message using a serverK generated from that PMS.*)
   1.245 +goal thy
   1.246 + "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;  B' ~= Spy |]                \
   1.247 +\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.248 +\      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   1.249 +\      B = B'";
   1.250 +by (analz_induct_tac 1);	(*17 seconds*)
   1.251 +by clarify_tac;
   1.252 +(*ServerResume, ServerFinished: by unicity of PMS*)
   1.253 +by (REPEAT
   1.254 +    (blast_tac (!claset addSEs [MPair_parts]
   1.255 +		        addSDs [Notes_master_imp_Crypt_PMS, 
   1.256 +				Says_imp_spies RS parts.Inj]
   1.257 +                        addDs  [Spy_not_see_PMS, 
   1.258 +				Notes_Crypt_parts_spies,
   1.259 +				Crypt_unique_PMS]) 2));
   1.260 +(*ClientCertKeyEx*)
   1.261 +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   1.262 +	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   1.263 +bind_thm ("Says_serverK_unique",
   1.264 +	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.265 +
   1.266 +(*If A created PMS for B, and B has not leaked his serverK to the Spy, 
   1.267 +  then nobody has.*)
   1.268 +goal thy
   1.269 + "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                        \
   1.270 +\  ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   1.271 +\      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   1.272 +\      (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   1.273 +by (etac tls.induct 1);
   1.274 +(*This roundabout proof sequence avoids looping in simplification*)
   1.275 +by (ALLGOALS Simp_tac);
   1.276 +by clarify_tac;
   1.277 +by (Fake_parts_insert_tac 1);
   1.278 +by (ALLGOALS Asm_simp_tac);
   1.279 +(*Oops*)
   1.280 +by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
   1.281 +(*ClientCertKeyEx*)
   1.282 +by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   1.283 +			       spies_partsEs)) 1);
   1.284 +qed_spec_mp "serverK_Oops_ALL";
   1.285 +
   1.286 +
   1.287 +
   1.288  (*** Protocol goals: if A receives ServerFinished, then B is present 
   1.289       and has used the quoted values XA, XB, etc.  Note that it is up to A
   1.290       to compare XA with what she originally sent.
   1.291 @@ -619,25 +709,44 @@
   1.292  \        X : parts (spies evs) --> Says B A X : set evs";
   1.293  by (etac rev_mp 1);
   1.294  by (hyp_subst_tac 1);
   1.295 -by (analz_induct_tac 1);	(*16 seconds*)
   1.296 -(*ServerResume is trivial, but Blast_tac is too slow*)
   1.297 -by (Best_tac 3);
   1.298 +by (analz_induct_tac 1);        (*27 seconds*)
   1.299 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.300 +by clarify_tac;
   1.301 +(*ServerResume*)
   1.302 +by (Blast_tac 3);
   1.303  (*ClientCertKeyEx*)
   1.304 -by (Blast_tac 2);
   1.305 +by (fast_tac  (*blast_tac gives PROOF FAILED*)
   1.306 +    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.307  (*Fake: the Spy doesn't have the critical session key!*)
   1.308 -by (REPEAT (rtac impI 1));
   1.309  by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   1.310  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.311  				     not_parts_not_analz]) 2);
   1.312  by (Fake_parts_insert_tac 1);
   1.313 +val lemma = normalize_thm [RSspec, RSmp] (result());
   1.314 +
   1.315 +(*Final version*)
   1.316 +goal thy
   1.317 + "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   1.318 +\                 (Hash{|Nonce M, Number SID,             \
   1.319 +\                        Nonce NA, Number XA, Agent A,    \
   1.320 +\                        Nonce NB, Number XB, Agent B|}); \
   1.321 +\           M = PRF(PMS,NA,NB);                           \
   1.322 +\           X : parts (spies evs);                        \
   1.323 +\           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   1.324 +\           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   1.325 +\           evs : tls;  A ~: bad;  B ~: bad |]          \
   1.326 +\        ==> Says B A X : set evs";
   1.327 +by (blast_tac (!claset addIs [lemma]
   1.328 +                       addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   1.329  qed_spec_mp "TrustServerFinished";
   1.330  
   1.331  
   1.332 +
   1.333  (*This version refers not to ServerFinished but to any message from B.
   1.334    We don't assume B has received CertVerify, and an intruder could
   1.335    have changed A's identity in all other messages, so we can't be sure
   1.336    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   1.337 -  to bind A's identity with M, then we could replace A' by A below.*)
   1.338 +  to bind A's identity with PMS, then we could replace A' by A below.*)
   1.339  goal thy
   1.340   "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   1.341  \           evs : tls;  A ~: bad;  B ~: bad;                 \
   1.342 @@ -648,33 +757,47 @@
   1.343  by (etac rev_mp 1);
   1.344  by (hyp_subst_tac 1);
   1.345  by (analz_induct_tac 1);	(*20 seconds*)
   1.346 -by (REPEAT_FIRST (rtac impI));
   1.347 -(*ServerResume, by unicity of PMS*)
   1.348 -by (blast_tac (!claset addSEs [MPair_parts]
   1.349 -		       addDs  [Spy_not_see_PMS, 
   1.350 -			       Notes_Crypt_parts_spies,
   1.351 -			       Notes_master_imp_Crypt_PMS, unique_PMS]) 4);
   1.352 -(*ServerFinished, by unicity of PMS (10 seconds)*)
   1.353 -by (blast_tac (!claset addSEs [MPair_parts]
   1.354 -		       addDs  [Spy_not_see_PMS, 
   1.355 -			       Notes_Crypt_parts_spies,
   1.356 -			       Says_imp_spies RS parts.Inj,
   1.357 -			       unique_PMS]) 3);
   1.358 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.359 +by clarify_tac;
   1.360 +(*ServerResume, ServerFinished: by unicity of PMS*)
   1.361 +by (REPEAT
   1.362 +    (blast_tac (!claset addSEs [MPair_parts]
   1.363 +		        addSDs [Notes_master_imp_Crypt_PMS, 
   1.364 +				Says_imp_spies RS parts.Inj]
   1.365 +                        addDs  [Spy_not_see_PMS, 
   1.366 +				Notes_Crypt_parts_spies,
   1.367 +				Crypt_unique_PMS]) 3));
   1.368  (*ClientCertKeyEx*)
   1.369 -by (Blast_tac 2);
   1.370 +by (blast_tac
   1.371 +    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.372  (*Fake: the Spy doesn't have the critical session key!*)
   1.373  by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   1.374  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.375  				     not_parts_not_analz]) 2);
   1.376  by (Fake_parts_insert_tac 1);
   1.377 +val lemma = normalize_thm [RSspec, RSmp] (result());
   1.378 +
   1.379 +(*Final version*)
   1.380 +goal thy
   1.381 + "!!evs. [| M = PRF(PMS,NA,NB);                           \
   1.382 +\           Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
   1.383 +\           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   1.384 +\           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   1.385 +\           evs : tls;  A ~: bad;  B ~: bad |]          \
   1.386 +\        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
   1.387 +by (blast_tac (!claset addIs [lemma]
   1.388 +                       addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   1.389 +
   1.390  qed_spec_mp "TrustServerMsg";
   1.391  
   1.392  
   1.393 +
   1.394  (*** Protocol goal: if B receives any message encrypted with clientK
   1.395       then A has sent it, ASSUMING that A chose PMS.  Authentication is
   1.396       assumed here; B cannot verify it.  But if the message is
   1.397       ClientFinished, then B can then check the quoted values XA, XB, etc.
   1.398  ***)
   1.399 +
   1.400  goal thy
   1.401   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
   1.402  \  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
   1.403 @@ -682,23 +805,30 @@
   1.404  \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
   1.405  \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.406  by (analz_induct_tac 1);	(*23 seconds*)
   1.407 -by (REPEAT_FIRST (rtac impI));
   1.408 -(*ClientResume: by unicity of PMS*)
   1.409 -by (blast_tac (!claset delrules [conjI]
   1.410 -		       addSEs [MPair_parts]
   1.411 -                       addSDs [Notes_master_imp_Notes_PMS]
   1.412 -	 	       addDs  [good_Notes_unique_PMS]) 4);
   1.413 -(*ClientFinished: by unicity of PMS*)
   1.414 -by (blast_tac (!claset delrules [conjI]
   1.415 -		       addSEs [MPair_parts]
   1.416 -		       addDs  [good_Notes_unique_PMS]) 3);
   1.417 +by clarify_tac;
   1.418 +(*ClientFinished, ClientResume: by unicity of PMS*)
   1.419 +by (REPEAT (blast_tac (!claset delrules [conjI]
   1.420 +		               addSDs [Notes_master_imp_Notes_PMS]
   1.421 +	 	               addDs  [Notes_unique_PMS]) 3));
   1.422  (*ClientCertKeyEx*)
   1.423 -by (Blast_tac 2);
   1.424 +by (fast_tac  (*blast_tac gives PROOF FAILED*)
   1.425 +    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.426  (*Fake: the Spy doesn't have the critical session key!*)
   1.427  by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   1.428  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.429  				     not_parts_not_analz]) 2);
   1.430  by (Fake_parts_insert_tac 1);
   1.431 +val lemma = normalize_thm [RSspec, RSmp] (result());
   1.432 +
   1.433 +(*Final version*)
   1.434 +goal thy
   1.435 + "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs);  \
   1.436 +\           Notes A {|Agent B, Nonce PMS|} : set evs;        \
   1.437 +\           Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;  \
   1.438 +\           evs : tls;  A ~: bad;  B ~: bad |]                         \
   1.439 +\  ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.440 +by (blast_tac (!claset addIs [lemma]
   1.441 +                       addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
   1.442  qed_spec_mp "TrustClientMsg";
   1.443  
   1.444  
   1.445 @@ -708,7 +838,7 @@
   1.446       values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.447   ***)
   1.448  goal thy
   1.449 - "!!evs. [| ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   1.450 + "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   1.451  \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.452  \           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   1.453  \             : set evs;                                                  \
   1.454 @@ -722,3 +852,5 @@
   1.455  qed "AuthClientFinished";
   1.456  
   1.457  (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
   1.458 +
   1.459 +
     2.1 --- a/src/HOL/Auth/TLS.thy	Wed Sep 24 12:26:14 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Wed Sep 24 12:27:53 1997 +0200
     2.3 @@ -45,10 +45,11 @@
     2.4    (*Pseudo-random function of Section 5*)
     2.5    PRF  :: "nat*nat*nat => nat"
     2.6  
     2.7 -  (*Client, server write keys generated uniformly by function sessionK
     2.8 -    to avoid duplicating their properties.
     2.9 -    Theyimplicitly include the MAC secrets.*)
    2.10 -  sessionK :: "(nat*nat*nat)*bool => key"
    2.11 +  (*Client, server write keys are generated uniformly by function sessionK
    2.12 +    to avoid duplicating their properties.  They are indexed by a further
    2.13 +    natural number, not a bool, to avoid the peculiarities of if-and-only-if.
    2.14 +    Session keys implicitly include MAC secrets.*)
    2.15 +  sessionK :: "(nat*nat*nat)*nat => key"
    2.16  
    2.17    certificate      :: "[agent,key] => msg"
    2.18  
    2.19 @@ -60,8 +61,8 @@
    2.20      clientK, serverK :: "nat*nat*nat => key"
    2.21  
    2.22  translations
    2.23 -  "clientK (x)"	== "sessionK(x,True)"
    2.24 -  "serverK (x)"	== "sessionK(x,False)"
    2.25 +  "clientK (x)"	== "sessionK(x,0)"
    2.26 +  "serverK (x)"	== "sessionK(x,1)"
    2.27  
    2.28  rules
    2.29    inj_PRF       "inj PRF"