src/HOL/Auth/TLS.thy
changeset 3677 f2569416d18b
parent 3676 cbaec955056b
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/TLS.thy	Tue Sep 16 14:40:01 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Wed Sep 17 16:37:21 1997 +0200
     1.3 @@ -41,8 +41,10 @@
     1.4    (*Pseudo-random function of Section 5*)
     1.5    PRF  :: "nat*nat*nat => nat"
     1.6  
     1.7 -  (*Client, server write keys implicitly include the MAC secrets.*)
     1.8 -  clientK, serverK :: "nat*nat*nat => key"
     1.9 +  (*Client, server write keys generated uniformly by function sessionK
    1.10 +    to avoid duplicating their properties.
    1.11 +    Theyimplicitly include the MAC secrets.*)
    1.12 +  sessionK :: "bool*nat*nat*nat => key"
    1.13  
    1.14    certificate      :: "[agent,key] => msg"
    1.15  
    1.16 @@ -50,16 +52,24 @@
    1.17    certificate_def
    1.18      "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    1.19  
    1.20 +syntax
    1.21 +    clientK, serverK :: "nat*nat*nat => key"
    1.22 +
    1.23 +translations
    1.24 +  "clientK x"	== "sessionK(True,x)"
    1.25 +  "serverK x"	== "sessionK(False,x)"
    1.26 +
    1.27  rules
    1.28    inj_PRF       "inj PRF"	
    1.29  
    1.30 -  (*clientK is collision-free and makes symmetric keys*)
    1.31 -  inj_clientK   "inj clientK"	
    1.32 -  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    1.33 +  (*sessionK is collision-free and makes symmetric keys*)
    1.34 +  inj_sessionK  "inj sessionK"	
    1.35 +
    1.36 +  isSym_sessionK "isSymKey (sessionK x)"
    1.37  
    1.38    (*serverK is similar*)
    1.39    inj_serverK   "inj serverK"	
    1.40 -  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
    1.41 +  isSym_serverK "isSymKey (serverK x)"
    1.42  
    1.43    (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
    1.44    clientK_range "range clientK <= Compl (range serverK)"
    1.45 @@ -179,6 +189,37 @@
    1.46  			       Nonce NB, Number XB, Agent B|}))
    1.47                # evsSF  :  tls"
    1.48  
    1.49 +	(*Having transmitted CLIENT FINISHED and received an identical
    1.50 +          message encrypted with serverK, the client stores the parameters
    1.51 +          needed to resume this session.*)
    1.52 +    ClientAccepts
    1.53 +         "[| evsCA: tls;
    1.54 +             Notes A {|Agent B, Nonce PMS|} : set evsCA;
    1.55 +	     M = PRF(PMS,NA,NB);  
    1.56 +	     X = Hash{|Nonce M, Number SID,
    1.57 +	               Nonce NA, Number XA, Agent A, 
    1.58 +		       Nonce NB, Number XB, Agent B|};
    1.59 +             Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
    1.60 +             Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
    1.61 +          ==> 
    1.62 +             Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
    1.63 +
    1.64 +	(*Having transmitted SERVER FINISHED and received an identical
    1.65 +          message encrypted with clientK, the server stores the parameters
    1.66 +          needed to resume this session.*)
    1.67 +    ServerAccepts
    1.68 +         "[| evsSA: tls;
    1.69 +             Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
    1.70 +	       : set evsSA;
    1.71 +	     M = PRF(PMS,NA,NB);  
    1.72 +	     X = Hash{|Nonce M, Number SID,
    1.73 +	               Nonce NA, Number XA, Agent A, 
    1.74 +		       Nonce NB, Number XB, Agent B|};
    1.75 +             Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
    1.76 +             Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
    1.77 +          ==> 
    1.78 +             Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
    1.79 +
    1.80    (**Oops message??**)
    1.81  
    1.82  end