src/HOL/Auth/TLS.thy
changeset 6284 147db42c1009
parent 5653 204083e3f368
child 11185 1b737b4c2108
     1.1 --- a/src/HOL/Auth/TLS.thy	Tue Feb 16 10:50:35 1999 +0100
     1.2 +++ b/src/HOL/Auth/TLS.thy	Tue Feb 16 10:54:55 1999 +0100
     1.3 @@ -45,6 +45,8 @@
     1.4    certificate      :: "[agent,key] => msg"
     1.5      "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
     1.6  
     1.7 +datatype role = ClientRole | ServerRole
     1.8 +
     1.9  consts
    1.10    (*Pseudo-random function of Section 5*)
    1.11    PRF  :: "nat*nat*nat => nat"
    1.12 @@ -53,14 +55,14 @@
    1.13      to avoid duplicating their properties.  They are distinguished by a
    1.14      tag (not a bool, to avoid the peculiarities of if-and-only-if).
    1.15      Session keys implicitly include MAC secrets.*)
    1.16 -  sessionK :: "(nat*nat*nat) * (unit option) => key"
    1.17 +  sessionK :: "(nat*nat*nat) * role => key"
    1.18  
    1.19  syntax
    1.20      clientK, serverK :: "nat*nat*nat => key"
    1.21  
    1.22  translations
    1.23 -  "clientK X" == "sessionK(X,None)"
    1.24 -  "serverK X" == "sessionK(X,Some())"
    1.25 +  "clientK X" == "sessionK(X, ClientRole)"
    1.26 +  "serverK X" == "sessionK(X, ServerRole)"
    1.27  
    1.28  rules
    1.29    (*the pseudo-random function is collision-free*)
    1.30 @@ -87,7 +89,7 @@
    1.31           "[| evsSK: tls;
    1.32  	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
    1.33            ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
    1.34 -			   Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
    1.35 +			   Key (sessionK((NA,NB,M),role)) |} # evsSK : tls"
    1.36  
    1.37      ClientHello
    1.38  	 (*(7.4.1.2)
    1.39 @@ -113,8 +115,7 @@
    1.40  
    1.41      Certificate
    1.42           (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
    1.43 -         "[| evsC: tls |]
    1.44 -          ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    1.45 +         "evsC: tls ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    1.46  
    1.47      ClientKeyExch
    1.48           (*CLIENT KEY EXCHANGE (7.4.7).
    1.49 @@ -151,7 +152,7 @@
    1.50          (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
    1.51            rule's applying when the Spy has satisfied the "Says A B" by
    1.52            repaying messages sent by the true client; in that case, the
    1.53 -          Spy does not know PMS and could not sent ClientFinished.  One
    1.54 +          Spy does not know PMS and could not send ClientFinished.  One
    1.55            could simply put A~=Spy into the rule, but one should not
    1.56            expect the spy to be well-behaved.*)
    1.57           "[| evsCF: tls;  
    1.58 @@ -246,7 +247,7 @@
    1.59             rather unlikely.  The assumption A ~= Spy is essential: otherwise
    1.60             the Spy could learn session keys merely by replaying messages!*)
    1.61           "[| evso: tls;  A ~= Spy;
    1.62 -	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
    1.63 -          ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
    1.64 +	     Says A B (Crypt (sessionK((NA,NB,M),role)) X) : set evso |]
    1.65 +          ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso  :  tls"
    1.66  
    1.67  end