src/HOL/Auth/TLS.thy
changeset 3704 2f99d7a0dccc
parent 3687 fb7d096d7884
child 3710 ea830f6e3c2d
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Sep 24 12:26:14 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Wed Sep 24 12:27:53 1997 +0200
     1.3 @@ -45,10 +45,11 @@
     1.4    (*Pseudo-random function of Section 5*)
     1.5    PRF  :: "nat*nat*nat => nat"
     1.6  
     1.7 -  (*Client, server write keys generated uniformly by function sessionK
     1.8 -    to avoid duplicating their properties.
     1.9 -    Theyimplicitly include the MAC secrets.*)
    1.10 -  sessionK :: "(nat*nat*nat)*bool => key"
    1.11 +  (*Client, server write keys are generated uniformly by function sessionK
    1.12 +    to avoid duplicating their properties.  They are indexed by a further
    1.13 +    natural number, not a bool, to avoid the peculiarities of if-and-only-if.
    1.14 +    Session keys implicitly include MAC secrets.*)
    1.15 +  sessionK :: "(nat*nat*nat)*nat => key"
    1.16  
    1.17    certificate      :: "[agent,key] => msg"
    1.18  
    1.19 @@ -60,8 +61,8 @@
    1.20      clientK, serverK :: "nat*nat*nat => key"
    1.21  
    1.22  translations
    1.23 -  "clientK (x)"	== "sessionK(x,True)"
    1.24 -  "serverK (x)"	== "sessionK(x,False)"
    1.25 +  "clientK (x)"	== "sessionK(x,0)"
    1.26 +  "serverK (x)"	== "sessionK(x,1)"
    1.27  
    1.28  rules
    1.29    inj_PRF       "inj PRF"