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