--- a/src/HOL/Auth/TLS.thy Fri Sep 12 10:45:51 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Tue Sep 16 13:32:22 1997 +0200
@@ -4,6 +4,12 @@
Copyright 1997 University of Cambridge
Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
+This protocol is essentially the same as SSL 3.0.
+
+Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
+Allen, Transport Layer Security Working Group, 21 May 1997,
+INTERNET-DRAFT draft-ietf-tls-protocol-03.txt. Section numbers below refer
+to that memo.
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
@@ -15,18 +21,14 @@
The model assumes that no fraudulent certificates are present, but it does
assume that some private keys are to the spy.
-Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
-Allen, Transport Layer Security Working Group, 21 May 1997,
-INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
-
-NOTE. The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx,
+REMARK. The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
CertVerify, ClientFinished to record that A knows M. It is a note from A to
herself. Nobody else can see it. In ClientCertKeyEx, the Spy can substitute
his own certificate for A's, but he cannot replace A's note by one for himself.
-The note is needed because of a weakness in the public-key model. Each
+The Note event avoids a weakness in the public-key model. Each
agent's state is recorded as the trace of messages. When the true client (A)
-invents M, he encrypts M with B's public key before sending it. The model
+invents PMS, he encrypts PMS with B's public key before sending it. The model
does not distinguish the original occurrence of such a message from a replay.
In the shared-key model, the ability to encrypt implies the ability to
@@ -36,8 +38,12 @@
TLS = Public +
consts
- (*Client, server write keys. They implicitly include the MAC secrets.*)
+ (*Pseudo-random function of Section 5*)
+ PRF :: "nat*nat*nat => nat"
+
+ (*Client, server write keys implicitly include the MAC secrets.*)
clientK, serverK :: "nat*nat*nat => key"
+
certificate :: "[agent,key] => msg"
defs
@@ -45,6 +51,8 @@
"certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
rules
+ inj_PRF "inj PRF"
+
(*clientK is collision-free and makes symmetric keys*)
inj_clientK "inj clientK"
isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*)
@@ -68,95 +76,105 @@
X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : tls"
- SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
- "[| evs: tls;
- Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
- ==> Says Spy B {| Key (clientK(NA,NB,M)),
- Key (serverK(NA,NB,M)) |} # evs : tls"
+ SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
+ "[| evsSK: tls;
+ Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
+ ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
+ Key (clientK(NA,NB,M)),
+ Key (serverK(NA,NB,M)) |} # evsSK : tls"
ClientHello
- (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
+ (*(7.4.1.2)
+ XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
It is uninterpreted but will be confirmed in the FINISHED messages.
As an initial simplification, SESSION_ID is identified with NA
- and reuse of sessions is not supported.*)
- "[| evs: tls; A ~= B; Nonce NA ~: used evs |]
- ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs : tls"
+ and reuse of sessions is not supported.
+ May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
+ while MASTER SECRET is 48 byptes (6.1)*)
+ "[| evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF |]
+ ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH : tls"
ServerHello
- (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
- NA is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is
- implied and a SERVER CERTIFICATE is always present.*)
- "[| evs: tls; A ~= B; Nonce NB ~: used evs;
- Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
- ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
+ (*7.4.1.3 of the TLS Internet-Draft
+ XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
+ NA is returned in its role as SESSION_ID.
+ SERVER CERTIFICATE (7.4.2) is always present.
+ CERTIFICATE_REQUEST (7.4.4) is implied.*)
+ "[| evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF;
+ Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
+ ==> Says B A {|Nonce NA, Nonce NB, Number XB,
certificate B (pubK B)|}
- # evs : tls"
+ # evsSH : tls"
ClientCertKeyEx
- (*CLIENT CERTIFICATE and KEY EXCHANGE. The client, A, chooses M,
- the pre-master-secret. She encrypts M using the supplied KB,
- which ought to be pubK B, and also with her own public key,
- to record in the trace that she knows M (see NOTE at top).*)
- "[| evs: tls; A ~= B; Nonce M ~: used evs;
- Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
- : set evs |]
- ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
- # Notes A {|Agent B, Nonce M|}
- # evs : tls"
+ (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
+ The client, A, chooses PMS, the PREMASTER SECRET.
+ She encrypts PMS using the supplied KB, which ought to be pubK B.
+ We assume PMS ~: range PRF because a clash betweem the PMS
+ and another MASTER SECRET is highly unlikely (even though
+ both items have the same length, 48 bytes).
+ The Note event records in the trace that she knows PMS
+ (see REMARK at top).*)
+ "[| evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF;
+ Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+ : set evsCX |]
+ ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
+ # Notes A {|Agent B, Nonce PMS|}
+ # evsCX : tls"
CertVerify
- (*The optional CERTIFICATE VERIFY message contains the specific
- components listed in the security analysis, Appendix F.1.1.2;
- it also contains the pre-master-secret. Checking the signature,
- which is the only use of A's certificate, assures B of A's presence*)
- "[| evs: tls; A ~= B;
- Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
- : set evs;
- Notes A {|Agent B, Nonce M|} : set evs |]
+ (*The optional CERTIFICATE VERIFY (7.4.8) message contains the
+ specific components listed in the security analysis, F.1.1.2.
+ It adds the pre-master-secret, which is also essential!
+ Checking the signature, which is the only use of A's certificate,
+ assures B of A's presence*)
+ "[| evsCV: tls; A ~= B;
+ Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+ : set evsCV;
+ Notes A {|Agent B, Nonce PMS|} : set evsCV |]
==> Says A B (Crypt (priK A)
- (Hash{|Nonce NB, certificate B KB, Nonce M|}))
- # evs : tls"
+ (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
+ # evsCV : tls"
- (*Finally come the FINISHED messages, confirming XA and XB among
- other things. The master-secret is the hash of NA, NB and M.
+ (*Finally come the FINISHED messages (7.4.8), confirming XA and XB
+ among other things. The master-secret is PRF(PMS,NA,NB).
Either party may sent its message first.*)
- (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the
+ (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
rule's applying when the Spy has satisfied the "Says A B" by
repaying messages sent by the true client; in that case, the
- Spy does not know M and could not sent CLIENT FINISHED. One
+ Spy does not know PMS and could not sent CLIENT FINISHED. One
could simply put A~=Spy into the rule, but one should not
expect the spy to be well-behaved.*)
ClientFinished
- "[| evs: tls; A ~= B;
- Says A B {|Agent A, Nonce NA, Agent XA|} : set evs;
- Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
- : set evs;
- Notes A {|Agent B, Nonce M|} : set evs |]
+ "[| evsCF: tls;
+ Says A B {|Agent A, Nonce NA, Number XA|} : set evsCF;
+ Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+ : set evsCF;
+ Notes A {|Agent B, Nonce PMS|} : set evsCF;
+ M = PRF(PMS,NA,NB) |]
==> Says A B (Crypt (clientK(NA,NB,M))
- (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
- Nonce NA, Agent XA,
- certificate A (pubK A),
- Nonce NB, Agent XB, Agent B|}))
- # evs : tls"
+ (Hash{|Nonce M,
+ Nonce NA, Number XA, Agent A,
+ Nonce NB, Number XB, Agent B|}))
+ # evsCF : tls"
(*Keeping A' and A'' distinct means B cannot even check that the
- two messages originate from the same source. B does not attempt
- to read A's encrypted "note to herself".*)
+ two messages originate from the same source. *)
ServerFinished
- "[| evs: tls; A ~= B;
- Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs;
- Says B A {|Nonce NA, Nonce NB, Agent XB,
+ "[| evsSF: tls;
+ Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSF;
+ Says B A {|Nonce NA, Nonce NB, Number XB,
certificate B (pubK B)|}
- : set evs;
- Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|}
- : set evs |]
+ : set evsSF;
+ Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
+ : set evsSF;
+ M = PRF(PMS,NA,NB) |]
==> Says B A (Crypt (serverK(NA,NB,M))
- (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
- Nonce NA, Agent XA, Agent A,
- Nonce NB, Agent XB,
- certificate B (pubK B)|}))
- # evs : tls"
+ (Hash{|Nonce M,
+ Nonce NA, Number XA, Agent A,
+ Nonce NB, Number XB, Agent B|}))
+ # evsSF : tls"
(**Oops message??**)