src/HOL/Auth/TLS.ML
changeset 3729 6be7cf5086ab
parent 3711 2f86b403d975
child 3745 4c5d3b1ddc75
     1.1 --- a/src/HOL/Auth/TLS.ML	Mon Sep 29 11:45:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Mon Sep 29 11:46:33 1997 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  * A upon receiving ServerFinished knows that B is present
     1.5  
     1.6  * Each party who has received a FINISHED message can trust that the other
     1.7 -  party agrees on all message components, including XA and XB (thus foiling
     1.8 +  party agrees on all message components, including PA and PB (thus foiling
     1.9    rollback attacks).
    1.10  *)
    1.11  
    1.12 @@ -102,7 +102,7 @@
    1.13  (*And one for ServerAccepts.  Either FINISHED message may come first.*)
    1.14  goal thy 
    1.15   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.16 -\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
    1.17 +\           A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls.    \
    1.18  \  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.19  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.20  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.21 @@ -115,8 +115,7 @@
    1.22  goal thy 
    1.23   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.24  \           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
    1.25 -\  Says A B (Crypt (priK A)                 \
    1.26 -\            (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
    1.27 +\  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
    1.28  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.29  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.30  	  RS tls.CertVerify) 2);
    1.31 @@ -130,11 +129,11 @@
    1.32  \           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.33  \           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.34  \           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.35 -\           A ~= B |] ==> EX NA XA NB XB. EX evs: tls.    \
    1.36 +\           A ~= B |] ==> EX NA PA NB PB. EX evs: tls.    \
    1.37  \  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.38  \            (Hash{|Nonce M, Number SID,             \
    1.39 -\                   Nonce NA, Number XA, Agent A,      \
    1.40 -\                   Nonce NB, Number XB, Agent B|})) : set evs";
    1.41 +\                   Nonce NA, Number PA, Agent A,      \
    1.42 +\                   Nonce NB, Number PB, Agent B|})) : set evs";
    1.43  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.44  by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
    1.45  by possibility_tac;
    1.46 @@ -301,10 +300,9 @@
    1.47    message is Fake.  We don't need guarantees for the Spy anyway.  We must
    1.48    assume A~:bad; otherwise, the Spy can forge A's signature.*)
    1.49  goal thy
    1.50 - "!!evs. [| X = Crypt (priK A)                                        \
    1.51 -\                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
    1.52 + "!!evs. [| X = Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|});      \
    1.53  \           evs : tls;  A ~: bad;  B ~= Spy |]                       \
    1.54 -\    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
    1.55 +\    ==> Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
    1.56  \          : set evs --> \
    1.57  \        X : parts (spies evs) --> Says A B X : set evs";
    1.58  by (hyp_subst_tac 1);
    1.59 @@ -318,7 +316,7 @@
    1.60  
    1.61  (*If CertVerify is present then A has chosen PMS.*)
    1.62  goal thy
    1.63 - "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
    1.64 + "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})  \
    1.65  \             : parts (spies evs);                                \
    1.66  \           evs : tls;  A ~: bad |]                                      \
    1.67  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
    1.68 @@ -692,8 +690,8 @@
    1.69  
    1.70  
    1.71  (*** Protocol goals: if A receives ServerFinished, then B is present 
    1.72 -     and has used the quoted values XA, XB, etc.  Note that it is up to A
    1.73 -     to compare XA with what she originally sent.
    1.74 +     and has used the quoted values PA, PB, etc.  Note that it is up to A
    1.75 +     to compare PA with what she originally sent.
    1.76  ***)
    1.77  
    1.78  (*The mention of her name (A) in X assures A that B knows who she is.*)
    1.79 @@ -701,8 +699,8 @@
    1.80   "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
    1.81  \           X = Crypt (serverK(Na,Nb,M))                  \
    1.82  \                 (Hash{|Nonce M, Number SID,             \
    1.83 -\                        Nonce NA, Number XA, Agent A,    \
    1.84 -\                        Nonce NB, Number XB, Agent B|}); \
    1.85 +\                        Nonce NA, Number PA, Agent A,    \
    1.86 +\                        Nonce NB, Number PB, Agent B|}); \
    1.87  \           M = PRF(PMS,NA,NB);                           \
    1.88  \           evs : tls;  A ~: bad;  B ~: bad |]          \
    1.89  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
    1.90 @@ -727,8 +725,8 @@
    1.91  goal thy
    1.92   "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
    1.93  \                 (Hash{|Nonce M, Number SID,             \
    1.94 -\                        Nonce NA, Number XA, Agent A,    \
    1.95 -\                        Nonce NB, Number XB, Agent B|}); \
    1.96 +\                        Nonce NA, Number PA, Agent A,    \
    1.97 +\                        Nonce NB, Number PB, Agent B|}); \
    1.98  \           M = PRF(PMS,NA,NB);                           \
    1.99  \           X : parts (spies evs);                        \
   1.100  \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   1.101 @@ -794,7 +792,7 @@
   1.102  (*** Protocol goal: if B receives any message encrypted with clientK
   1.103       then A has sent it, ASSUMING that A chose PMS.  Authentication is
   1.104       assumed here; B cannot verify it.  But if the message is
   1.105 -     ClientFinished, then B can then check the quoted values XA, XB, etc.
   1.106 +     ClientFinished, then B can then check the quoted values PA, PB, etc.
   1.107  ***)
   1.108  
   1.109  goal thy
   1.110 @@ -834,15 +832,14 @@
   1.111  
   1.112  (*** Protocol goal: if B receives ClientFinished, and if B is able to
   1.113       check a CertVerify from A, then A has used the quoted
   1.114 -     values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.115 +     values PA, PB, etc.  Even this one requires A to be uncompromised.
   1.116   ***)
   1.117  goal thy
   1.118   "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   1.119  \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.120 -\           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   1.121 +\           Says B  A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
   1.122  \             : set evs;                                                  \
   1.123 -\           Says A'' B (Crypt (priK A)                                    \
   1.124 -\                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
   1.125 +\           Says A'' B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))\
   1.126  \             : set evs;                                                  \
   1.127  \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   1.128  \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";