# HG changeset patch
# User paulson
# Date 908533387 -7200
# Node ID 204083e3f368d248cb625ccfa0a6363c926e1815
# Parent  fe5f5510aef49935cee5efd767beff1cb8fc3333
changed tags from 0, 1 to None, Some() to avoid special treatment of 0

diff -r fe5f5510aef4 -r 204083e3f368 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Fri Oct 16 12:20:41 1998 +0200
+++ b/src/HOL/Auth/TLS.ML	Fri Oct 16 12:23:07 1998 +0200
@@ -526,12 +526,9 @@
 \     ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
-(* FIXME zero_neq_conv *)
-DelIffs [zero_neq_conv];
 by (analz_induct_tac 1);        (*17 seconds*)
 (*Oops*)
 by (blast_tac (claset() addIs [Says_clientK_unique]) 4);
-AddIffs [zero_neq_conv];
 (*ClientKeyExch*)
 by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]) 3);
 (*SpyKeys*)
diff -r fe5f5510aef4 -r 204083e3f368 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Fri Oct 16 12:20:41 1998 +0200
+++ b/src/HOL/Auth/TLS.thy	Fri Oct 16 12:23:07 1998 +0200
@@ -41,28 +41,26 @@
 
 TLS = Public + 
 
+constdefs
+  certificate      :: "[agent,key] => msg"
+    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
+
 consts
   (*Pseudo-random function of Section 5*)
   PRF  :: "nat*nat*nat => nat"
 
   (*Client, server write keys are generated uniformly by function sessionK
-    to avoid duplicating their properties.  They are indexed by a further
-    natural number, not a bool, to avoid the peculiarities of if-and-only-if.
+    to avoid duplicating their properties.  They are distinguished by a
+    tag (not a bool, to avoid the peculiarities of if-and-only-if).
     Session keys implicitly include MAC secrets.*)
-  sessionK :: "(nat*nat*nat)*nat => key"
-
-  certificate      :: "[agent,key] => msg"
-
-defs
-  certificate_def
-    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
+  sessionK :: "(nat*nat*nat) * (unit option) => key"
 
 syntax
     clientK, serverK :: "nat*nat*nat => key"
 
 translations
-  "clientK X" == "sessionK(X,0)"
-  "serverK X" == "sessionK(X,1)"
+  "clientK X" == "sessionK(X,None)"
+  "serverK X" == "sessionK(X,Some())"
 
 rules
   (*the pseudo-random function is collision-free*)