src/HOL/Auth/TLS.thy
changeset 3686 4b484805b4c4
parent 3685 5b8c0c8f576e
child 3687 fb7d096d7884
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 19 16:12:21 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Sep 19 18:27:31 1997 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4    (*Client, server write keys generated uniformly by function sessionK
     1.5      to avoid duplicating their properties.
     1.6      Theyimplicitly include the MAC secrets.*)
     1.7 -  sessionK :: "bool*nat*nat*nat => key"
     1.8 +  sessionK :: "(nat*nat*nat)*bool => key"
     1.9  
    1.10    certificate      :: "[agent,key] => msg"
    1.11  
    1.12 @@ -60,8 +60,8 @@
    1.13      clientK, serverK :: "nat*nat*nat => key"
    1.14  
    1.15  translations
    1.16 -  "clientK (x)"	== "sessionK(True,x)"
    1.17 -  "serverK (x)"	== "sessionK(False,x)"
    1.18 +  "clientK (x)"	== "sessionK(x,True)"
    1.19 +  "serverK (x)"	== "sessionK(x,False)"
    1.20  
    1.21  rules
    1.22    inj_PRF       "inj PRF"	
    1.23 @@ -252,6 +252,12 @@
    1.24  			       Nonce NB, Number XB, Agent B|}))
    1.25                # evsCR  :  tls"
    1.26  
    1.27 -  (**Oops message??**)
    1.28 +    Oops 
    1.29 +         (*The most plausible compromise is of an old session key.  Losing
    1.30 +           the MASTER SECRET or PREMASTER SECRET is more serious but
    1.31 +           rather unlikely.*)
    1.32 +         "[| evso: tls;  A ~= Spy;  
    1.33 +	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
    1.34 +          ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
    1.35  
    1.36  end