Strengthened the possibility property for resumption so that it could have
authorpaulson
Wed Oct 01 13:42:18 1997 +0200 (1997-10-01)
changeset 376077f71f650433
parent 3759 3d1ac6b82b28
child 3761 d99d93d46ca5
Strengthened the possibility property for resumption so that it could have
detected the problem with ServerResume
src/HOL/Auth/TLS.ML
     1.1 --- a/src/HOL/Auth/TLS.ML	Wed Oct 01 13:41:38 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Wed Oct 01 13:42:18 1997 +0200
     1.3 @@ -90,8 +90,9 @@
     1.4  (*Possibility property ending with ClientAccepts.*)
     1.5  goal thy 
     1.6   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
     1.7 -\           A ~= B |] ==> EX SID M. EX evs: tls.    \
     1.8 -\  Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
     1.9 +\           A ~= B |]            \
    1.10 +\  ==> EX SID M. EX evs: tls.    \
    1.11 +\        Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.12  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.13  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    1.14  	  tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS
    1.15 @@ -103,8 +104,9 @@
    1.16  (*And one for ServerAccepts.  Either FINISHED message may come first.*)
    1.17  goal thy 
    1.18   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.19 -\           A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls.    \
    1.20 -\  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.21 +\           A ~= B |]                        \
    1.22 +\  ==> EX SID NA PA NB PB M. EX evs: tls.    \
    1.23 +\        Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.24  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.25  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    1.26  	  tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS
    1.27 @@ -116,7 +118,8 @@
    1.28  (*Another one, for CertVerify (which is optional)*)
    1.29  goal thy 
    1.30   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.31 -\           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
    1.32 +\           A ~= B |]                       \
    1.33 +\  ==> EX NB PMS. EX evs: tls.   \
    1.34  \  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
    1.35  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.36  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    1.37 @@ -131,11 +134,12 @@
    1.38  \           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.39  \           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.40  \           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.41 -\           A ~= B |] ==> EX NA PA NB PB. EX evs: tls.    \
    1.42 -\  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.43 -\            (Hash{|Number SID, Nonce M,             \
    1.44 -\                   Nonce NA, Number PA, Agent A,      \
    1.45 -\                   Nonce NB, Number PB, Agent B|})) : set evs";
    1.46 +\           A ~= B |] ==> EX NA PA NB PB X. EX evs: tls.    \
    1.47 +\      X = Hash{|Number SID, Nonce M,             \
    1.48 +\                       Nonce NA, Number PA, Agent A,      \
    1.49 +\                       Nonce NB, Number PB, Agent B|}  &  \
    1.50 +\      Says A B (Crypt (clientK(NA,NB,M)) X) : set evs  &  \
    1.51 +\      Says B A (Crypt (serverK(NA,NB,M)) X) : set evs";
    1.52  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.53  by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS 
    1.54  	  tls.ClientResume) 2);
    1.55 @@ -820,3 +824,4 @@
    1.56  (*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
    1.57  (*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
    1.58  (*30/9/97: loads in 476s, after removing unused theorems*)
    1.59 +(*30/9/97: loads in 448s, after fixing ServerResume*)