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