--- a/src/HOL/Auth/TLS.ML Mon Sep 29 11:45:52 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Mon Sep 29 11:46:33 1997 +0200
@@ -13,7 +13,7 @@
* A upon receiving ServerFinished knows that B is present
* Each party who has received a FINISHED message can trust that the other
- party agrees on all message components, including XA and XB (thus foiling
+ party agrees on all message components, including PA and PB (thus foiling
rollback attacks).
*)
@@ -102,7 +102,7 @@
(*And one for ServerAccepts. Either FINISHED message may come first.*)
goal thy
"!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
-\ A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls. \
+\ A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls. \
\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
@@ -115,8 +115,7 @@
goal thy
"!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
\ A ~= B |] ==> EX NB PMS. EX evs: tls. \
-\ Says A B (Crypt (priK A) \
-\ (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
+\ Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
RS tls.CertVerify) 2);
@@ -130,11 +129,11 @@
\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \
-\ A ~= B |] ==> EX NA XA NB XB. EX evs: tls. \
+\ A ~= B |] ==> EX NA PA NB PB. EX evs: tls. \
\ Says A B (Crypt (clientK(NA,NB,M)) \
\ (Hash{|Nonce M, Number SID, \
-\ Nonce NA, Number XA, Agent A, \
-\ Nonce NB, Number XB, Agent B|})) : set evs";
+\ Nonce NA, Number PA, Agent A, \
+\ Nonce NB, Number PB, Agent B|})) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
by possibility_tac;
@@ -301,10 +300,9 @@
message is Fake. We don't need guarantees for the Spy anyway. We must
assume A~:bad; otherwise, the Spy can forge A's signature.*)
goal thy
- "!!evs. [| X = Crypt (priK A) \
-\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|}); \
+ "!!evs. [| X = Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}); \
\ evs : tls; A ~: bad; B ~= Spy |] \
-\ ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|} \
+\ ==> Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|} \
\ : set evs --> \
\ X : parts (spies evs) --> Says A B X : set evs";
by (hyp_subst_tac 1);
@@ -318,7 +316,7 @@
(*If CertVerify is present then A has chosen PMS.*)
goal thy
- "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|}) \
+ "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}) \
\ : parts (spies evs); \
\ evs : tls; A ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
@@ -692,8 +690,8 @@
(*** Protocol goals: if A receives ServerFinished, then B is present
- and has used the quoted values XA, XB, etc. Note that it is up to A
- to compare XA with what she originally sent.
+ and has used the quoted values PA, PB, etc. Note that it is up to A
+ to compare PA with what she originally sent.
***)
(*The mention of her name (A) in X assures A that B knows who she is.*)
@@ -701,8 +699,8 @@
"!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
\ X = Crypt (serverK(Na,Nb,M)) \
\ (Hash{|Nonce M, Number SID, \
-\ Nonce NA, Number XA, Agent A, \
-\ Nonce NB, Number XB, Agent B|}); \
+\ Nonce NA, Number PA, Agent A, \
+\ Nonce NB, Number PB, Agent B|}); \
\ M = PRF(PMS,NA,NB); \
\ evs : tls; A ~: bad; B ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
@@ -727,8 +725,8 @@
goal thy
"!!evs. [| X = Crypt (serverK(Na,Nb,M)) \
\ (Hash{|Nonce M, Number SID, \
-\ Nonce NA, Number XA, Agent A, \
-\ Nonce NB, Number XB, Agent B|}); \
+\ Nonce NA, Number PA, Agent A, \
+\ Nonce NB, Number PB, Agent B|}); \
\ M = PRF(PMS,NA,NB); \
\ X : parts (spies evs); \
\ Notes A {|Agent B, Nonce PMS|} : set evs; \
@@ -794,7 +792,7 @@
(*** Protocol goal: if B receives any message encrypted with clientK
then A has sent it, ASSUMING that A chose PMS. Authentication is
assumed here; B cannot verify it. But if the message is
- ClientFinished, then B can then check the quoted values XA, XB, etc.
+ ClientFinished, then B can then check the quoted values PA, PB, etc.
***)
goal thy
@@ -834,15 +832,14 @@
(*** Protocol goal: if B receives ClientFinished, and if B is able to
check a CertVerify from A, then A has used the quoted
- values XA, XB, etc. Even this one requires A to be uncompromised.
+ values PA, PB, etc. Even this one requires A to be uncompromised.
***)
goal thy
"!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
\ Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
-\ Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|} \
+\ Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|} \
\ : set evs; \
-\ Says A'' B (Crypt (priK A) \
-\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|})) \
+\ Says A'' B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))\
\ : set evs; \
\ evs : tls; A ~: bad; B ~: bad |] \
\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
--- a/src/HOL/Auth/TLS.thy Mon Sep 29 11:45:52 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Mon Sep 29 11:46:33 1997 +0200
@@ -93,25 +93,25 @@
ClientHello
(*(7.4.1.2)
- XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
+ PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
It is uninterpreted but will be confirmed in the FINISHED messages.
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 SID, Number XA|}
+ ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
# evsCH : tls"
ServerHello
(*7.4.1.3 of the TLS Internet-Draft
- XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
+ PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
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 SID, Number XA|}
+ Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsSH |]
- ==> Says B A {|Nonce NB, Number SID, Number XB,
+ ==> Says B A {|Nonce NB, Number SID, Number PB,
certificate B (pubK B)|}
# evsSH : tls"
@@ -125,7 +125,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 NB, Number SID, Number XB, certificate B KB|}
+ Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
: set evsCX |]
==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
# Notes A {|Agent B, Nonce PMS|}
@@ -138,14 +138,13 @@
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 NB, Number SID, Number XB, certificate B KB|}
+ Says B' A {|Nonce NB, Number SID, Number PB, 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|}))
+ ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
# evsCV : tls"
- (*Finally come the FINISHED messages (7.4.8), confirming XA and XB
+ (*Finally come the FINISHED messages (7.4.8), confirming PA and PB
among other things. The master-secret is PRF(PMS,NA,NB).
Either party may sent its message first.*)
@@ -157,25 +156,25 @@
could simply put A~=Spy into the rule, but one should not
expect the spy to be well-behaved.*)
"[| evsCF: tls;
- Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
+ Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsCF;
- Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
+ Says B' A {|Nonce NB, Number SID, Number PB, 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, Number SID,
- Nonce NA, Number XA, Agent A,
- Nonce NB, Number XB, Agent B|}))
+ Nonce NA, Number PA, Agent A,
+ Nonce NB, Number PB, Agent B|}))
# evsCF : tls"
ServerFinished
(*Keeping A' and A'' distinct means B cannot even check that the
two messages originate from the same source. *)
"[| evsSF: tls;
- Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
+ Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsSF;
- Says B A {|Nonce NB, Number SID, Number XB,
+ Says B A {|Nonce NB, Number SID, Number PB,
certificate B (pubK B)|}
: set evsSF;
Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
@@ -183,8 +182,8 @@
M = PRF(PMS,NA,NB) |]
==> Says B A (Crypt (serverK(NA,NB,M))
(Hash{|Nonce M, Number SID,
- Nonce NA, Number XA, Agent A,
- Nonce NB, Number XB, Agent B|}))
+ Nonce NA, Number PA, Agent A,
+ Nonce NB, Number PB, Agent B|}))
# evsSF : tls"
ClientAccepts
@@ -196,8 +195,8 @@
Notes A {|Agent B, Nonce PMS|} : set evsCA;
M = PRF(PMS,NA,NB);
X = Hash{|Nonce M, Number SID,
- Nonce NA, Number XA, Agent A,
- Nonce NB, Number XB, Agent B|};
+ Nonce NA, Number PA, Agent A,
+ Nonce NB, Number PB, Agent B|};
Says A B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
==>
@@ -213,8 +212,8 @@
: set evsSA;
M = PRF(PMS,NA,NB);
X = Hash{|Nonce M, Number SID,
- Nonce NA, Number XA, Agent A,
- Nonce NB, Number XB, Agent B|};
+ Nonce NA, Number PA, Agent A,
+ Nonce NB, Number PB, Agent B|};
Says B A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
==>
@@ -226,26 +225,26 @@
previously stored MASTER SECRET*)
"[| evsSR: tls; A ~= B; Nonce NB ~: used evsSR; NB ~: range PRF;
Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
- Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
+ Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsSR |]
==> Says B A (Crypt (serverK(NA,NB,M))
(Hash{|Nonce M, Number SID,
- Nonce NA, Number XA, Agent A,
- Nonce NB, Number XB, Agent B|}))
- # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR : tls"
+ Nonce NA, Number PA, Agent A,
+ Nonce NB, Number PB, Agent B|}))
+ # Says B A {|Nonce NB, Number SID, Number PB|} # evsSR : tls"
ClientResume
(*If the response to ClientHello is ServerResume then send
a FINISHED message using the new nonces and stored MASTER SECRET.*)
"[| evsCR: tls;
- Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
+ Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
: set evsCR;
- Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
+ Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
==> Says A B (Crypt (clientK(NA,NB,M))
(Hash{|Nonce M, Number SID,
- Nonce NA, Number XA, Agent A,
- Nonce NB, Number XB, Agent B|}))
+ Nonce NA, Number PA, Agent A,
+ Nonce NB, Number PB, Agent B|}))
# evsCR : tls"
Oops