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