src/HOL/Auth/TLS.thy
changeset 5653 204083e3f368
parent 5434 9b4bed3f394c
child 6284 147db42c1009
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Oct 16 12:20:41 1998 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Oct 16 12:23:07 1998 +0200
     1.3 @@ -41,28 +41,26 @@
     1.4  
     1.5  TLS = Public + 
     1.6  
     1.7 +constdefs
     1.8 +  certificate      :: "[agent,key] => msg"
     1.9 +    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    1.10 +
    1.11  consts
    1.12    (*Pseudo-random function of Section 5*)
    1.13    PRF  :: "nat*nat*nat => nat"
    1.14  
    1.15    (*Client, server write keys are generated uniformly by function sessionK
    1.16 -    to avoid duplicating their properties.  They are indexed by a further
    1.17 -    natural number, not a bool, to avoid the peculiarities of if-and-only-if.
    1.18 +    to avoid duplicating their properties.  They are distinguished by a
    1.19 +    tag (not a bool, to avoid the peculiarities of if-and-only-if).
    1.20      Session keys implicitly include MAC secrets.*)
    1.21 -  sessionK :: "(nat*nat*nat)*nat => key"
    1.22 -
    1.23 -  certificate      :: "[agent,key] => msg"
    1.24 -
    1.25 -defs
    1.26 -  certificate_def
    1.27 -    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    1.28 +  sessionK :: "(nat*nat*nat) * (unit option) => key"
    1.29  
    1.30  syntax
    1.31      clientK, serverK :: "nat*nat*nat => key"
    1.32  
    1.33  translations
    1.34 -  "clientK X" == "sessionK(X,0)"
    1.35 -  "serverK X" == "sessionK(X,1)"
    1.36 +  "clientK X" == "sessionK(X,None)"
    1.37 +  "serverK X" == "sessionK(X,Some())"
    1.38  
    1.39  rules
    1.40    (*the pseudo-random function is collision-free*)