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