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