src/HOL/Auth/TLS.ML
changeset 3676 cbaec955056b
parent 3672 56e4365a0c99
child 3677 f2569416d18b
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Sep 16 14:04:10 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Sep 16 14:40:01 1997 +0200
     1.3 @@ -110,9 +110,10 @@
     1.4  (*Possibility property ending with ServerFinished.*)
     1.5  goal thy 
     1.6   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
     1.7 -\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
     1.8 +\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
     1.9  \  Says B A (Crypt (serverK(NA,NB,M))                       \
    1.10 -\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A,      \
    1.11 +\            (Hash{|Nonce M, Number SID,             \
    1.12 +\                   Nonce NA, Number XA, Agent A,      \
    1.13  \                   Nonce NB, Number XB, Agent B|})) \
    1.14  \    : set evs";
    1.15  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.16 @@ -125,9 +126,10 @@
    1.17  (*And one for ClientFinished.  Either FINISHED message may come first.*)
    1.18  goal thy 
    1.19   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.20 -\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
    1.21 +\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
    1.22  \  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.23 -\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
    1.24 +\            (Hash{|Nonce M, Number SID,             \
    1.25 +\                   Nonce NA, Number XA, Agent A,      \
    1.26  \                   Nonce NB, Number XB, Agent B|})) : set evs";
    1.27  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.28  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.29 @@ -292,7 +294,7 @@
    1.30   "!!evs. [| X = Crypt (priK A)                                        \
    1.31  \                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
    1.32  \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
    1.33 -\    ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
    1.34 +\    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
    1.35  \          : set evs --> \
    1.36  \        X : parts (sees Spy evs) --> Says A B X : set evs";
    1.37  by (hyp_subst_tac 1);
    1.38 @@ -588,12 +590,13 @@
    1.39  
    1.40  (*The mention of her name (A) in X assumes A that B knows who she is.*)
    1.41  goal thy
    1.42 - "!!evs. [| X = Crypt (serverK(Na,Nb,M))                                \
    1.43 -\                 (Hash{|Nonce M, Nonce NA, Number XA, Agent A,         \
    1.44 + "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
    1.45 +\                 (Hash{|Nonce M, Number SID,             \
    1.46 +\                        Nonce NA, Number XA, Agent A,    \
    1.47  \                        Nonce NB, Number XB, Agent B|}); \
    1.48 -\           M = PRF(PMS,NA,NB); \
    1.49 -\           evs : tls;  A ~: lost;  B ~: lost |]                        \
    1.50 -\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                 \
    1.51 +\           M = PRF(PMS,NA,NB);                           \
    1.52 +\           evs : tls;  A ~: lost;  B ~: lost |]          \
    1.53 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
    1.54  \        X : parts (sees Spy evs) --> Says B A X : set evs";
    1.55  by (hyp_subst_tac 1);
    1.56  by (analz_induct_tac 1);
    1.57 @@ -674,7 +677,7 @@
    1.58   ***)
    1.59  goal thy
    1.60   "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
    1.61 -\           Says B  A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
    1.62 +\           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
    1.63  \             : set evs;                                                  \
    1.64  \           Says A'' B (Crypt (priK A)                                    \
    1.65  \                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \