src/HOL/Auth/TLS.thy
author paulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13922 75ae4244a596
permissions -rw-r--r--
tidying of Isar scripts
     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], possibility, blast+)
   322 done
   323 
   324 
   325 (*And one for ServerAccepts.  Either FINISHED message may come first.*)
   326 lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
   327       ==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
   328            Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
   329 apply (intro exI bexI)
   330 apply (rule_tac [2] tls.Nil
   331                     [THEN tls.ClientHello, THEN tls.ServerHello,
   332                      THEN tls.Certificate, THEN tls.ClientKeyExch,
   333                      THEN tls.ServerFinished, THEN tls.ClientFinished, 
   334                      THEN tls.ServerAccepts], possibility, blast+)
   335 done
   336 
   337 
   338 (*Another one, for CertVerify (which is optional)*)
   339 lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B |]
   340        ==> \<exists>NB PMS. \<exists>evs \<in> tls.
   341               Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) 
   342                 \<in> set evs"
   343 apply (intro exI bexI)
   344 apply (rule_tac [2] tls.Nil
   345                     [THEN tls.ClientHello, THEN tls.ServerHello,
   346                      THEN tls.Certificate, THEN tls.ClientKeyExch,
   347                      THEN tls.CertVerify], possibility, blast+)
   348 done
   349 
   350 
   351 (*Another one, for session resumption (both ServerResume and ClientResume).
   352   NO tls.Nil here: we refer to a previous session, not the empty trace.*)
   353 lemma "[| evs0 \<in> tls;
   354           Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
   355           Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
   356           \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;
   357           A \<noteq> B |]
   358       ==> \<exists>NA PA NB PB X. \<exists>evs \<in> tls.
   359 		X = Hash{|Number SID, Nonce M,
   360 			  Nonce NA, Number PA, Agent A,
   361 			  Nonce NB, Number PB, Agent B|}  &
   362 		Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evs  &
   363 		Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evs"
   364 apply (intro exI bexI)
   365 apply (rule_tac [2] tls.ClientHello
   366                     [THEN tls.ServerHello,
   367                      THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+)
   368 done
   369 
   370 
   371 (**** Inductive proofs about tls ****)
   372 
   373 
   374 (*Induction for regularity theorems.  If induction formula has the form
   375    X \<notin> analz (spies evs) --> ... then it shortens the proof by discarding
   376    needless information about analz (insert X (spies evs))  
   377 fun parts_induct_tac i =
   378     etac tls.induct i
   379     THEN REPEAT (FIRSTGOAL analz_mono_contra_tac)
   380     THEN Force_tac i THEN
   381     ALLGOALS Asm_simp_tac
   382 *)
   383 
   384 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
   385     sends messages containing X! **)
   386 
   387 (*Spy never sees a good agent's private key!*)
   388 lemma Spy_see_priK [simp]:
   389      "evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
   390 apply (erule tls.induct, force, simp_all, blast)
   391 done
   392 
   393 lemma Spy_analz_priK [simp]:
   394      "evs \<in> tls ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
   395 by auto
   396 
   397 lemma Spy_see_priK_D [dest!]:
   398      "[|Key (priK A) \<in> parts (knows Spy evs);  evs \<in> tls|] ==> A \<in> bad"
   399 by (blast dest: Spy_see_priK)
   400 
   401 
   402 (*This lemma says that no false certificates exist.  One might extend the
   403   model to include bogus certificates for the agents, but there seems
   404   little point in doing so: the loss of their private keys is a worse
   405   breach of security.*)
   406 lemma certificate_valid:
   407     "[| certificate B KB \<in> parts (spies evs);  evs \<in> tls |] ==> KB = pubK B"
   408 apply (erule rev_mp)
   409 apply (erule tls.induct, force, simp_all, blast) 
   410 done
   411 
   412 lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
   413 
   414 
   415 (*** Properties of items found in Notes ***)
   416 
   417 lemma Notes_Crypt_parts_spies:
   418      "[| Notes A {|Agent B, X|} \<in> set evs;  evs \<in> tls |]
   419       ==> Crypt (pubK B) X \<in> parts (spies evs)"
   420 apply (erule rev_mp)
   421 apply (erule tls.induct, 
   422        frule_tac [7] CX_KB_is_pubKB, force, simp_all)
   423 apply (blast intro: parts_insertI)
   424 done
   425 
   426 (*C may be either A or B*)
   427 lemma Notes_master_imp_Crypt_PMS:
   428      "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
   429          evs \<in> tls |]
   430       ==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
   431 apply (erule rev_mp)
   432 apply (erule tls.induct, force, simp_all)
   433 (*Fake*)
   434 apply (blast intro: parts_insertI)
   435 (*Client, Server Accept*)
   436 apply (blast dest!: Notes_Crypt_parts_spies)+
   437 done
   438 
   439 (*Compared with the theorem above, both premise and conclusion are stronger*)
   440 lemma Notes_master_imp_Notes_PMS:
   441      "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
   442          evs \<in> tls |]
   443       ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
   444 apply (erule rev_mp)
   445 apply (erule tls.induct, force, simp_all)
   446 (*ServerAccepts*)
   447 apply blast
   448 done
   449 
   450 
   451 (*** Protocol goal: if B receives CertVerify, then A sent it ***)
   452 
   453 (*B can check A's signature if he has received A's certificate.*)
   454 lemma TrustCertVerify_lemma:
   455      "[| X \<in> parts (spies evs);
   456          X = Crypt (priK A) (Hash{|nb, Agent B, pms|});
   457          evs \<in> tls;  A \<notin> bad |]
   458       ==> Says A B X \<in> set evs"
   459 apply (erule rev_mp, erule ssubst)
   460 apply (erule tls.induct, force, simp_all, blast)
   461 done
   462 
   463 (*Final version: B checks X using the distributed KA instead of priK A*)
   464 lemma TrustCertVerify:
   465      "[| X \<in> parts (spies evs);
   466          X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});
   467          certificate A KA \<in> parts (spies evs);
   468          evs \<in> tls;  A \<notin> bad |]
   469       ==> Says A B X \<in> set evs"
   470 by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma)
   471 
   472 
   473 (*If CertVerify is present then A has chosen PMS.*)
   474 lemma UseCertVerify_lemma:
   475      "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \<in> parts (spies evs);
   476          evs \<in> tls;  A \<notin> bad |]
   477       ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
   478 apply (erule rev_mp)
   479 apply (erule tls.induct, force, simp_all, blast)
   480 done
   481 
   482 (*Final version using the distributed KA instead of priK A*)
   483 lemma UseCertVerify:
   484      "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})
   485            \<in> parts (spies evs);
   486          certificate A KA \<in> parts (spies evs);
   487          evs \<in> tls;  A \<notin> bad |]
   488       ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
   489 by (blast dest!: certificate_valid intro!: UseCertVerify_lemma)
   490 
   491 
   492 lemma no_Notes_A_PRF [simp]:
   493      "evs \<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \<notin> set evs"
   494 apply (erule tls.induct, force, simp_all)
   495 (*ClientKeyExch: PMS is assumed to differ from any PRF.*)
   496 apply blast
   497 done
   498 
   499 
   500 lemma MS_imp_PMS [dest!]:
   501      "[| Nonce (PRF (PMS,NA,NB)) \<in> parts (spies evs);  evs \<in> tls |]
   502       ==> Nonce PMS \<in> parts (spies evs)"
   503 apply (erule rev_mp)
   504 apply (erule tls.induct, force, simp_all)
   505 (*Fake*)
   506 apply (blast intro: parts_insertI)
   507 (*Easy, e.g. by freshness*)
   508 apply (blast dest: Notes_Crypt_parts_spies)+
   509 done
   510 
   511 
   512 
   513 
   514 (*** Unicity results for PMS, the pre-master-secret ***)
   515 
   516 (*PMS determines B.*)
   517 lemma Crypt_unique_PMS:
   518      "[| Crypt(pubK B)  (Nonce PMS) \<in> parts (spies evs);
   519          Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs);
   520          Nonce PMS \<notin> analz (spies evs);
   521          evs \<in> tls |]
   522       ==> B=B'"
   523 apply (erule rev_mp, erule rev_mp, erule rev_mp)
   524 apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp))
   525 (*Fake, ClientKeyExch*)
   526 apply blast+
   527 done
   528 
   529 
   530 (** It is frustrating that we need two versions of the unicity results.
   531     But Notes A {|Agent B, Nonce PMS|} determines both A and B.  Sometimes
   532     we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which
   533     determines B alone, and only if PMS is secret.
   534 **)
   535 
   536 (*In A's internal Note, PMS determines A and B.*)
   537 lemma Notes_unique_PMS:
   538      "[| Notes A  {|Agent B,  Nonce PMS|} \<in> set evs;
   539          Notes A' {|Agent B', Nonce PMS|} \<in> set evs;
   540          evs \<in> tls |]
   541       ==> A=A' & B=B'"
   542 apply (erule rev_mp, erule rev_mp)
   543 apply (erule tls.induct, force, simp_all)
   544 (*ClientKeyExch*)
   545 apply (blast dest!: Notes_Crypt_parts_spies)
   546 done
   547 
   548 
   549 (**** Secrecy Theorems ****)
   550 
   551 (*Key compromise lemma needed to prove analz_image_keys.
   552   No collection of keys can help the spy get new private keys.*)
   553 lemma analz_image_priK [rule_format]:
   554      "evs \<in> tls
   555       ==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK Un (spies evs))) =
   556           (priK B \<in> KK | B \<in> bad)"
   557 apply (erule tls.induct)
   558 apply (simp_all (no_asm_simp)
   559 		del: image_insert
   560                 add: image_Un [THEN sym]
   561                      insert_Key_image Un_assoc [THEN sym])
   562 (*Fake*)
   563 apply spy_analz
   564 done
   565 
   566 
   567 (*slightly speeds up the big simplification below*)
   568 lemma range_sessionkeys_not_priK:
   569      "KK <= range sessionK ==> priK B \<notin> KK"
   570 by blast
   571 
   572 
   573 (*Lemma for the trivial direction of the if-and-only-if*)
   574 lemma analz_image_keys_lemma:
   575      "(X \<in> analz (G Un H)) --> (X \<in> analz H)  ==>
   576       (X \<in> analz (G Un H))  =  (X \<in> analz H)"
   577 by (blast intro: analz_mono [THEN subsetD])
   578 
   579 (** Strangely, the following version doesn't work:
   580 \<forall>Z. (Nonce N \<in> analz (Key`(sessionK`Z) Un (spies evs))) =
   581     (Nonce N \<in> analz (spies evs))"
   582 **)
   583 
   584 lemma analz_image_keys [rule_format]:
   585      "evs \<in> tls ==>
   586       \<forall>KK. KK <= range sessionK -->
   587 	      (Nonce N \<in> analz (Key`KK Un (spies evs))) =
   588 	      (Nonce N \<in> analz (spies evs))"
   589 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   590 apply (safe del: iffI)
   591 apply (safe del: impI iffI intro!: analz_image_keys_lemma)
   592 apply (simp_all (no_asm_simp)               (*faster*)
   593                 del: image_insert imp_disjL (*reduces blow-up*)
   594 		add: image_Un [THEN sym]  Un_assoc [THEN sym]
   595 		     insert_Key_singleton
   596 		     range_sessionkeys_not_priK analz_image_priK)
   597 apply (simp_all add: insert_absorb)
   598 (*Fake*)
   599 apply spy_analz
   600 done
   601 
   602 (*Knowing some session keys is no help in getting new nonces*)
   603 lemma analz_insert_key [simp]:
   604      "evs \<in> tls ==>
   605       (Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) =
   606       (Nonce N \<in> analz (spies evs))"
   607 by (simp del: image_insert
   608          add: insert_Key_singleton analz_image_keys)
   609 
   610 
   611 (*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   612 
   613 (** Some lemmas about session keys, comprising clientK and serverK **)
   614 
   615 
   616 (*Lemma: session keys are never used if PMS is fresh.
   617   Nonces don't have to agree, allowing session resumption.
   618   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   619   THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
   620 lemma PMS_lemma:
   621      "[| Nonce PMS \<notin> parts (spies evs);
   622          K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role);
   623          evs \<in> tls |]
   624    ==> Key K \<notin> parts (spies evs) & (\<forall>Y. Crypt K Y \<notin> parts (spies evs))"
   625 apply (erule rev_mp, erule ssubst)
   626 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   627 apply (force, simp_all (no_asm_simp))
   628 (*Fake*)
   629 apply (blast intro: parts_insertI)
   630 (*SpyKeys*)
   631 apply blast
   632 (*Many others*)
   633 apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+
   634 done
   635 
   636 lemma PMS_sessionK_not_spied:
   637      "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) \<in> parts (spies evs);
   638          evs \<in> tls |]
   639       ==> Nonce PMS \<in> parts (spies evs)"
   640 by (blast dest: PMS_lemma)
   641 
   642 lemma PMS_Crypt_sessionK_not_spied:
   643      "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y
   644            \<in> parts (spies evs);  evs \<in> tls |]
   645       ==> Nonce PMS \<in> parts (spies evs)"
   646 by (blast dest: PMS_lemma)
   647 
   648 (*Write keys are never sent if M (MASTER SECRET) is secure.
   649   Converse fails; betraying M doesn't force the keys to be sent!
   650   The strong Oops condition can be weakened later by unicity reasoning,
   651   with some effort.
   652   NO LONGER USED: see clientK_not_spied and serverK_not_spied*)
   653 lemma sessionK_not_spied:
   654      "[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs;
   655          Nonce M \<notin> analz (spies evs);  evs \<in> tls |]
   656       ==> Key (sessionK((NA,NB,M),role)) \<notin> parts (spies evs)"
   657 apply (erule rev_mp, erule rev_mp)
   658 apply (erule tls.induct, analz_mono_contra)
   659 apply (force, simp_all (no_asm_simp))
   660 (*Fake, SpyKeys*)
   661 apply blast+
   662 done
   663 
   664 
   665 (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
   666 lemma Spy_not_see_PMS:
   667      "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   668          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   669       ==> Nonce PMS \<notin> analz (spies evs)"
   670 apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   671 apply (force, simp_all (no_asm_simp))
   672 (*Fake*)
   673 apply spy_analz
   674 (*SpyKeys*)
   675 apply force
   676 apply (simp_all add: insert_absorb) 
   677 (*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*)
   678 apply (blast dest: Notes_Crypt_parts_spies)
   679 apply (blast dest: Notes_Crypt_parts_spies)
   680 apply (blast dest: Notes_Crypt_parts_spies)
   681 (*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*)
   682 apply force+
   683 done
   684 
   685 
   686 (*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   687   will stay secret.*)
   688 lemma Spy_not_see_MS:
   689      "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   690          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   691       ==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
   692 apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   693 apply (force, simp_all (no_asm_simp))
   694 (*Fake*)
   695 apply spy_analz
   696 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   697 apply (blast dest!: Spy_not_see_PMS)
   698 apply (simp_all add: insert_absorb)
   699 (*ClientAccepts and ServerAccepts: because PMS was already visible;
   700   others, freshness etc.*)
   701 apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS 
   702                    Notes_imp_knows_Spy [THEN analz.Inj])+
   703 done
   704 
   705 
   706 
   707 (*** Weakening the Oops conditions for leakage of clientK ***)
   708 
   709 (*If A created PMS then nobody else (except the Spy in replays)
   710   would send a message using a clientK generated from that PMS.*)
   711 lemma Says_clientK_unique:
   712      "[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
   713          Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   714          evs \<in> tls;  A' \<noteq> Spy |]
   715       ==> A = A'"
   716 apply (erule rev_mp, erule rev_mp)
   717 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   718 apply (force, simp_all)
   719 (*ClientKeyExch*)
   720 apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   721 (*ClientFinished, ClientResume: by unicity of PMS*)
   722 apply (blast dest!: Notes_master_imp_Notes_PMS 
   723              intro: Notes_unique_PMS [THEN conjunct1])+
   724 done
   725 
   726 
   727 (*If A created PMS and has not leaked her clientK to the Spy,
   728   then it is completely secure: not even in parts!*)
   729 lemma clientK_not_spied:
   730      "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   731          Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
   732          A \<notin> bad;  B \<notin> bad;
   733          evs \<in> tls |]
   734       ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
   735 apply (erule rev_mp, erule rev_mp)
   736 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   737 apply (force, simp_all (no_asm_simp))
   738 (*ClientKeyExch*)
   739 apply blast 
   740 (*SpyKeys*)
   741 apply (blast dest!: Spy_not_see_MS)
   742 (*ClientKeyExch*)
   743 apply (blast dest!: PMS_sessionK_not_spied)
   744 (*Oops*)
   745 apply (blast intro: Says_clientK_unique)
   746 done
   747 
   748 
   749 (*** Weakening the Oops conditions for leakage of serverK ***)
   750 
   751 (*If A created PMS for B, then nobody other than B or the Spy would
   752   send a message using a serverK generated from that PMS.*)
   753 lemma Says_serverK_unique:
   754      "[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
   755          Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   756          evs \<in> tls;  A \<notin> bad;  B \<notin> bad;  B' \<noteq> Spy |]
   757       ==> B = B'"
   758 apply (erule rev_mp, erule rev_mp)
   759 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   760 apply (force, simp_all)
   761 (*ClientKeyExch*)
   762 apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   763 (*ServerResume, ServerFinished: by unicity of PMS*)
   764 apply (blast dest!: Notes_master_imp_Crypt_PMS 
   765              dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
   766 done
   767 
   768 
   769 (*If A created PMS for B, and B has not leaked his serverK to the Spy,
   770   then it is completely secure: not even in parts!*)
   771 lemma serverK_not_spied:
   772      "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
   773          Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
   774          A \<notin> bad;  B \<notin> bad;  evs \<in> tls |]
   775       ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
   776 apply (erule rev_mp, erule rev_mp)
   777 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   778 apply (force, simp_all (no_asm_simp))
   779 (*Fake*)
   780 apply blast 
   781 (*SpyKeys*)
   782 apply (blast dest!: Spy_not_see_MS)
   783 (*ClientKeyExch*)
   784 apply (blast dest!: PMS_sessionK_not_spied)
   785 (*Oops*)
   786 apply (blast intro: Says_serverK_unique)
   787 done
   788 
   789 
   790 (*** Protocol goals: if A receives ServerFinished, then B is present
   791      and has used the quoted values PA, PB, etc.  Note that it is up to A
   792      to compare PA with what she originally sent.
   793 ***)
   794 
   795 (*The mention of her name (A) in X assures A that B knows who she is.*)
   796 lemma TrustServerFinished [rule_format]:
   797      "[| X = Crypt (serverK(Na,Nb,M))
   798                (Hash{|Number SID, Nonce M,
   799                       Nonce Na, Number PA, Agent A,
   800                       Nonce Nb, Number PB, Agent B|});
   801          M = PRF(PMS,NA,NB);
   802          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   803       ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
   804           Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
   805           X \<in> parts (spies evs) --> Says B A X \<in> set evs"
   806 apply (erule ssubst)+
   807 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   808 apply (force, simp_all (no_asm_simp))
   809 (*Fake: the Spy doesn't have the critical session key!*)
   810 apply (blast dest: serverK_not_spied)
   811 (*ClientKeyExch*)
   812 apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   813 done
   814 
   815 (*This version refers not to ServerFinished but to any message from B.
   816   We don't assume B has received CertVerify, and an intruder could
   817   have changed A's identity in all other messages, so we can't be sure
   818   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   819   to bind A's identity with PMS, then we could replace A' by A below.*)
   820 lemma TrustServerMsg [rule_format]:
   821      "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   822       ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
   823           Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
   824           Crypt (serverK(Na,Nb,M)) Y \<in> parts (spies evs)  -->
   825           (\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \<in> set evs)"
   826 apply (erule ssubst)
   827 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   828 apply (force, simp_all (no_asm_simp) add: ex_disj_distrib)
   829 (*Fake: the Spy doesn't have the critical session key!*)
   830 apply (blast dest: serverK_not_spied)
   831 (*ClientKeyExch*)
   832 apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied)
   833 (*ServerResume, ServerFinished: by unicity of PMS*)
   834 apply (blast dest!: Notes_master_imp_Crypt_PMS 
   835              dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
   836 done
   837 
   838 
   839 (*** Protocol goal: if B receives any message encrypted with clientK
   840      then A has sent it, ASSUMING that A chose PMS.  Authentication is
   841      assumed here; B cannot verify it.  But if the message is
   842      ClientFinished, then B can then check the quoted values PA, PB, etc.
   843 ***)
   844 
   845 lemma TrustClientMsg [rule_format]:
   846      "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   847       ==> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs -->
   848           Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
   849           Crypt (clientK(Na,Nb,M)) Y \<in> parts (spies evs) -->
   850           Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
   851 apply (erule ssubst)
   852 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
   853 apply (force, simp_all (no_asm_simp))
   854 (*Fake: the Spy doesn't have the critical session key!*)
   855 apply (blast dest: clientK_not_spied)
   856 (*ClientKeyExch*)
   857 apply (blast dest!: PMS_Crypt_sessionK_not_spied)
   858 (*ClientFinished, ClientResume: by unicity of PMS*)
   859 apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+
   860 done
   861 
   862 
   863 (*** Protocol goal: if B receives ClientFinished, and if B is able to
   864      check a CertVerify from A, then A has used the quoted
   865      values PA, PB, etc.  Even this one requires A to be uncompromised.
   866  ***)
   867 lemma AuthClientFinished:
   868      "[| M = PRF(PMS,NA,NB);
   869          Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;
   870          Says A' B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs;
   871          certificate A KA \<in> parts (spies evs);
   872          Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))
   873            \<in> set evs;
   874          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
   875       ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
   876 by (blast intro!: TrustClientMsg UseCertVerify)
   877 
   878 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
   879 (*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
   880 (*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
   881 (*30/9/97: loads in 476s, after removing unused theorems*)
   882 (*30/9/97: loads in 448s, after fixing ServerResume*)
   883 
   884 (*08/9/97: loads in 189s (pike), after much reorganization,
   885            back to 621s on albatross?*)
   886 
   887 (*10/2/99: loads in 139s (pike)
   888            down to 433s on albatross*)
   889 
   890 (*5/5/01: conversion to Isar script
   891 	  loads in 137s (perch)
   892           the last ML version loaded in 122s on perch, a 600MHz machine:
   893 		twice as fast as pike.  No idea why it's so much slower!
   894 	  The Isar script is slower still, perhaps because simp_all simplifies
   895 	  the assumptions be default.
   896 *)
   897 
   898 end