src/HOL/Auth/Kerberos_BAN.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Fri Jun 19 10:34:33 1998 +0200
@@ -0,0 +1,97 @@
+(*  Title:      HOL/Auth/Kerberos_BAN
+    ID:         $Id$
+    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Kerberos protocol, BAN version.
+
+From page 251 of
+  Burrows, Abadi and Needham.  A Logic of Authentication.
+  Proc. Royal Soc. 426 (1989)
+*)
+
+Kerberos_BAN = Shared + 
+
+(* Temporal modelization: session keys can be leaked 
+                          ONLY when they have expired *)
+
+syntax
+    CT :: event list=>nat
+    Expired :: [nat, event list] => bool
+    RecentAuth :: [nat, event list] => bool
+
+consts
+
+    (*Duration of the session key*)
+    SesKeyLife   :: nat
+
+    (*Duration of the authenticator*)
+    AutLife :: nat
+
+rules
+    (*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    "1 <= AutLife"
+
+translations
+   "CT" == "length"
+  
+   "Expired T evs" == "SesKeyLife + T < CT evs"
+
+   "RecentAuth T evs" == "CT evs <= AutLife + T"
+
+consts  kerberos_ban   :: event list set
+inductive "kerberos_ban"
+  intrs 
+
+    Nil  "[]: kerberos_ban"
+
+
+    Fake "[| evs: kerberos_ban;  B ~= Spy;  
+             X: synth (analz (spies evs)) |]
+          ==> Says Spy B X # evs : kerberos_ban"
+
+
+    Kb1  "[| evs1: kerberos_ban;  A ~= Server |]
+          ==> Says A Server {|Agent A, Agent B|} # evs1
+                :  kerberos_ban"
+
+
+    Kb2  "[| evs2: kerberos_ban;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
+             Says A' Server {|Agent A, Agent B|} : set evs2 |]
+          ==> Says Server A 
+                (Crypt (shrK A)
+                   {|Number (CT evs2), Agent B, Key KAB,  
+                    (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 
+                # evs2 : kerberos_ban"
+
+
+    Kb3  "[| evs3: kerberos_ban;  A ~= B; 
+             Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
+               : set evs3;
+             Says A Server {|Agent A, Agent B|} : set evs3;
+             ~ Expired Ts evs3 |]
+          ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 
+               # evs3 : kerberos_ban"
+
+
+    Kb4  "[| evs4: kerberos_ban;  A ~= B;  
+             Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
+		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
+             ~ Expired Ts evs4; 
+             RecentAuth Ta evs4|]
+          ==> Says B A (Crypt K (Number Ta)) # evs4
+                : kerberos_ban"
+
+
+(*The session key has EXPIRED when it gets lost *)
+    Oops "[| evso: kerberos_ban;  A ~= Spy;
+             Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+               : set evso;
+             Expired Ts evso |]
+          ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
+
+
+end