1(* Title: HOL/Auth/TLS.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1997 University of Cambridge 4 5Inductive relation "tls" for the TLS (Transport Layer Security) protocol. 6This protocol is essentially the same as SSL 3.0. 7 8Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher 9Allen, Transport Layer Security Working Group, 21 May 1997, 10INTERNET-DRAFT draft-ietf-tls-protocol-03.txt. Section numbers below refer 11to that memo. 12 13An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down 14to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a 15global signing authority. 16 17A is the client and B is the server, not to be confused with the constant 18Server, who is in charge of all public keys. 19 20The model assumes that no fraudulent certificates are present, but it does 21assume that some private keys are to the spy. 22 23REMARK. The event "Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>" appears in ClientKeyExch, 24CertVerify, ClientFinished to record that A knows M. It is a note from A to 25herself. Nobody else can see it. In ClientKeyExch, the Spy can substitute 26his own certificate for A's, but he cannot replace A's note by one for himself. 27 28The Note event avoids a weakness in the public-key model. Each 29agent's state is recorded as the trace of messages. When the true client (A) 30invents PMS, he encrypts PMS with B's public key before sending it. The model 31does not distinguish the original occurrence of such a message from a replay. 32In the shared-key model, the ability to encrypt implies the ability to 33decrypt, so the problem does not arise. 34 35Proofs would be simpler if ClientKeyExch included A's name within 36Crypt KB (Nonce PMS). As things stand, there is much overlap between proofs 37about that message (which B receives) and the stronger event 38Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>. 39*) 40 41section\<open>The TLS Protocol: Transport Layer Security\<close> 42 43theory TLS imports Public "HOL-Library.Nat_Bijection" begin 44 45definition certificate :: "[agent,key] \<Rightarrow> msg" where 46 "certificate A KA == Crypt (priSK Server) \<lbrace>Agent A, Key KA\<rbrace>" 47 48text\<open>TLS apparently does not require separate keypairs for encryption and 49signature. Therefore, we formalize signature as encryption using the 50private encryption key.\<close> 51 52datatype role = ClientRole | ServerRole 53 54consts 55 (*Pseudo-random function of Section 5*) 56 PRF :: "nat*nat*nat \<Rightarrow> nat" 57 58 (*Client, server write keys are generated uniformly by function sessionK 59 to avoid duplicating their properties. They are distinguished by a 60 tag (not a bool, to avoid the peculiarities of if-and-only-if). 61 Session keys implicitly include MAC secrets.*) 62 sessionK :: "(nat*nat*nat) * role \<Rightarrow> key" 63 64abbreviation 65 clientK :: "nat*nat*nat \<Rightarrow> key" where 66 "clientK X == sessionK(X, ClientRole)" 67 68abbreviation 69 serverK :: "nat*nat*nat \<Rightarrow> key" where 70 "serverK X == sessionK(X, ServerRole)" 71 72 73specification (PRF) 74 inj_PRF: "inj PRF" 75 \<comment> \<open>the pseudo-random function is collision-free\<close> 76 apply (rule exI [of _ "\<lambda>(x,y,z). prod_encode(x, prod_encode(y,z))"]) 77 apply (simp add: inj_on_def prod_encode_eq) 78 done 79 80specification (sessionK) 81 inj_sessionK: "inj sessionK" 82 \<comment> \<open>sessionK is collision-free; also, no clientK clashes with any serverK.\<close> 83 apply (rule exI [of _ 84 "\<lambda>((x,y,z), r). prod_encode(case_role 0 1 r, 85 prod_encode(x, prod_encode(y,z)))"]) 86 apply (simp add: inj_on_def prod_encode_eq split: role.split) 87 done 88 89axiomatization where 90 \<comment> \<open>sessionK makes symmetric keys\<close> 91 isSym_sessionK: "sessionK nonces \<in> symKeys" and 92 93 \<comment> \<open>sessionK never clashes with a long-term symmetric key 94 (they don't exist in TLS anyway)\<close> 95 sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A" 96 97 98inductive_set tls :: "event list set" 99 where 100 Nil: \<comment> \<open>The initial, empty trace\<close> 101 "[] \<in> tls" 102 103 | Fake: \<comment> \<open>The Spy may say anything he can say. The sender field is correct, 104 but agents don't use that information.\<close> 105 "[| evsf \<in> tls; X \<in> synth (analz (spies evsf)) |] 106 ==> Says Spy B X # evsf \<in> tls" 107 108 | SpyKeys: \<comment> \<open>The spy may apply \<^term>\<open>PRF\<close> and \<^term>\<open>sessionK\<close> 109 to available nonces\<close> 110 "[| evsSK \<in> tls; 111 {Nonce NA, Nonce NB, Nonce M} \<subseteq> analz (spies evsSK) |] 112 ==> Notes Spy \<lbrace> Nonce (PRF(M,NA,NB)), 113 Key (sessionK((NA,NB,M),role))\<rbrace> # evsSK \<in> tls" 114 115 | ClientHello: 116 \<comment> \<open>(7.4.1.2) 117 PA represents \<open>CLIENT_VERSION\<close>, \<open>CIPHER_SUITES\<close> and \<open>COMPRESSION_METHODS\<close>. 118 It is uninterpreted but will be confirmed in the FINISHED messages. 119 NA is CLIENT RANDOM, while SID is \<open>SESSION_ID\<close>. 120 UNIX TIME is omitted because the protocol doesn't use it. 121 May assume \<^term>\<open>NA \<notin> range PRF\<close> because CLIENT RANDOM is 122 28 bytes while MASTER SECRET is 48 bytes\<close> 123 "[| evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> range PRF |] 124 ==> Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> 125 # evsCH \<in> tls" 126 127 | ServerHello: 128 \<comment> \<open>7.4.1.3 of the TLS Internet-Draft 129 PB represents \<open>CLIENT_VERSION\<close>, \<open>CIPHER_SUITE\<close> and \<open>COMPRESSION_METHOD\<close>. 130 SERVER CERTIFICATE (7.4.2) is always present. 131 \<open>CERTIFICATE_REQUEST\<close> (7.4.4) is implied.\<close> 132 "[| evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF; 133 Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> 134 \<in> set evsSH |] 135 ==> Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> # evsSH \<in> tls" 136 137 | Certificate: 138 \<comment> \<open>SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.\<close> 139 "evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC \<in> tls" 140 141 | ClientKeyExch: 142 \<comment> \<open>CLIENT KEY EXCHANGE (7.4.7). 143 The client, A, chooses PMS, the PREMASTER SECRET. 144 She encrypts PMS using the supplied KB, which ought to be pubK B. 145 We assume \<^term>\<open>PMS \<notin> range PRF\<close> because a clash betweem the PMS 146 and another MASTER SECRET is highly unlikely (even though 147 both items have the same length, 48 bytes). 148 The Note event records in the trace that she knows PMS 149 (see REMARK at top).\<close> 150 "[| evsCX \<in> tls; Nonce PMS \<notin> used evsCX; PMS \<notin> range PRF; 151 Says B' A (certificate B KB) \<in> set evsCX |] 152 ==> Says A B (Crypt KB (Nonce PMS)) 153 # Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> 154 # evsCX \<in> tls" 155 156 | CertVerify: 157 \<comment> \<open>The optional Certificate Verify (7.4.8) message contains the 158 specific components listed in the security analysis, F.1.1.2. 159 It adds the pre-master-secret, which is also essential! 160 Checking the signature, which is the only use of A's certificate, 161 assures B of A's presence\<close> 162 "[| evsCV \<in> tls; 163 Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCV; 164 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCV |] 165 ==> Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>)) 166 # evsCV \<in> tls" 167 168 \<comment> \<open>Finally come the FINISHED messages (7.4.8), confirming PA and PB 169 among other things. The master-secret is PRF(PMS,NA,NB). 170 Either party may send its message first.\<close> 171 172 | ClientFinished: 173 \<comment> \<open>The occurrence of \<open>Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>\<close> stops the 174 rule's applying when the Spy has satisfied the \<open>Says A B\<close> by 175 repaying messages sent by the true client; in that case, the 176 Spy does not know PMS and could not send ClientFinished. One 177 could simply put \<^term>\<open>A\<noteq>Spy\<close> into the rule, but one should not 178 expect the spy to be well-behaved.\<close> 179 "[| evsCF \<in> tls; 180 Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> 181 \<in> set evsCF; 182 Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCF; 183 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCF; 184 M = PRF(PMS,NA,NB) |] 185 ==> Says A B (Crypt (clientK(NA,NB,M)) 186 (Hash\<lbrace>Number SID, Nonce M, 187 Nonce NA, Number PA, Agent A, 188 Nonce NB, Number PB, Agent B\<rbrace>)) 189 # evsCF \<in> tls" 190 191 | ServerFinished: 192 \<comment> \<open>Keeping A' and A'' distinct means B cannot even check that the 193 two messages originate from the same source.\<close> 194 "[| evsSF \<in> tls; 195 Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> 196 \<in> set evsSF; 197 Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSF; 198 Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSF; 199 M = PRF(PMS,NA,NB) |] 200 ==> Says B A (Crypt (serverK(NA,NB,M)) 201 (Hash\<lbrace>Number SID, Nonce M, 202 Nonce NA, Number PA, Agent A, 203 Nonce NB, Number PB, Agent B\<rbrace>)) 204 # evsSF \<in> tls" 205 206 | ClientAccepts: 207 \<comment> \<open>Having transmitted ClientFinished and received an identical 208 message encrypted with serverK, the client stores the parameters 209 needed to resume this session. The "Notes A ..." premise is 210 used to prove \<open>Notes_master_imp_Crypt_PMS\<close>.\<close> 211 "[| evsCA \<in> tls; 212 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCA; 213 M = PRF(PMS,NA,NB); 214 X = Hash\<lbrace>Number SID, Nonce M, 215 Nonce NA, Number PA, Agent A, 216 Nonce NB, Number PB, Agent B\<rbrace>; 217 Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA; 218 Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |] 219 ==> 220 Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsCA \<in> tls" 221 222 | ServerAccepts: 223 \<comment> \<open>Having transmitted ServerFinished and received an identical 224 message encrypted with clientK, the server stores the parameters 225 needed to resume this session. The "Says A'' B ..." premise is 226 used to prove \<open>Notes_master_imp_Crypt_PMS\<close>.\<close> 227 "[| evsSA \<in> tls; 228 A \<noteq> B; 229 Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA; 230 M = PRF(PMS,NA,NB); 231 X = Hash\<lbrace>Number SID, Nonce M, 232 Nonce NA, Number PA, Agent A, 233 Nonce NB, Number PB, Agent B\<rbrace>; 234 Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA; 235 Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |] 236 ==> 237 Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsSA \<in> tls" 238 239 | ClientResume: 240 \<comment> \<open>If A recalls the \<open>SESSION_ID\<close>, then she sends a FINISHED 241 message using the new nonces and stored MASTER SECRET.\<close> 242 "[| evsCR \<in> tls; 243 Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> \<in> set evsCR; 244 Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCR; 245 Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsCR |] 246 ==> Says A B (Crypt (clientK(NA,NB,M)) 247 (Hash\<lbrace>Number SID, Nonce M, 248 Nonce NA, Number PA, Agent A, 249 Nonce NB, Number PB, Agent B\<rbrace>)) 250 # evsCR \<in> tls" 251 252 | ServerResume: 253 \<comment> \<open>Resumption (7.3): If B finds the \<open>SESSION_ID\<close> then he can 254 send a FINISHED message using the recovered MASTER SECRET\<close> 255 "[| evsSR \<in> tls; 256 Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace> \<in> set evsSR; 257 Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSR; 258 Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsSR |] 259 ==> Says B A (Crypt (serverK(NA,NB,M)) 260 (Hash\<lbrace>Number SID, Nonce M, 261 Nonce NA, Number PA, Agent A, 262 Nonce NB, Number PB, Agent B\<rbrace>)) # evsSR 263 \<in> tls" 264 265 | Oops: 266 \<comment> \<open>The most plausible compromise is of an old session key. Losing 267 the MASTER SECRET or PREMASTER SECRET is more serious but 268 rather unlikely. The assumption \<^term>\<open>A\<noteq>Spy\<close> is essential: 269 otherwise the Spy could learn session keys merely by 270 replaying messages!\<close> 271 "[| evso \<in> tls; A \<noteq> Spy; 272 Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |] 273 ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso \<in> tls" 274 275(* 276Protocol goals: 277* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two 278 parties (though A is not necessarily authenticated). 279 280* B upon receiving CertVerify knows that A is present (But this 281 message is optional!) 282 283* A upon receiving ServerFinished knows that B is present 284 285* Each party who has received a FINISHED message can trust that the other 286 party agrees on all message components, including PA and PB (thus foiling 287 rollback attacks). 288*) 289 290declare Says_imp_knows_Spy [THEN analz.Inj, dest] 291declare parts.Body [dest] 292declare analz_into_parts [dest] 293declare Fake_parts_insert_in_Un [dest] 294 295 296text\<open>Automatically unfold the definition of "certificate"\<close> 297declare certificate_def [simp] 298 299text\<open>Injectiveness of key-generating functions\<close> 300declare inj_PRF [THEN inj_eq, iff] 301declare inj_sessionK [THEN inj_eq, iff] 302declare isSym_sessionK [simp] 303 304 305(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***) 306 307lemma pubK_neq_sessionK [iff]: "publicKey b A \<noteq> sessionK arg" 308by (simp add: symKeys_neq_imp_neq) 309 310declare pubK_neq_sessionK [THEN not_sym, iff] 311 312lemma priK_neq_sessionK [iff]: "invKey (publicKey b A) \<noteq> sessionK arg" 313by (simp add: symKeys_neq_imp_neq) 314 315declare priK_neq_sessionK [THEN not_sym, iff] 316 317lemmas keys_distinct = pubK_neq_sessionK priK_neq_sessionK 318 319 320subsection\<open>Protocol Proofs\<close> 321 322text\<open>Possibility properties state that some traces run the protocol to the 323end. Four paths and 12 rules are considered.\<close> 324 325 326(** These proofs assume that the Nonce_supply nonces 327 (which have the form @ N. Nonce N \<notin> used evs) 328 lie outside the range of PRF. It seems reasonable, but as it is needed 329 only for the possibility theorems, it is not taken as an axiom. 330**) 331 332 333text\<open>Possibility property ending with ClientAccepts.\<close> 334lemma "[| \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |] 335 ==> \<exists>SID M. \<exists>evs \<in> tls. 336 Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs" 337apply (intro exI bexI) 338apply (rule_tac [2] tls.Nil 339 [THEN tls.ClientHello, THEN tls.ServerHello, 340 THEN tls.Certificate, THEN tls.ClientKeyExch, 341 THEN tls.ClientFinished, THEN tls.ServerFinished, 342 THEN tls.ClientAccepts], possibility, blast+) 343done 344 345 346text\<open>And one for ServerAccepts. Either FINISHED message may come first.\<close> 347lemma "[| \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |] 348 ==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls. 349 Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs" 350apply (intro exI bexI) 351apply (rule_tac [2] tls.Nil 352 [THEN tls.ClientHello, THEN tls.ServerHello, 353 THEN tls.Certificate, THEN tls.ClientKeyExch, 354 THEN tls.ServerFinished, THEN tls.ClientFinished, 355 THEN tls.ServerAccepts], possibility, blast+) 356done 357 358 359text\<open>Another one, for CertVerify (which is optional)\<close> 360lemma "[| \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |] 361 ==> \<exists>NB PMS. \<exists>evs \<in> tls. 362 Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>)) 363 \<in> set evs" 364apply (intro exI bexI) 365apply (rule_tac [2] tls.Nil 366 [THEN tls.ClientHello, THEN tls.ServerHello, 367 THEN tls.Certificate, THEN tls.ClientKeyExch, 368 THEN tls.CertVerify], possibility, blast+) 369done 370 371 372text\<open>Another one, for session resumption (both ServerResume and ClientResume). 373 NO tls.Nil here: we refer to a previous session, not the empty trace.\<close> 374lemma "[| evs0 \<in> tls; 375 Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0; 376 Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0; 377 \<forall>evs. (SOME N. Nonce N \<notin> used evs) \<notin> range PRF; 378 A \<noteq> B |] 379 ==> \<exists>NA PA NB PB X. \<exists>evs \<in> tls. 380 X = Hash\<lbrace>Number SID, Nonce M, 381 Nonce NA, Number PA, Agent A, 382 Nonce NB, Number PB, Agent B\<rbrace> \<and> 383 Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evs \<and> 384 Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evs" 385apply (intro exI bexI) 386apply (rule_tac [2] tls.ClientHello 387 [THEN tls.ServerHello, 388 THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+) 389done 390 391 392subsection\<open>Inductive proofs about tls\<close> 393 394 395(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY 396 sends messages containing X! **) 397 398text\<open>Spy never sees a good agent's private key!\<close> 399lemma Spy_see_priK [simp]: 400 "evs \<in> tls ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)" 401by (erule tls.induct, force, simp_all, blast) 402 403lemma Spy_analz_priK [simp]: 404 "evs \<in> tls ==> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)" 405by auto 406 407lemma Spy_see_priK_D [dest!]: 408 "[|Key (privateKey b A) \<in> parts (knows Spy evs); evs \<in> tls|] ==> A \<in> bad" 409by (blast dest: Spy_see_priK) 410 411 412text\<open>This lemma says that no false certificates exist. One might extend the 413 model to include bogus certificates for the agents, but there seems 414 little point in doing so: the loss of their private keys is a worse 415 breach of security.\<close> 416lemma certificate_valid: 417 "[| certificate B KB \<in> parts (spies evs); evs \<in> tls |] ==> KB = pubK B" 418apply (erule rev_mp) 419apply (erule tls.induct, force, simp_all, blast) 420done 421 422lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid] 423 424 425subsubsection\<open>Properties of items found in Notes\<close> 426 427lemma Notes_Crypt_parts_spies: 428 "[| Notes A \<lbrace>Agent B, X\<rbrace> \<in> set evs; evs \<in> tls |] 429 ==> Crypt (pubK B) X \<in> parts (spies evs)" 430apply (erule rev_mp) 431apply (erule tls.induct, 432 frule_tac [7] CX_KB_is_pubKB, force, simp_all) 433apply (blast intro: parts_insertI) 434done 435 436text\<open>C may be either A or B\<close> 437lemma Notes_master_imp_Crypt_PMS: 438 "[| Notes C \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs; 439 evs \<in> tls |] 440 ==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)" 441apply (erule rev_mp) 442apply (erule tls.induct, force, simp_all) 443txt\<open>Fake\<close> 444apply (blast intro: parts_insertI) 445txt\<open>Client, Server Accept\<close> 446apply (blast dest!: Notes_Crypt_parts_spies)+ 447done 448 449text\<open>Compared with the theorem above, both premise and conclusion are stronger\<close> 450lemma Notes_master_imp_Notes_PMS: 451 "[| Notes A \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs; 452 evs \<in> tls |] 453 ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs" 454apply (erule rev_mp) 455apply (erule tls.induct, force, simp_all) 456txt\<open>ServerAccepts\<close> 457apply blast 458done 459 460 461subsubsection\<open>Protocol goal: if B receives CertVerify, then A sent it\<close> 462 463text\<open>B can check A's signature if he has received A's certificate.\<close> 464lemma TrustCertVerify_lemma: 465 "[| X \<in> parts (spies evs); 466 X = Crypt (priK A) (Hash\<lbrace>nb, Agent B, pms\<rbrace>); 467 evs \<in> tls; A \<notin> bad |] 468 ==> Says A B X \<in> set evs" 469apply (erule rev_mp, erule ssubst) 470apply (erule tls.induct, force, simp_all, blast) 471done 472 473text\<open>Final version: B checks X using the distributed KA instead of priK A\<close> 474lemma TrustCertVerify: 475 "[| X \<in> parts (spies evs); 476 X = Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, pms\<rbrace>); 477 certificate A KA \<in> parts (spies evs); 478 evs \<in> tls; A \<notin> bad |] 479 ==> Says A B X \<in> set evs" 480by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma) 481 482 483text\<open>If CertVerify is present then A has chosen PMS.\<close> 484lemma UseCertVerify_lemma: 485 "[| Crypt (priK A) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>) \<in> parts (spies evs); 486 evs \<in> tls; A \<notin> bad |] 487 ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs" 488apply (erule rev_mp) 489apply (erule tls.induct, force, simp_all, blast) 490done 491 492text\<open>Final version using the distributed KA instead of priK A\<close> 493lemma UseCertVerify: 494 "[| Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>) 495 \<in> parts (spies evs); 496 certificate A KA \<in> parts (spies evs); 497 evs \<in> tls; A \<notin> bad |] 498 ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs" 499by (blast dest!: certificate_valid intro!: UseCertVerify_lemma) 500 501 502lemma no_Notes_A_PRF [simp]: 503 "evs \<in> tls ==> Notes A \<lbrace>Agent B, Nonce (PRF x)\<rbrace> \<notin> set evs" 504apply (erule tls.induct, force, simp_all) 505txt\<open>ClientKeyExch: PMS is assumed to differ from any PRF.\<close> 506apply blast 507done 508 509 510lemma MS_imp_PMS [dest!]: 511 "[| Nonce (PRF (PMS,NA,NB)) \<in> parts (spies evs); evs \<in> tls |] 512 ==> Nonce PMS \<in> parts (spies evs)" 513apply (erule rev_mp) 514apply (erule tls.induct, force, simp_all) 515txt\<open>Fake\<close> 516apply (blast intro: parts_insertI) 517txt\<open>Easy, e.g. by freshness\<close> 518apply (blast dest: Notes_Crypt_parts_spies)+ 519done 520 521 522 523 524subsubsection\<open>Unicity results for PMS, the pre-master-secret\<close> 525 526text\<open>PMS determines B.\<close> 527lemma Crypt_unique_PMS: 528 "[| Crypt(pubK B) (Nonce PMS) \<in> parts (spies evs); 529 Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs); 530 Nonce PMS \<notin> analz (spies evs); 531 evs \<in> tls |] 532 ==> B=B'" 533apply (erule rev_mp, erule rev_mp, erule rev_mp) 534apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp)) 535txt\<open>Fake, ClientKeyExch\<close> 536apply blast+ 537done 538 539 540(** It is frustrating that we need two versions of the unicity results. 541 But Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> determines both A and B. Sometimes 542 we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which 543 determines B alone, and only if PMS is secret. 544**) 545 546text\<open>In A's internal Note, PMS determines A and B.\<close> 547lemma Notes_unique_PMS: 548 "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs; 549 Notes A' \<lbrace>Agent B', Nonce PMS\<rbrace> \<in> set evs; 550 evs \<in> tls |] 551 ==> A=A' \<and> B=B'" 552apply (erule rev_mp, erule rev_mp) 553apply (erule tls.induct, force, simp_all) 554txt\<open>ClientKeyExch\<close> 555apply (blast dest!: Notes_Crypt_parts_spies) 556done 557 558 559subsection\<open>Secrecy Theorems\<close> 560 561text\<open>Key compromise lemma needed to prove \<^term>\<open>analz_image_keys\<close>. 562 No collection of keys can help the spy get new private keys.\<close> 563lemma analz_image_priK [rule_format]: 564 "evs \<in> tls 565 ==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK \<union> (spies evs))) = 566 (priK B \<in> KK | B \<in> bad)" 567apply (erule tls.induct) 568apply (simp_all (no_asm_simp) 569 del: image_insert 570 add: image_Un [THEN sym] 571 insert_Key_image Un_assoc [THEN sym]) 572txt\<open>Fake\<close> 573apply spy_analz 574done 575 576 577text\<open>slightly speeds up the big simplification below\<close> 578lemma range_sessionkeys_not_priK: 579 "KK \<subseteq> range sessionK \<Longrightarrow> priK B \<notin> KK" 580by blast 581 582 583text\<open>Lemma for the trivial direction of the if-and-only-if\<close> 584lemma analz_image_keys_lemma: 585 "(X \<in> analz (G \<union> H)) \<longrightarrow> (X \<in> analz H) ==> 586 (X \<in> analz (G \<union> H)) = (X \<in> analz H)" 587by (blast intro: analz_mono [THEN subsetD]) 588 589(** Strangely, the following version doesn't work: 590\<forall>Z. (Nonce N \<in> analz (Key`(sessionK`Z) \<union> (spies evs))) = 591 (Nonce N \<in> analz (spies evs))" 592**) 593 594lemma analz_image_keys [rule_format]: 595 "evs \<in> tls ==> 596 \<forall>KK. KK \<subseteq> range sessionK \<longrightarrow> 597 (Nonce N \<in> analz (Key`KK \<union> (spies evs))) = 598 (Nonce N \<in> analz (spies evs))" 599apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 600apply (safe del: iffI) 601apply (safe del: impI iffI intro!: analz_image_keys_lemma) 602apply (simp_all (no_asm_simp) (*faster*) 603 del: image_insert imp_disjL (*reduces blow-up*) 604 add: image_Un [THEN sym] Un_assoc [THEN sym] 605 insert_Key_singleton 606 range_sessionkeys_not_priK analz_image_priK) 607apply (simp_all add: insert_absorb) 608txt\<open>Fake\<close> 609apply spy_analz 610done 611 612text\<open>Knowing some session keys is no help in getting new nonces\<close> 613lemma analz_insert_key [simp]: 614 "evs \<in> tls ==> 615 (Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) = 616 (Nonce N \<in> analz (spies evs))" 617by (simp del: image_insert 618 add: insert_Key_singleton analz_image_keys) 619 620 621subsubsection\<open>Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure\<close> 622 623(** Some lemmas about session keys, comprising clientK and serverK **) 624 625 626text\<open>Lemma: session keys are never used if PMS is fresh. 627 Nonces don't have to agree, allowing session resumption. 628 Converse doesn't hold; revealing PMS doesn't force the keys to be sent. 629 THEY ARE NOT SUITABLE AS SAFE ELIM RULES.\<close> 630lemma PMS_lemma: 631 "[| Nonce PMS \<notin> parts (spies evs); 632 K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role); 633 evs \<in> tls |] 634 ==> Key K \<notin> parts (spies evs) \<and> (\<forall>Y. Crypt K Y \<notin> parts (spies evs))" 635apply (erule rev_mp, erule ssubst) 636apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 637apply (force, simp_all (no_asm_simp)) 638txt\<open>Fake\<close> 639apply (blast intro: parts_insertI) 640txt\<open>SpyKeys\<close> 641apply blast 642txt\<open>Many others\<close> 643apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+ 644done 645 646lemma PMS_sessionK_not_spied: 647 "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) \<in> parts (spies evs); 648 evs \<in> tls |] 649 ==> Nonce PMS \<in> parts (spies evs)" 650by (blast dest: PMS_lemma) 651 652lemma PMS_Crypt_sessionK_not_spied: 653 "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y 654 \<in> parts (spies evs); evs \<in> tls |] 655 ==> Nonce PMS \<in> parts (spies evs)" 656by (blast dest: PMS_lemma) 657 658text\<open>Write keys are never sent if M (MASTER SECRET) is secure. 659 Converse fails; betraying M doesn't force the keys to be sent! 660 The strong Oops condition can be weakened later by unicity reasoning, 661 with some effort. 662 NO LONGER USED: see \<open>clientK_not_spied\<close> and \<open>serverK_not_spied\<close>\<close> 663lemma sessionK_not_spied: 664 "[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs; 665 Nonce M \<notin> analz (spies evs); evs \<in> tls |] 666 ==> Key (sessionK((NA,NB,M),role)) \<notin> parts (spies evs)" 667apply (erule rev_mp, erule rev_mp) 668apply (erule tls.induct, analz_mono_contra) 669apply (force, simp_all (no_asm_simp)) 670txt\<open>Fake, SpyKeys\<close> 671apply blast+ 672done 673 674 675text\<open>If A sends ClientKeyExch to an honest B, then the PMS will stay secret.\<close> 676lemma Spy_not_see_PMS: 677 "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs; 678 evs \<in> tls; A \<notin> bad; B \<notin> bad |] 679 ==> Nonce PMS \<notin> analz (spies evs)" 680apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 681apply (force, simp_all (no_asm_simp)) 682txt\<open>Fake\<close> 683apply spy_analz 684txt\<open>SpyKeys\<close> 685apply force 686apply (simp_all add: insert_absorb) 687txt\<open>ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning\<close> 688apply (blast dest: Notes_Crypt_parts_spies) 689apply (blast dest: Notes_Crypt_parts_spies) 690apply (blast dest: Notes_Crypt_parts_spies) 691txt\<open>ClientAccepts and ServerAccepts: because \<^term>\<open>PMS \<notin> range PRF\<close>\<close> 692apply force+ 693done 694 695 696text\<open>If A sends ClientKeyExch to an honest B, then the MASTER SECRET 697 will stay secret.\<close> 698lemma Spy_not_see_MS: 699 "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs; 700 evs \<in> tls; A \<notin> bad; B \<notin> bad |] 701 ==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)" 702apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 703apply (force, simp_all (no_asm_simp)) 704txt\<open>Fake\<close> 705apply spy_analz 706txt\<open>SpyKeys: by secrecy of the PMS, Spy cannot make the MS\<close> 707apply (blast dest!: Spy_not_see_PMS) 708apply (simp_all add: insert_absorb) 709txt\<open>ClientAccepts and ServerAccepts: because PMS was already visible; 710 others, freshness etc.\<close> 711apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS 712 Notes_imp_knows_Spy [THEN analz.Inj])+ 713done 714 715 716 717subsubsection\<open>Weakening the Oops conditions for leakage of clientK\<close> 718 719text\<open>If A created PMS then nobody else (except the Spy in replays) 720 would send a message using a clientK generated from that PMS.\<close> 721lemma Says_clientK_unique: 722 "[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs; 723 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs; 724 evs \<in> tls; A' \<noteq> Spy |] 725 ==> A = A'" 726apply (erule rev_mp, erule rev_mp) 727apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 728apply (force, simp_all) 729txt\<open>ClientKeyExch\<close> 730apply (blast dest!: PMS_Crypt_sessionK_not_spied) 731txt\<open>ClientFinished, ClientResume: by unicity of PMS\<close> 732apply (blast dest!: Notes_master_imp_Notes_PMS 733 intro: Notes_unique_PMS [THEN conjunct1])+ 734done 735 736 737text\<open>If A created PMS and has not leaked her clientK to the Spy, 738 then it is completely secure: not even in parts!\<close> 739lemma clientK_not_spied: 740 "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs; 741 Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs; 742 A \<notin> bad; B \<notin> bad; 743 evs \<in> tls |] 744 ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)" 745apply (erule rev_mp, erule rev_mp) 746apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 747apply (force, simp_all (no_asm_simp)) 748txt\<open>ClientKeyExch\<close> 749apply blast 750txt\<open>SpyKeys\<close> 751apply (blast dest!: Spy_not_see_MS) 752txt\<open>ClientKeyExch\<close> 753apply (blast dest!: PMS_sessionK_not_spied) 754txt\<open>Oops\<close> 755apply (blast intro: Says_clientK_unique) 756done 757 758 759subsubsection\<open>Weakening the Oops conditions for leakage of serverK\<close> 760 761text\<open>If A created PMS for B, then nobody other than B or the Spy would 762 send a message using a serverK generated from that PMS.\<close> 763lemma Says_serverK_unique: 764 "[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs; 765 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs; 766 evs \<in> tls; A \<notin> bad; B \<notin> bad; B' \<noteq> Spy |] 767 ==> B = B'" 768apply (erule rev_mp, erule rev_mp) 769apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 770apply (force, simp_all) 771txt\<open>ClientKeyExch\<close> 772apply (blast dest!: PMS_Crypt_sessionK_not_spied) 773txt\<open>ServerResume, ServerFinished: by unicity of PMS\<close> 774apply (blast dest!: Notes_master_imp_Crypt_PMS 775 dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+ 776done 777 778 779text\<open>If A created PMS for B, and B has not leaked his serverK to the Spy, 780 then it is completely secure: not even in parts!\<close> 781lemma serverK_not_spied: 782 "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs; 783 Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs; 784 A \<notin> bad; B \<notin> bad; evs \<in> tls |] 785 ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)" 786apply (erule rev_mp, erule rev_mp) 787apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 788apply (force, simp_all (no_asm_simp)) 789txt\<open>Fake\<close> 790apply blast 791txt\<open>SpyKeys\<close> 792apply (blast dest!: Spy_not_see_MS) 793txt\<open>ClientKeyExch\<close> 794apply (blast dest!: PMS_sessionK_not_spied) 795txt\<open>Oops\<close> 796apply (blast intro: Says_serverK_unique) 797done 798 799 800subsubsection\<open>Protocol goals: if A receives ServerFinished, then B is present 801 and has used the quoted values PA, PB, etc. Note that it is up to A 802 to compare PA with what she originally sent.\<close> 803 804text\<open>The mention of her name (A) in X assures A that B knows who she is.\<close> 805lemma TrustServerFinished [rule_format]: 806 "[| X = Crypt (serverK(Na,Nb,M)) 807 (Hash\<lbrace>Number SID, Nonce M, 808 Nonce Na, Number PA, Agent A, 809 Nonce Nb, Number PB, Agent B\<rbrace>); 810 M = PRF(PMS,NA,NB); 811 evs \<in> tls; A \<notin> bad; B \<notin> bad |] 812 ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs \<longrightarrow> 813 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs \<longrightarrow> 814 X \<in> parts (spies evs) \<longrightarrow> Says B A X \<in> set evs" 815apply (erule ssubst)+ 816apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 817apply (force, simp_all (no_asm_simp)) 818txt\<open>Fake: the Spy doesn't have the critical session key!\<close> 819apply (blast dest: serverK_not_spied) 820txt\<open>ClientKeyExch\<close> 821apply (blast dest!: PMS_Crypt_sessionK_not_spied) 822done 823 824text\<open>This version refers not to ServerFinished but to any message from B. 825 We don't assume B has received CertVerify, and an intruder could 826 have changed A's identity in all other messages, so we can't be sure 827 that B sends his message to A. If CLIENT KEY EXCHANGE were augmented 828 to bind A's identity with PMS, then we could replace A' by A below.\<close> 829lemma TrustServerMsg [rule_format]: 830 "[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |] 831 ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs \<longrightarrow> 832 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs \<longrightarrow> 833 Crypt (serverK(Na,Nb,M)) Y \<in> parts (spies evs) \<longrightarrow> 834 (\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \<in> set evs)" 835apply (erule ssubst) 836apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 837apply (force, simp_all (no_asm_simp) add: ex_disj_distrib) 838txt\<open>Fake: the Spy doesn't have the critical session key!\<close> 839apply (blast dest: serverK_not_spied) 840txt\<open>ClientKeyExch\<close> 841apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied) 842txt\<open>ServerResume, ServerFinished: by unicity of PMS\<close> 843apply (blast dest!: Notes_master_imp_Crypt_PMS 844 dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+ 845done 846 847 848subsubsection\<open>Protocol goal: if B receives any message encrypted with clientK 849 then A has sent it\<close> 850 851text\<open>ASSUMING that A chose PMS. Authentication is 852 assumed here; B cannot verify it. But if the message is 853 ClientFinished, then B can then check the quoted values PA, PB, etc.\<close> 854 855lemma TrustClientMsg [rule_format]: 856 "[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |] 857 ==> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs \<longrightarrow> 858 Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs \<longrightarrow> 859 Crypt (clientK(Na,Nb,M)) Y \<in> parts (spies evs) \<longrightarrow> 860 Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs" 861apply (erule ssubst) 862apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 863apply (force, simp_all (no_asm_simp)) 864txt\<open>Fake: the Spy doesn't have the critical session key!\<close> 865apply (blast dest: clientK_not_spied) 866txt\<open>ClientKeyExch\<close> 867apply (blast dest!: PMS_Crypt_sessionK_not_spied) 868txt\<open>ClientFinished, ClientResume: by unicity of PMS\<close> 869apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+ 870done 871 872 873subsubsection\<open>Protocol goal: if B receives ClientFinished, and if B is able to 874 check a CertVerify from A, then A has used the quoted 875 values PA, PB, etc. Even this one requires A to be uncompromised.\<close> 876lemma AuthClientFinished: 877 "[| M = PRF(PMS,NA,NB); 878 Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs; 879 Says A' B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs; 880 certificate A KA \<in> parts (spies evs); 881 Says A'' B (Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>)) 882 \<in> set evs; 883 evs \<in> tls; A \<notin> bad; B \<notin> bad |] 884 ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs" 885by (blast intro!: TrustClientMsg UseCertVerify) 886 887(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) 888(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*) 889(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*) 890(*30/9/97: loads in 476s, after removing unused theorems*) 891(*30/9/97: loads in 448s, after fixing ServerResume*) 892 893(*08/9/97: loads in 189s (pike), after much reorganization, 894 back to 621s on albatross?*) 895 896(*10/2/99: loads in 139s (pike) 897 down to 433s on albatross*) 898 899(*5/5/01: conversion to Isar script 900 loads in 137s (perch) 901 the last ML version loaded in 122s on perch, a 600MHz machine: 902 twice as fast as pike. No idea why it's so much slower! 903 The Isar script is slower still, perhaps because simp_all simplifies 904 the assumptions be default. 905*) 906 907(*20/11/11: loads in 5.8s elapses time, 9.3s CPU time on dual-core laptop*) 908 909end 910