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