# HG changeset patch
# User paulson
# Date 875706138 -7200
# Node ID 77f71f650433a9cc38574ce08df096a53273d409
# Parent  3d1ac6b82b28dc7ea2d8ae2916aae4627901744f
Strengthened the possibility property for resumption so that it could have
detected the problem with ServerResume

diff -r 3d1ac6b82b28 -r 77f71f650433 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Wed Oct 01 13:41:38 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Wed Oct 01 13:42:18 1997 +0200
@@ -90,8 +90,9 @@
 (*Possibility property ending with ClientAccepts.*)
 goal thy 
  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
-\           A ~= B |] ==> EX SID M. EX evs: tls.    \
-\  Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
+\           A ~= B |]            \
+\  ==> EX SID M. EX evs: tls.    \
+\        Notes A {|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.Certificate RS
 	  tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS
@@ -103,8 +104,9 @@
 (*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 PA NB PB M. EX evs: tls.    \
-\  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
+\           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.Certificate RS
 	  tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS
@@ -116,7 +118,8 @@
 (*Another one, for CertVerify (which is optional)*)
 goal thy 
  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
-\           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
+\           A ~= B |]                       \
+\  ==> EX NB PMS. EX evs: tls.   \
 \  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.Certificate RS
@@ -131,11 +134,12 @@
 \           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 PA NB PB. EX evs: tls.    \
-\  Says A B (Crypt (clientK(NA,NB,M))                           \
-\            (Hash{|Number SID, Nonce M,             \
-\                   Nonce NA, Number PA, Agent A,      \
-\                   Nonce NB, Number PB, Agent B|})) : set evs";
+\           A ~= B |] ==> EX NA PA NB PB X. EX evs: tls.    \
+\      X = Hash{|Number SID, Nonce M,             \
+\                       Nonce NA, Number PA, Agent A,      \
+\                       Nonce NB, Number PB, Agent B|}  &  \
+\      Says A B (Crypt (clientK(NA,NB,M)) X) : set evs  &  \
+\      Says B A (Crypt (serverK(NA,NB,M)) X) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS 
 	  tls.ClientResume) 2);
@@ -820,3 +824,4 @@
 (*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
 (*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
 (*30/9/97: loads in 476s, after removing unused theorems*)
+(*30/9/97: loads in 448s, after fixing ServerResume*)