--- a/src/HOL/Auth/KerberosIV.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Fri Nov 17 02:20:03 2006 +0100
@@ -11,11 +11,10 @@
text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
abbreviation
- Kas :: agent
- "Kas == Server"
+ Kas :: agent where "Kas == Server"
- Tgs :: agent
- "Tgs == Friend 0"
+abbreviation
+ Tgs :: agent where "Tgs == Friend 0"
axioms
@@ -79,19 +78,23 @@
abbreviation
(*The current time is the length of the trace*)
- CT :: "event list=>nat"
+ CT :: "event list=>nat" where
"CT == length"
- expiredAK :: "[nat, event list] => bool"
+abbreviation
+ expiredAK :: "[nat, event list] => bool" where
"expiredAK Ta evs == authKlife + Ta < CT evs"
- expiredSK :: "[nat, event list] => bool"
+abbreviation
+ expiredSK :: "[nat, event list] => bool" where
"expiredSK Ts evs == servKlife + Ts < CT evs"
- expiredA :: "[nat, event list] => bool"
+abbreviation
+ expiredA :: "[nat, event list] => bool" where
"expiredA T evs == authlife + T < CT evs"
- valid :: "[nat, nat] => bool" ("valid _ wrt _")
+abbreviation
+ valid :: "[nat, nat] => bool" ("valid _ wrt _") where
"valid T1 wrt T2 == T1 <= replylife + T2"
(*---------------------------------------------------------------------*)