|
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 |
|
15 The model assumes that no fraudulent certificates are present. |
|
16 |
|
17 Protocol goals: |
|
18 * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two |
|
19 parties (though A is not necessarily authenticated). |
|
20 |
|
21 * B upon receiving CERTIFICATE VERIFY knows that A is present (But this |
|
22 message is optional!) |
|
23 |
|
24 * A upon receiving SERVER FINISHED knows that B is present |
|
25 |
|
26 * Each party who has received a FINISHED message can trust that the other |
|
27 party agrees on all message components, including XA and XB (thus foiling |
|
28 rollback attacks). |
|
29 *) |
|
30 |
|
31 TLS = Public + |
|
32 |
|
33 consts |
|
34 (*Client, server write keys. They implicitly include the MAC secrets.*) |
|
35 clientK, serverK :: "nat*nat*nat => key" |
|
36 |
|
37 rules |
|
38 (*clientK is collision-free and makes symmetric keys*) |
|
39 inj_clientK "inj clientK" |
|
40 isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*) |
|
41 |
|
42 inj_serverK "inj serverK" |
|
43 isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*) |
|
44 |
|
45 (*Spy has access to his own key for spoof messages, but Server is secure*) |
|
46 Spy_in_lost "Spy: lost" |
|
47 Server_not_lost "Server ~: lost" |
|
48 |
|
49 |
|
50 consts lost :: agent set (*No need for it to be a variable*) |
|
51 tls :: event list set |
|
52 |
|
53 inductive tls |
|
54 intrs |
|
55 Nil (*Initial trace is empty*) |
|
56 "[]: tls" |
|
57 |
|
58 Fake (*The spy, an active attacker, MAY say anything he CAN say.*) |
|
59 "[| evs: tls; B ~= Spy; |
|
60 X: synth (analz (sees lost Spy evs)) |] |
|
61 ==> Says Spy B X # evs : tls" |
|
62 |
|
63 ClientHello |
|
64 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. |
|
65 It is uninterpreted but will be confirmed in the FINISHED messages. |
|
66 As an initial simplification, SESSION_ID is identified with NA |
|
67 and reuse of sessions is not supported.*) |
|
68 "[| evs: tls; A ~= B; Nonce NA ~: used evs |] |
|
69 ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs : tls" |
|
70 |
|
71 ServerHello |
|
72 (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. |
|
73 Na is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is |
|
74 implied and a SERVER CERTIFICATE is always present.*) |
|
75 "[| evs: tls; A ~= B; Nonce NB ~: used evs; |
|
76 Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |] |
|
77 ==> Says B A {|Nonce NA, Nonce NB, Agent XB, |
|
78 Crypt (priK Server) {|Agent B, Key (pubK B)|}|} |
|
79 # evs : tls" |
|
80 |
|
81 ClientCertKeyEx |
|
82 (*CLIENT CERTIFICATE and KEY EXCHANGE. M is the pre-master-secret. |
|
83 Note that A encrypts using the supplied KB, not pubK B.*) |
|
84 "[| evs: tls; A ~= B; Nonce M ~: used evs; |
|
85 Says B' A {|Nonce NA, Nonce NB, Agent XB, |
|
86 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |] |
|
87 ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, |
|
88 Crypt KB (Nonce M)|} |
|
89 # evs : tls" |
|
90 |
|
91 CertVerify |
|
92 (*The optional CERTIFICATE VERIFY message contains the specific |
|
93 components listed in the security analysis, Appendix F.1.1.2. |
|
94 By checking the signature, B is assured of A's existence: |
|
95 the only use of A's certificate.*) |
|
96 "[| evs: tls; A ~= B; |
|
97 Says B' A {|Nonce NA, Nonce NB, Agent XB, |
|
98 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |] |
|
99 ==> Says A B (Crypt (priK A) |
|
100 (Hash{|Nonce NB, |
|
101 Crypt (priK Server) {|Agent B, Key KB|}|})) |
|
102 # evs : tls" |
|
103 |
|
104 (*Finally come the FINISHED messages, confirming XA and XB among |
|
105 other things. The master-secret is the hash of NA, NB and M. |
|
106 Either party may sent its message first.*) |
|
107 |
|
108 ClientFinished |
|
109 "[| evs: tls; A ~= B; |
|
110 Says A B {|Agent A, Nonce NA, Agent XA|} : set evs; |
|
111 Says B' A {|Nonce NA, Nonce NB, Agent XB, |
|
112 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs; |
|
113 Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, |
|
114 Crypt KB (Nonce M)|} : set evs |] |
|
115 ==> Says A B (Crypt (clientK(NA,NB,M)) |
|
116 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, |
|
117 Nonce NA, Agent XA, |
|
118 Crypt (priK Server) {|Agent A, Key(pubK A)|}, |
|
119 Nonce NB, Agent XB, Agent B|})) |
|
120 # evs : tls" |
|
121 |
|
122 (*Keeping A' and A'' distinct means B cannot even check that the |
|
123 two messages originate from the same source.*) |
|
124 |
|
125 ServerFinished |
|
126 "[| evs: tls; A ~= B; |
|
127 Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs; |
|
128 Says B A {|Nonce NA, Nonce NB, Agent XB, |
|
129 Crypt (priK Server) {|Agent B, Key (pubK B)|}|} |
|
130 : set evs; |
|
131 Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |] |
|
132 ==> Says B A (Crypt (serverK(NA,NB,M)) |
|
133 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, |
|
134 Nonce NA, Agent XA, Agent A, |
|
135 Nonce NB, Agent XB, |
|
136 Crypt (priK Server) {|Agent B, Key(pubK B)|}|})) |
|
137 # evs : tls" |
|
138 |
|
139 (**Oops message??**) |
|
140 |
|
141 end |