src/HOL/Auth/TLS.thy
author paulson
Mon, 22 Sep 1997 13:17:29 +0200
changeset 3687 fb7d096d7884
parent 3686 4b484805b4c4
child 3704 2f99d7a0dccc
permissions -rw-r--r--
Simplified SpyKeys to use sessionK instead of clientK and serverK Proved and used analz_insert_key, shortening scripts
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
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     6
Inductive relation "tls" for the baby 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
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    24
REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
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
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    26
herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
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
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    36
Proofs would be simpler if ClientCertKeyEx included A's name within
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
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    44
consts
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    45
  (*Pseudo-random function of Section 5*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    46
  PRF  :: "nat*nat*nat => nat"
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    47
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    48
  (*Client, server write keys generated uniformly by function sessionK
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    49
    to avoid duplicating their properties.
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    50
    Theyimplicitly include the MAC secrets.*)
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
    51
  sessionK :: "(nat*nat*nat)*bool => key"
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    52
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    53
  certificate      :: "[agent,key] => msg"
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    54
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    55
defs
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    56
  certificate_def
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    57
    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    58
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    59
syntax
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    60
    clientK, serverK :: "nat*nat*nat => key"
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    61
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    62
translations
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
    63
  "clientK (x)"	== "sessionK(x,True)"
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
    64
  "serverK (x)"	== "sessionK(x,False)"
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    65
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    66
rules
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    67
  inj_PRF       "inj PRF"	
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    68
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
    69
  (*sessionK is collision-free and makes symmetric keys.  Also, no clientK
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
    70
    clashes with any serverK.*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    71
  inj_sessionK  "inj sessionK"	
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    72
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    73
  isSym_sessionK "isSymKey (sessionK x)"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    74
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    75
  (*serverK is similar*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    76
  inj_serverK   "inj serverK"	
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    77
  isSym_serverK "isSymKey (serverK x)"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    78
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    79
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    80
consts    tls :: event list set
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    81
inductive tls
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    82
  intrs 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    83
    Nil  (*Initial trace is empty*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    84
         "[]: tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    85
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    86
    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    87
         "[| evs: tls;  B ~= Spy;  
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
    88
             X: synth (analz (spies evs)) |]
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    89
          ==> Says Spy B X # evs : tls"
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    90
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
    91
    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
    92
         "[| evsSK: tls;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    93
	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    94
          ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
    95
			    Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    96
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    97
    ClientHello
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    98
	 (*(7.4.1.2)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    99
	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   100
	   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
   101
	   NA is CLIENT RANDOM, while SID is SESSION_ID.
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   102
           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
   103
           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   104
	   while MASTER SECRET is 48 byptes*)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   105
         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   106
          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   107
	        # evsCH  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   108
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   109
    ServerHello
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   110
         (*7.4.1.3 of the TLS Internet-Draft
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   111
	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   112
           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
   113
           CERTIFICATE_REQUEST (7.4.4) is implied.*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   114
         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   115
             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   116
	       : set evsSH |]
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   117
          ==> Says B A {|Nonce NB, Number SID, Number XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   118
			 certificate B (pubK B)|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   119
                # evsSH  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   120
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   121
    ClientCertKeyEx
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   122
         (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   123
           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
   124
           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
   125
           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
   126
           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
   127
	   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
   128
           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
   129
               (see REMARK at top). *)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   130
         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   131
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   132
	       : set evsCX |]
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   133
          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   134
	      # Notes A {|Agent B, Nonce PMS|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   135
	      # evsCX  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   136
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   137
    CertVerify
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   138
	(*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
   139
          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
   140
          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
   141
          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
   142
          assures B of A's presence*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   143
         "[| evsCV: tls;  A ~= B;  
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   144
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   145
	       : set evsCV;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   146
	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   147
          ==> Says A B (Crypt (priK A)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   148
			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   149
              # evsCV  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   150
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   151
	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   152
          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
   153
          Either party may sent its message first.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   154
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   155
    ClientFinished
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   156
        (*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
   157
          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
   158
          repaying messages sent by the true client; in that case, the
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   159
          Spy does not know PMS and could not sent ClientFinished.  One
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   160
          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
   161
          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
   162
         "[| evsCF: tls;  
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   163
	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   164
	       : set evsCF;
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   165
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   166
	       : set evsCF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   167
             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
   168
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   169
          ==> Says A B (Crypt (clientK(NA,NB,M))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   170
			(Hash{|Nonce M, Number SID,
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   171
			       Nonce NA, Number XA, Agent A, 
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   172
			       Nonce NB, Number XB, Agent B|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   173
              # evsCF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   174
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   175
    ServerFinished
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   176
	(*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
   177
          two messages originate from the same source. *)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   178
         "[| evsSF: tls;
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   179
	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   180
	       : set evsSF;
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   181
	     Says B  A  {|Nonce NB, Number SID, Number XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   182
		 	  certificate B (pubK B)|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   183
	       : set evsSF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   184
	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   185
	       : set evsSF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   186
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   187
          ==> Says B A (Crypt (serverK(NA,NB,M))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   188
			(Hash{|Nonce M, Number SID,
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   189
			       Nonce NA, Number XA, Agent A, 
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   190
			       Nonce NB, Number XB, Agent B|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   191
              # evsSF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   192
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   193
    ClientAccepts
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   194
	(*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
   195
          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
   196
          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
   197
          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
   198
         "[| evsCA: tls;
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   199
	     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
   200
	     M = PRF(PMS,NA,NB);  
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   201
	     X = Hash{|Nonce M, Number SID,
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   202
	               Nonce NA, Number XA, Agent A, 
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   203
		       Nonce NB, Number XB, Agent B|};
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   204
             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
   205
             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
   206
          ==> 
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   207
             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
   208
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   209
    ServerAccepts
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   210
	(*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
   211
          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
   212
          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
   213
          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
   214
         "[| evsSA: tls;
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   215
             Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   216
	       : set evsSA;
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   217
	     M = PRF(PMS,NA,NB);  
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   218
	     X = Hash{|Nonce M, Number SID,
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   219
	               Nonce NA, Number XA, Agent A, 
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   220
		       Nonce NB, Number XB, Agent B|};
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   221
             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
   222
             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
   223
          ==> 
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   224
             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
   225
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   226
    ServerResume
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   227
         (*Resumption is described in 7.3.  If B finds the SESSION_ID
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   228
           then he sends HELLO and FINISHED messages, using the
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   229
           previously stored MASTER SECRET*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   230
         "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   231
             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   232
	     Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   233
	       : set evsSR |]
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   234
          ==> Says B A (Crypt (serverK(NA,NB,M))
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   235
			(Hash{|Nonce M, Number SID,
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   236
			       Nonce NA, Number XA, Agent A, 
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   237
			       Nonce NB, Number XB, Agent B|}))
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   238
              # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR  :  tls"
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   239
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   240
    ClientResume
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   241
         (*If the response to ClientHello is ServerResume then send
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   242
           a FINISHED message using the new nonces and stored MASTER SECRET.*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   243
         "[| evsCR: tls;  
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   244
	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   245
	       : set evsCR;
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   246
             Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   247
             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
   248
          ==> Says A B (Crypt (clientK(NA,NB,M))
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   249
			(Hash{|Nonce M, Number SID,
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   250
			       Nonce NA, Number XA, Agent A, 
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   251
			       Nonce NB, Number XB, Agent B|}))
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   252
              # evsCR  :  tls"
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   253
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   254
    Oops 
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   255
         (*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
   256
           the MASTER SECRET or PREMASTER SECRET is more serious but
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   257
           rather unlikely.*)
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   258
         "[| evso: tls;  A ~= Spy;  
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   259
	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   260
          ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   261
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   262
end