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