src/HOL/Auth/TLS.thy
author paulson
Tue, 16 Sep 1997 13:32:22 +0200
changeset 3672 56e4365a0c99
parent 3519 ab0a9fbed4c0
child 3676 cbaec955056b
permissions -rw-r--r--
TLS now with a distinction between premaster secret and master secret
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.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    90
	   As an initial simplification, SESSION_ID is identified with NA
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    91
           and reuse of sessions is not supported.
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    92
           May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    93
	   while MASTER SECRET is 48 byptes (6.1)*)
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 |]
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    95
          ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH  :  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
    ServerHello
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    98
         (*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
    99
	   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
   100
	   NA is returned in its role as SESSION_ID.
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;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   104
             Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   105
          ==> Says B A {|Nonce NA, Nonce NB, Number XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   106
			 certificate B (pubK B)|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   107
                # evsSH  :  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
    ClientCertKeyEx
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   110
         (*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
   111
           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
   112
           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
   113
           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
   114
           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
   115
	   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
   116
           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
   117
               (see REMARK at top).*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   118
         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   119
             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   120
	       : set evsCX |]
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   121
          ==> 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
   122
	      # Notes A {|Agent B, Nonce PMS|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   123
	      # evsCX  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   124
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   125
    CertVerify
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   126
	(*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
   127
          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
   128
          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
   129
          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
   130
          assures B of A's presence*)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   131
         "[| evsCV: tls;  A ~= B;  
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   132
             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   133
	       : set evsCV;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   134
	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   135
          ==> Says A B (Crypt (priK A)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   136
			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   137
                # evsCV  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   138
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   139
	(*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
   140
          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
   141
          Either party may sent its message first.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   142
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   143
        (*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
   144
          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
   145
          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
   146
          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
   147
          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
   148
          expect the spy to be well-behaved.*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   149
    ClientFinished
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   150
         "[| evsCF: tls;  
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   151
	     Says A  B {|Agent A, Nonce NA, Number XA|} : set evsCF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   152
             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   153
	       : set evsCF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   154
             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
   155
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   156
          ==> Says A B (Crypt (clientK(NA,NB,M))
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   157
			(Hash{|Nonce M,
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   158
			       Nonce NA, Number XA, Agent A, 
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   159
			       Nonce NB, Number XB, Agent B|}))
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   160
                # evsCF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   161
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   162
	(*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
   163
          two messages originate from the same source. *)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   164
    ServerFinished
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   165
         "[| evsSF: tls;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   166
	     Says A' B  {|Agent A, Nonce NA, Number XA|} : set evsSF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   167
	     Says B  A  {|Nonce NA, Nonce NB, Number XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   168
		 	  certificate B (pubK B)|}
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   169
	       : set evsSF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   170
	     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
   171
	       : set evsSF;
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   172
	     M = PRF(PMS,NA,NB) |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   173
          ==> Says B A (Crypt (serverK(NA,NB,M))
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   174
			(Hash{|Nonce M,
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   175
			       Nonce NA, Number XA, Agent A, 
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   176
			       Nonce NB, Number XB, Agent B|}))
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   177
                # evsSF  :  tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   178
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   179
  (**Oops message??**)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   180
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   181
end