src/HOL/Auth/TLS.thy
author paulson
Tue, 16 Sep 1997 14:40:01 +0200
changeset 3676 cbaec955056b
parent 3672 56e4365a0c99
child 3677 f2569416d18b
permissions -rw-r--r--
Addition of SessionIDs to the Hello and Finished messages
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
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    34
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
    35
decrypt, so the problem does not arise.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    36
*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    37
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    38
TLS = Public + 
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
consts
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    41
  (*Pseudo-random function of Section 5*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    42
  PRF  :: "nat*nat*nat => nat"
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    43
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    44
  (*Client, server write keys implicitly include the MAC secrets.*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    45
  clientK, serverK :: "nat*nat*nat => key"
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    46
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    47
  certificate      :: "[agent,key] => msg"
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    48
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    49
defs
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    50
  certificate_def
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    51
    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    52
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    53
rules
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    54
  inj_PRF       "inj PRF"	
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    55
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    56
  (*clientK is collision-free and makes symmetric keys*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    57
  inj_clientK   "inj clientK"	
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    58
  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    59
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    60
  (*serverK is similar*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    61
  inj_serverK   "inj serverK"	
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    62
  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    63
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    64
  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    65
  clientK_range "range clientK <= Compl (range serverK)"
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    66
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    67
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    68
consts    tls :: event list set
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    69
inductive tls
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    70
  intrs 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    71
    Nil  (*Initial trace is empty*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    72
         "[]: tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    73
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    74
    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
    75
         "[| evs: tls;  B ~= Spy;  
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    76
             X: synth (analz (sees Spy evs)) |]
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    77
          ==> Says Spy B X # evs : tls"
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    78
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    79
    SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    80
         "[| evsSK: tls;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    81
	     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
    82
          ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    83
			    Key (clientK(NA,NB,M)),
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    84
			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
3474
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
    ClientHello
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    87
	 (*(7.4.1.2)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    88
	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    89
	   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
    90
	   NA is CLIENT RANDOM, while SID is SESSION_ID.
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
    91
           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
    92
           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
    93
	   while MASTER SECRET is 48 byptes*)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    94
         "[| 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
    95
          ==> 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
    96
	        # evsCH  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    97
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    98
    ServerHello
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    99
         (*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
   100
	   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
   101
           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
   102
           CERTIFICATE_REQUEST (7.4.4) is implied.*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   103
         "[| 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
   104
             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
   105
	       : set evsSH |]
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   106
          ==> Says B A {|Nonce NB, Number SID, Number XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   107
			 certificate B (pubK B)|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   108
                # evsSH  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   109
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   110
    ClientCertKeyEx
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   111
         (*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
   112
           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
   113
           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
   114
           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
   115
           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
   116
	   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
   117
           The Note event records in the trace that she knows PMS
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   118
               (see REMARK at top).*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   119
         "[| 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
   120
             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
   121
	       : set evsCX |]
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   122
          ==> 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
   123
	      # Notes A {|Agent B, Nonce PMS|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   124
	      # evsCX  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   125
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   126
    CertVerify
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   127
	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   128
          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
   129
          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
   130
          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
   131
          assures B of A's presence*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   132
         "[| evsCV: tls;  A ~= B;  
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   133
             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
   134
	       : set evsCV;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   135
	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   136
          ==> Says A B (Crypt (priK A)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   137
			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   138
              # evsCV  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   139
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   140
	(*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
   141
          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
   142
          Either party may sent its message first.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   143
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   144
        (*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
   145
          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
   146
          repaying messages sent by the true client; in that case, the
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   147
          Spy does not know PMS and could not sent CLIENT FINISHED.  One
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   148
          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
   149
          expect the spy to be well-behaved.*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   150
    ClientFinished
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   151
         "[| evsCF: tls;  
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   152
	     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
   153
	       : set evsCF;
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   154
             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
   155
	       : set evsCF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   156
             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
   157
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   158
          ==> Says A B (Crypt (clientK(NA,NB,M))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   159
			(Hash{|Nonce M, Number SID,
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   160
			       Nonce NA, Number XA, Agent A, 
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   161
			       Nonce NB, Number XB, Agent B|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   162
              # evsCF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   163
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   164
	(*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
   165
          two messages originate from the same source. *)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   166
    ServerFinished
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   167
         "[| evsSF: tls;
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   168
	     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
   169
	       : set evsSF;
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   170
	     Says B  A  {|Nonce NB, Number SID, Number XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   171
		 	  certificate B (pubK B)|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   172
	       : set evsSF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   173
	     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
   174
	       : set evsSF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   175
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   176
          ==> Says B A (Crypt (serverK(NA,NB,M))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   177
			(Hash{|Nonce M, Number SID,
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   178
			       Nonce NA, Number XA, Agent A, 
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   179
			       Nonce NB, Number XB, Agent B|}))
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   180
              # evsSF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   181
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   182
  (**Oops message??**)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   183
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   184
end