src/HOL/Auth/TLS.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 6284 147db42c1009
child 11185 1b737b4c2108
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/TLS
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     2
    ID:         $Id$
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     5
3759
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
     6
Inductive relation "tls" for the TLS (Transport Layer Security) protocol.
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
     7
This protocol is essentially the same as SSL 3.0.
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
     8
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
     9
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    10
Allen, Transport Layer Security Working Group, 21 May 1997,
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    11
INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    12
to that memo.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    13
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    14
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    15
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    16
global signing authority.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    17
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    18
A is the client and B is the server, not to be confused with the constant
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    19
Server, who is in charge of all public keys.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    20
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    21
The model assumes that no fraudulent certificates are present, but it does
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    22
assume that some private keys are to the spy.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    23
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    24
REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientKeyExch,
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    25
CertVerify, ClientFinished to record that A knows M.  It is a note from A to
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    26
herself.  Nobody else can see it.  In ClientKeyExch, the Spy can substitute
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    27
his own certificate for A's, but he cannot replace A's note by one for himself.
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    28
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    29
The Note event avoids a weakness in the public-key model.  Each
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    30
agent's state is recorded as the trace of messages.  When the true client (A)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    31
invents PMS, he encrypts PMS with B's public key before sending it.  The model
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    32
does not distinguish the original occurrence of such a message from a replay.
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    33
In the shared-key model, the ability to encrypt implies the ability to
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    34
decrypt, so the problem does not arise.
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    35
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    36
Proofs would be simpler if ClientKeyExch included A's name within
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    37
Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    38
about that message (which B receives) and the stronger event
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    39
	Notes A {|Agent B, Nonce PMS|}.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    40
*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    41
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    42
TLS = Public + 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    43
5653
204083e3f368 changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents: 5434
diff changeset
    44
constdefs
204083e3f368 changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents: 5434
diff changeset
    45
  certificate      :: "[agent,key] => msg"
204083e3f368 changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents: 5434
diff changeset
    46
    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
204083e3f368 changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents: 5434
diff changeset
    47
6284
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
    48
datatype role = ClientRole | ServerRole
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
    49
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    50
consts
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    51
  (*Pseudo-random function of Section 5*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    52
  PRF  :: "nat*nat*nat => nat"
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    53
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
    54
  (*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
    55
    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
    56
    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
    57
    Session keys implicitly include MAC secrets.*)
6284
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
    58
  sessionK :: "(nat*nat*nat) * role => key"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    59
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    60
syntax
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    61
    clientK, serverK :: "nat*nat*nat => key"
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    62
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    63
translations
6284
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
    64
  "clientK X" == "sessionK(X, ClientRole)"
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
    65
  "serverK X" == "sessionK(X, ServerRole)"
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    66
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    67
rules
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    68
  (*the pseudo-random function is collision-free*)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    69
  inj_PRF       "inj PRF"	
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    70
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    71
  (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    72
  inj_sessionK  "inj sessionK"	
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    73
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    74
  (*sessionK makes symmetric keys*)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    75
  isSym_sessionK "isSymKey (sessionK nonces)"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    76
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    77
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    78
consts    tls :: event list set
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    79
inductive tls
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    80
  intrs 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    81
    Nil  (*Initial trace is empty*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    82
         "[]: tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    83
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    84
    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    85
         "[| evs: tls;  X: synth (analz (spies evs)) |]
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    86
          ==> Says Spy B X # evs : tls"
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    87
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
    88
    SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    89
         "[| evsSK: tls;
5359
bd539b72d484 Tidying
paulson
parents: 5074
diff changeset
    90
	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
4421
88639289be39 Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
paulson
parents: 4198
diff changeset
    91
          ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
6284
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
    92
			   Key (sessionK((NA,NB,M),role)) |} # evsSK : tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    93
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    94
    ClientHello
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    95
	 (*(7.4.1.2)
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
    96
	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    97
	   It is uninterpreted but will be confirmed in the FINISHED messages.
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
    98
	   NA is CLIENT RANDOM, while SID is SESSION_ID.
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
    99
           UNIX TIME is omitted because the protocol doesn't use it.
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   100
           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
4198
c63639beeff1 Fixed spelling error
paulson
parents: 3759
diff changeset
   101
	   while MASTER SECRET is 48 bytes*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   102
         "[| evsCH: tls;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   103
          ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   104
	        # evsCH  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   105
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   106
    ServerHello
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   107
         (*7.4.1.3 of the TLS Internet-Draft
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   108
	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   109
           SERVER CERTIFICATE (7.4.2) is always present.
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   110
           CERTIFICATE_REQUEST (7.4.4) is implied.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   111
         "[| evsSH: tls;  Nonce NB ~: used evsSH;  NB ~: range PRF;
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   112
             Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   113
	       : set evsSH |]
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   114
          ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   115
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   116
    Certificate
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   117
         (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
6284
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
   118
         "evsC: tls ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   119
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   120
    ClientKeyExch
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   121
         (*CLIENT KEY EXCHANGE (7.4.7).
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   122
           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
   123
           She encrypts PMS using the supplied KB, which ought to be pubK B.
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   124
           We assume PMS ~: range PRF because a clash betweem the PMS
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   125
           and another MASTER SECRET is highly unlikely (even though
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   126
	   both items have the same length, 48 bytes).
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   127
           The Note event records in the trace that she knows PMS
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   128
               (see REMARK at top). *)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   129
         "[| evsCX: tls;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
4421
88639289be39 Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
paulson
parents: 4198
diff changeset
   130
             Says B' A (certificate B KB) : set evsCX |]
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   131
          ==> Says A B (Crypt KB (Nonce PMS))
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   132
	      # Notes A {|Agent B, Nonce PMS|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   133
	      # evsCX  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   134
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   135
    CertVerify
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   136
	(*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
   137
          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
   138
          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
   139
          Checking the signature, which is the only use of A's certificate,
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   140
          assures B of A's presence*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   141
         "[| evsCV: tls;  
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   142
             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   143
	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   144
          ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   145
              # evsCV  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   146
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   147
	(*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
   148
          among other things.  The master-secret is PRF(PMS,NA,NB).
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   149
          Either party may sent its message first.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   150
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   151
    ClientFinished
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   152
        (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   153
          rule's applying when the Spy has satisfied the "Says A B" by
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   154
          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
   155
          Spy does not know PMS and could not send ClientFinished.  One
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   156
          could simply put A~=Spy into the rule, but one should not
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   157
          expect the spy to be well-behaved.*)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   158
         "[| evsCF: tls;  
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   159
	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   160
	       : set evsCF;
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   161
             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCF;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   162
             Notes A {|Agent B, Nonce PMS|} : set evsCF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   163
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   164
          ==> Says A B (Crypt (clientK(NA,NB,M))
3757
7524781c5c83 Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents: 3745
diff changeset
   165
			(Hash{|Number SID, Nonce M,
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   166
			       Nonce NA, Number PA, Agent A, 
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   167
			       Nonce NB, Number PB, Agent B|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   168
              # evsCF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   169
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   170
    ServerFinished
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   171
	(*Keeping A' and A'' distinct means B cannot even check that the
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   172
          two messages originate from the same source. *)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   173
         "[| evsSF: tls;
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   174
	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   175
	       : set evsSF;
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   176
	     Says B  A  {|Nonce NB, Number SID, Number PB|} : set evsSF;
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   177
	     Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   178
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   179
          ==> Says B A (Crypt (serverK(NA,NB,M))
3757
7524781c5c83 Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents: 3745
diff changeset
   180
			(Hash{|Number SID, Nonce M,
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   181
			       Nonce NA, Number PA, Agent A, 
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   182
			       Nonce NB, Number PB, Agent B|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   183
              # evsSF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   184
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   185
    ClientAccepts
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   186
	(*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
   187
          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
   188
          needed to resume this session.  The "Notes A ..." premise is
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   189
          used to prove Notes_master_imp_Crypt_PMS.*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   190
         "[| evsCA: tls;
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   191
	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   192
	     M = PRF(PMS,NA,NB);  
3757
7524781c5c83 Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents: 3745
diff changeset
   193
	     X = Hash{|Number SID, Nonce M,
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   194
	               Nonce NA, Number PA, Agent A, 
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   195
		       Nonce NB, Number PB, Agent B|};
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   196
             Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   197
             Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   198
          ==> 
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   199
             Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   200
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   201
    ServerAccepts
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   202
	(*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
   203
          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
   204
          needed to resume this session.  The "Says A'' B ..." premise is
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   205
          used to prove Notes_master_imp_Crypt_PMS.*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   206
         "[| evsSA: tls;
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   207
	     A ~= B;
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   208
             Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   209
	     M = PRF(PMS,NA,NB);  
3757
7524781c5c83 Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents: 3745
diff changeset
   210
	     X = Hash{|Number SID, Nonce M,
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   211
	               Nonce NA, Number PA, Agent A, 
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   212
		       Nonce NB, Number PB, Agent B|};
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   213
             Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   214
             Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   215
          ==> 
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   216
             Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   217
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   218
    ClientResume
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   219
         (*If A recalls the SESSION_ID, then she sends a FINISHED message
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   220
           using the new nonces and stored MASTER SECRET.*)
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   221
         "[| evsCR: tls;  
3759
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   222
	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   223
             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   224
             Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   225
          ==> Says A B (Crypt (clientK(NA,NB,M))
3757
7524781c5c83 Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents: 3745
diff changeset
   226
			(Hash{|Number SID, Nonce M,
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   227
			       Nonce NA, Number PA, Agent A, 
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3710
diff changeset
   228
			       Nonce NB, Number PB, Agent B|}))
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   229
              # evsCR  :  tls"
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   230
3759
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   231
    ServerResume
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   232
         (*Resumption (7.3):  If B finds the SESSION_ID then he can send
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   233
           a FINISHED message using the recovered MASTER SECRET*)
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   234
         "[| evsSR: tls;
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   235
	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   236
	     Says B  A {|Nonce NB, Number SID, Number PB|} : set evsSR;  
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   237
             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR |]
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   238
          ==> Says B A (Crypt (serverK(NA,NB,M))
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   239
			(Hash{|Number SID, Nonce M,
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   240
			       Nonce NA, Number PA, Agent A, 
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   241
			       Nonce NB, Number PB, Agent B|})) # evsSR
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   242
	        :  tls"
3d1ac6b82b28 Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents: 3757
diff changeset
   243
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   244
    Oops 
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   245
         (*The most plausible compromise is of an old session key.  Losing
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   246
           the MASTER SECRET or PREMASTER SECRET is more serious but
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   247
           rather unlikely.  The assumption A ~= Spy is essential: otherwise
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   248
           the Spy could learn session keys merely by replaying messages!*)
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
   249
         "[| evso: tls;  A ~= Spy;
6284
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
   250
	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) : set evso |]
147db42c1009 tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents: 5653
diff changeset
   251
          ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   252
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   253
end