--- 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|})) \