src/HOL/Auth/Kerberos_BAN.thy

     SesKeyLife   :: nat
 
     (*Duration of the authenticator*)
     AutLife :: nat
 
-axioms
-    (*The ticket should remain fresh for two journeys on the network at least*)
-    SesKeyLife_LB: "2 <= SesKeyLife"
-
-    (*The authenticator only for one journey*)
-    AutLife_LB:    "Suc 0 <= AutLife"
+text{*The ticket should remain fresh for two journeys on the network at least*}
+specification (SesKeyLife)
+  SesKeyLife_LB [iff]: "2 \<le> SesKeyLife"
+    by blast
+
+text{*The authenticator only for one journey*}
+specification (AutLife)
+  AutLife_LB [iff]:    "Suc 0 \<le> AutLife"
+    by blast
+
 
 translations
    "CT" == "length"
   
    "Expired T evs" == "SesKeyLife + T < CT evs"
 
-   "RecentAuth T evs" == "CT evs <= AutLife + T"
+   "RecentAuth T evs" == "CT evs \<le> AutLife + T"
 
 consts  kerberos_ban   :: "event list set"
 inductive "kerberos_ban"
  intros 
 

 
 
 declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
 declare analz_subset_parts [THEN subsetD, dest]
 declare Fake_parts_insert [THEN subsetD, dest]
-
-declare SesKeyLife_LB [iff] AutLife_LB [iff]
-
 
 (*A "possibility property": there are traces that reach the end.*)
 lemma "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.     
              Says B A (Crypt K (Number Timestamp))  
                   \<in> set evs"

 
 (** Session keys are not used to encrypt other session keys **)
 
 lemma analz_image_freshK [rule_format (no_asm)]:
      "evs \<in> kerberos_ban ==>                           
-   \<forall>K KK. KK <= - (range shrK) -->                  
+   \<forall>K KK. KK \<subseteq> - (range shrK) -->                  
           (Key K \<in> analz (Key`KK Un (spies evs))) =   
           (K \<in> KK | Key K \<in> analz (spies evs))"
 apply (erule kerberos_ban.induct)
 apply (drule_tac [7] Says_Server_message_form)
 apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)