--- a/src/HOL/Auth/TLS.ML Tue Sep 16 14:04:10 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Tue Sep 16 14:40:01 1997 +0200
@@ -110,9 +110,10 @@
(*Possibility property ending with ServerFinished.*)
goal thy
"!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
-\ A ~= B |] ==> EX NA XA NB XB M. EX evs: tls. \
+\ A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls. \
\ Says B A (Crypt (serverK(NA,NB,M)) \
-\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+\ (Hash{|Nonce M, Number SID, \
+\ Nonce NA, Number XA, Agent A, \
\ Nonce NB, Number XB, Agent B|})) \
\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -125,9 +126,10 @@
(*And one for ClientFinished. Either FINISHED message may come first.*)
goal thy
"!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
-\ A ~= B |] ==> EX NA XA NB XB M. EX evs: tls. \
+\ A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls. \
\ Says A B (Crypt (clientK(NA,NB,M)) \
-\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+\ (Hash{|Nonce M, Number SID, \
+\ Nonce NA, Number XA, Agent A, \
\ Nonce NB, Number XB, Agent B|})) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
@@ -292,7 +294,7 @@
"!!evs. [| X = Crypt (priK A) \
\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|}); \
\ evs : tls; A ~: lost; B ~= Spy |] \
-\ ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} \
+\ ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|} \
\ : set evs --> \
\ X : parts (sees Spy evs) --> Says A B X : set evs";
by (hyp_subst_tac 1);
@@ -588,12 +590,13 @@
(*The mention of her name (A) in X assumes A that B knows who she is.*)
goal thy
- "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
-\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+ "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
+\ (Hash{|Nonce M, Number SID, \
+\ Nonce NA, Number XA, Agent A, \
\ Nonce NB, Number XB, Agent B|}); \
-\ M = PRF(PMS,NA,NB); \
-\ evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ M = PRF(PMS,NA,NB); \
+\ evs : tls; A ~: lost; B ~: lost |] \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ X : parts (sees Spy evs) --> Says B A X : set evs";
by (hyp_subst_tac 1);
by (analz_induct_tac 1);
@@ -674,7 +677,7 @@
***)
goal thy
"!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
-\ Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} \
+\ Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|} \
\ : set evs; \
\ Says A'' B (Crypt (priK A) \
\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|})) \
--- a/src/HOL/Auth/TLS.thy Tue Sep 16 14:04:10 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Tue Sep 16 14:40:01 1997 +0200
@@ -87,22 +87,23 @@
(*(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.
- May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
- while MASTER SECRET is 48 byptes (6.1)*)
+ NA is CLIENT RANDOM, while SID is SESSION_ID.
+ UNIX TIME is omitted because the protocol doesn't use it.
+ May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
+ while MASTER SECRET is 48 byptes*)
"[| evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF |]
- ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH : tls"
+ ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
+ # evsCH : tls"
ServerHello
(*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,
+ Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
+ : set evsSH |]
+ ==> Says B A {|Nonce NB, Number SID, Number XB,
certificate B (pubK B)|}
# evsSH : tls"
@@ -116,7 +117,7 @@
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|}
+ Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
: set evsCX |]
==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
# Notes A {|Agent B, Nonce PMS|}
@@ -129,12 +130,12 @@
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|}
+ Says B' A {|Nonce NB, Number SID, 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 PMS|}))
- # evsCV : tls"
+ # evsCV : tls"
(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
among other things. The master-secret is PRF(PMS,NA,NB).
@@ -148,33 +149,35 @@
expect the spy to be well-behaved.*)
ClientFinished
"[| 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|}
+ Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
+ : set evsCF;
+ Says B' A {|Nonce NB, Number SID, 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{|Nonce M,
+ (Hash{|Nonce M, Number SID,
Nonce NA, Number XA, Agent A,
Nonce NB, Number XB, Agent B|}))
- # evsCF : tls"
+ # evsCF : tls"
(*Keeping A' and A'' distinct means B cannot even check that the
two messages originate from the same source. *)
ServerFinished
"[| evsSF: tls;
- Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSF;
- Says B A {|Nonce NA, Nonce NB, Number XB,
+ Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
+ : set evsSF;
+ Says B A {|Nonce NB, Number SID, Number XB,
certificate B (pubK B)|}
: 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{|Nonce M,
+ (Hash{|Nonce M, Number SID,
Nonce NA, Number XA, Agent A,
Nonce NB, Number XB, Agent B|}))
- # evsSF : tls"
+ # evsSF : tls"
(**Oops message??**)