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