author  paulson 
Fri, 11 Jul 1997 13:30:01 +0200  
changeset 3515  d8a71f6eaf40 
parent 3506  a36e0a49d2cd 
child 3519  ab0a9fbed4c0 
permissions  rwrr 
3474  1 
(* Title: HOL/Auth/TLS 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

6 
Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol. 

7 

8 
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down 

9 
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a 

10 
global signing authority. 

11 

12 
A is the client and B is the server, not to be confused with the constant 

13 
Server, who is in charge of all public keys. 

14 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

15 
The model assumes that no fraudulent certificates are present, but it does 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

16 
assume that some private keys are lost to the spy. 
3474  17 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

18 
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

19 
Allen, Transport Layer Security Working Group, 21 May 1997, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

20 
INTERNETDRAFT draftietftlsprotocol03.txt 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

21 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

22 
NOTE. The event "Notes A {Agent B, Nonce M}" appears in ClientCertKeyEx, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

23 
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

24 
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

25 
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

26 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

27 
The note is needed because of a weakness in the publickey model. Each 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

28 
agent's state is recorded as the trace of messages. When the true client (A) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

29 
invents M, he encrypts M with B's public key before sending it. The model 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

30 
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

31 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

32 
In the sharedkey model, the ability to encrypt implies the ability to 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

33 
decrypt, so the problem does not arise. 
3474  34 
*) 
35 

36 
TLS = Public + 

37 

38 
consts 

39 
(*Client, server write keys. They implicitly include the MAC secrets.*) 

40 
clientK, serverK :: "nat*nat*nat => key" 

3500  41 
certificate :: "[agent,key] => msg" 
42 

43 
defs 

44 
certificate_def 

45 
"certificate A KA == Crypt (priK Server) {Agent A, Key KA}" 

3474  46 

47 
rules 

48 
(*clientK is collisionfree and makes symmetric keys*) 

49 
inj_clientK "inj clientK" 

50 
isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*) 

51 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

52 
(*serverK is similar*) 
3474  53 
inj_serverK "inj serverK" 
54 
isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*) 

55 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

56 
(*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

57 
clientK_range "range clientK <= Compl (range serverK)" 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

58 

3474  59 
(*Spy has access to his own key for spoof messages, but Server is secure*) 
60 
Spy_in_lost "Spy: lost" 

61 
Server_not_lost "Server ~: lost" 

62 

63 

64 
consts lost :: agent set (*No need for it to be a variable*) 

65 
tls :: event list set 

66 

67 
inductive tls 

68 
intrs 

69 
Nil (*Initial trace is empty*) 

70 
"[]: tls" 

71 

72 
Fake (*The spy, an active attacker, MAY say anything he CAN say.*) 

73 
"[ evs: tls; B ~= Spy; 

74 
X: synth (analz (sees lost Spy evs)) ] 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

75 
==> Says Spy B X # evs : tls" 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

76 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

77 
SpyKeys (*The spy may apply clientK & serverK to nonces he's found*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

78 
"[ evs: tls; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

79 
Says Spy B {Nonce NA, Nonce NB, Nonce M} : set evs ] 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

80 
==> Says Spy B { Key (clientK(NA,NB,M)), 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

81 
Key (serverK(NA,NB,M)) } # evs : tls" 
3474  82 

83 
ClientHello 

84 
(*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. 

85 
It is uninterpreted but will be confirmed in the FINISHED messages. 

86 
As an initial simplification, SESSION_ID is identified with NA 

87 
and reuse of sessions is not supported.*) 

88 
"[ evs: tls; A ~= B; Nonce NA ~: used evs ] 

89 
==> Says A B {Agent A, Nonce NA, Agent XA} # evs : tls" 

90 

91 
ServerHello 

92 
(*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

93 
NA is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is 
3474  94 
implied and a SERVER CERTIFICATE is always present.*) 
95 
"[ evs: tls; A ~= B; Nonce NB ~: used evs; 

96 
Says A' B {Agent A, Nonce NA, Agent XA} : set evs ] 

97 
==> Says B A {Nonce NA, Nonce NB, Agent XB, 

3500  98 
certificate B (pubK B)} 
3474  99 
# evs : tls" 
100 

101 
ClientCertKeyEx 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

102 
(*CLIENT CERTIFICATE and KEY EXCHANGE. The client, A, chooses M, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

103 
the premastersecret. She encrypts M using the supplied KB, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

104 
which ought to be pubK B, and also with her own public key, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

105 
to record in the trace that she knows M (see NOTE at top).*) 
3474  106 
"[ evs: tls; A ~= B; Nonce M ~: used evs; 
3506  107 
Says B' A {Nonce NA, Nonce NB, Agent XB, certificate B KB} 
108 
: set evs ] 

109 
==> Says A B {certificate A (pubK A), Crypt KB (Nonce M)} 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

110 
# Notes A {Agent B, Nonce M} 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

111 
# evs : tls" 
3474  112 

113 
CertVerify 

114 
(*The optional CERTIFICATE VERIFY message contains the specific 

3506  115 
components listed in the security analysis, Appendix F.1.1.2; 
116 
it also contains the premastersecret. Checking the signature, 

117 
which is the only use of A's certificate, assures B of A's presence*) 

3474  118 
"[ evs: tls; A ~= B; 
3506  119 
Says B' A {Nonce NA, Nonce NB, Agent XB, certificate B KB} 
120 
: set evs; 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

121 
Notes A {Agent B, Nonce M} : set evs ] 
3474  122 
==> Says A B (Crypt (priK A) 
3506  123 
(Hash{Nonce NB, certificate B KB, Nonce M})) 
3474  124 
# evs : tls" 
125 

126 
(*Finally come the FINISHED messages, confirming XA and XB among 

127 
other things. The mastersecret is the hash of NA, NB and M. 

128 
Either party may sent its message first.*) 

129 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

130 
(*The occurrence of Crypt (pubK A) {Agent B, Nonce M} stops the 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

131 
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

132 
repaying messages sent by the true client; in that case, the 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

133 
Spy does not know M and could not sent CLIENT FINISHED. One 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

134 
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

135 
expect the spy to be wellbehaved.*) 
3474  136 
ClientFinished 
137 
"[ evs: tls; A ~= B; 

138 
Says A B {Agent A, Nonce NA, Agent XA} : set evs; 

3506  139 
Says B' A {Nonce NA, Nonce NB, Agent XB, certificate B KB} 
140 
: set evs; 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

141 
Notes A {Agent B, Nonce M} : set evs ] 
3474  142 
==> Says A B (Crypt (clientK(NA,NB,M)) 
143 
(Hash{Hash{Nonce NA, Nonce NB, Nonce M}, 

144 
Nonce NA, Agent XA, 

3500  145 
certificate A (pubK A), 
3474  146 
Nonce NB, Agent XB, Agent B})) 
147 
# evs : tls" 

148 

149 
(*Keeping A' and A'' distinct means B cannot even check that the 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

150 
two messages originate from the same source. B does not attempt 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

151 
to read A's encrypted "note to herself".*) 
3474  152 
ServerFinished 
153 
"[ evs: tls; A ~= B; 

154 
Says A' B {Agent A, Nonce NA, Agent XA} : set evs; 

155 
Says B A {Nonce NA, Nonce NB, Agent XB, 

3500  156 
certificate B (pubK B)} 
3474  157 
: set evs; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

158 
Says A'' B {certificate A KA, Crypt (pubK B) (Nonce M)} 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

159 
: set evs ] 
3474  160 
==> Says B A (Crypt (serverK(NA,NB,M)) 
161 
(Hash{Hash{Nonce NA, Nonce NB, Nonce M}, 

162 
Nonce NA, Agent XA, Agent A, 

163 
Nonce NB, Agent XB, 

3500  164 
certificate B (pubK B)})) 
3474  165 
# evs : tls" 
166 

167 
(**Oops message??**) 

168 

169 
end 