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