changed tags from 0, 1 to None, Some() to avoid special treatment of 0
authorpaulson
Fri Oct 16 12:23:07 1998 +0200 (1998-10-16)
changeset 5653204083e3f368
parent 5652 fe5f5510aef4
child 5654 8b872d546b9e
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Oct 16 12:20:41 1998 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Fri Oct 16 12:23:07 1998 +0200
     1.3 @@ -526,12 +526,9 @@
     1.4  \     ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)";
     1.5  by (etac rev_mp 1);
     1.6  by (etac rev_mp 1);
     1.7 -(* FIXME zero_neq_conv *)
     1.8 -DelIffs [zero_neq_conv];
     1.9  by (analz_induct_tac 1);        (*17 seconds*)
    1.10  (*Oops*)
    1.11  by (blast_tac (claset() addIs [Says_clientK_unique]) 4);
    1.12 -AddIffs [zero_neq_conv];
    1.13  (*ClientKeyExch*)
    1.14  by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]) 3);
    1.15  (*SpyKeys*)
     2.1 --- a/src/HOL/Auth/TLS.thy	Fri Oct 16 12:20:41 1998 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Fri Oct 16 12:23:07 1998 +0200
     2.3 @@ -41,28 +41,26 @@
     2.4  
     2.5  TLS = Public + 
     2.6  
     2.7 +constdefs
     2.8 +  certificate      :: "[agent,key] => msg"
     2.9 +    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    2.10 +
    2.11  consts
    2.12    (*Pseudo-random function of Section 5*)
    2.13    PRF  :: "nat*nat*nat => nat"
    2.14  
    2.15    (*Client, server write keys are generated uniformly by function sessionK
    2.16 -    to avoid duplicating their properties.  They are indexed by a further
    2.17 -    natural number, not a bool, to avoid the peculiarities of if-and-only-if.
    2.18 +    to avoid duplicating their properties.  They are distinguished by a
    2.19 +    tag (not a bool, to avoid the peculiarities of if-and-only-if).
    2.20      Session keys implicitly include MAC secrets.*)
    2.21 -  sessionK :: "(nat*nat*nat)*nat => key"
    2.22 -
    2.23 -  certificate      :: "[agent,key] => msg"
    2.24 -
    2.25 -defs
    2.26 -  certificate_def
    2.27 -    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    2.28 +  sessionK :: "(nat*nat*nat) * (unit option) => key"
    2.29  
    2.30  syntax
    2.31      clientK, serverK :: "nat*nat*nat => key"
    2.32  
    2.33  translations
    2.34 -  "clientK X" == "sessionK(X,0)"
    2.35 -  "serverK X" == "sessionK(X,1)"
    2.36 +  "clientK X" == "sessionK(X,None)"
    2.37 +  "serverK X" == "sessionK(X,Some())"
    2.38  
    2.39  rules
    2.40    (*the pseudo-random function is collision-free*)