author  paulson 
Mon, 07 Jul 1997 10:49:14 +0200  
changeset 3506  a36e0a49d2cd 
parent 3500  0d8ad2f192d8 
child 3515  d8a71f6eaf40 
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 
3474  21 
*) 
22 

23 
TLS = Public + 

24 

25 
consts 

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

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

3500  28 
certificate :: "[agent,key] => msg" 
29 

30 
defs 

31 
certificate_def 

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

3474  33 

34 
rules 

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

36 
inj_clientK "inj clientK" 

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

38 

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

39 
(*serverK is similar*) 
3474  40 
inj_serverK "inj serverK" 
41 
isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*) 

42 

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

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

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

45 

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

48 
Server_not_lost "Server ~: lost" 

49 

50 

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

52 
tls :: event list set 

53 

54 
inductive tls 

55 
intrs 

56 
Nil (*Initial trace is empty*) 

57 
"[]: tls" 

58 

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

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

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

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

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

63 

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

64 
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

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

66 
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

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

68 
Key (serverK(NA,NB,M)) } # evs : tls" 
3474  69 

70 
ClientHello 

71 
(*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. 

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

73 
As an initial simplification, SESSION_ID is identified with NA 

74 
and reuse of sessions is not supported.*) 

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

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

77 

78 
ServerHello 

79 
(*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. 

80 
Na is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is 

81 
implied and a SERVER CERTIFICATE is always present.*) 

82 
"[ evs: tls; A ~= B; Nonce NB ~: used evs; 

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

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

3500  85 
certificate B (pubK B)} 
3474  86 
# evs : tls" 
87 

88 
ClientCertKeyEx 

89 
(*CLIENT CERTIFICATE and KEY EXCHANGE. M is the premastersecret. 

90 
Note that A encrypts using the supplied KB, not pubK B.*) 

91 
"[ evs: tls; A ~= B; Nonce M ~: used evs; 

3506  92 
Says B' A {Nonce NA, Nonce NB, Agent XB, certificate B KB} 
93 
: set evs ] 

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

3474  95 
# evs : tls" 
96 

97 
CertVerify 

98 
(*The optional CERTIFICATE VERIFY message contains the specific 

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

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

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

105 
Says A B {certificate A (pubK A), Crypt KB (Nonce M)} 

106 
: set evs ] 

3474  107 
==> Says A B (Crypt (priK A) 
3506  108 
(Hash{Nonce NB, certificate B KB, Nonce M})) 
3474  109 
# evs : tls" 
110 

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

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

113 
Either party may sent its message first.*) 

114 

115 
ClientFinished 

116 
"[ evs: tls; A ~= B; 

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

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

120 
Says A B {certificate A (pubK A), Crypt KB (Nonce M)} 

121 
: set evs ] 

3474  122 
==> Says A B (Crypt (clientK(NA,NB,M)) 
123 
(Hash{Hash{Nonce NA, Nonce NB, Nonce M}, 

124 
Nonce NA, Agent XA, 

3500  125 
certificate A (pubK A), 
3474  126 
Nonce NB, Agent XB, Agent B})) 
127 
# evs : tls" 

128 

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

130 
two messages originate from the same source.*) 

131 

132 
ServerFinished 

133 
"[ evs: tls; A ~= B; 

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

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

3500  136 
certificate B (pubK B)} 
3474  137 
: set evs; 
138 
Says A'' B {CERTA, Crypt (pubK B) (Nonce M)} : set evs ] 

139 
==> Says B A (Crypt (serverK(NA,NB,M)) 

140 
(Hash{Hash{Nonce NA, Nonce NB, Nonce M}, 

141 
Nonce NA, Agent XA, Agent A, 

142 
Nonce NB, Agent XB, 

3500  143 
certificate B (pubK B)})) 
3474  144 
# evs : tls" 
145 

146 
(**Oops message??**) 

147 

148 
end 