src/HOL/Auth/Kerberos_BAN.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5434 9b4bed3f394c
child 11185 1b737b4c2108
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Auth/Kerberos_BAN
     2     ID:         $Id$
     3     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The Kerberos protocol, BAN version.
     7 
     8 From page 251 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 Kerberos_BAN = Shared + 
    14 
    15 (* Temporal modelization: session keys can be leaked 
    16                           ONLY when they have expired *)
    17 
    18 syntax
    19     CT :: event list=>nat
    20     Expired :: [nat, event list] => bool
    21     RecentAuth :: [nat, event list] => bool
    22 
    23 consts
    24 
    25     (*Duration of the session key*)
    26     SesKeyLife   :: nat
    27 
    28     (*Duration of the authenticator*)
    29     AutLife :: nat
    30 
    31 rules
    32     (*The ticket should remain fresh for two journeys on the network at least*)
    33     SesKeyLife_LB    "2 <= SesKeyLife"
    34 
    35     (*The authenticator only for one journey*)
    36     AutLife_LB    "1 <= AutLife"
    37 
    38 translations
    39    "CT" == "length"
    40   
    41    "Expired T evs" == "SesKeyLife + T < CT evs"
    42 
    43    "RecentAuth T evs" == "CT evs <= AutLife + T"
    44 
    45 consts  kerberos_ban   :: event list set
    46 inductive "kerberos_ban"
    47   intrs 
    48 
    49     Nil  "[]: kerberos_ban"
    50 
    51     Fake "[| evs: kerberos_ban;  X: synth (analz (spies evs)) |]
    52           ==> Says Spy B X # evs : kerberos_ban"
    53 
    54 
    55     Kb1  "[| evs1: kerberos_ban |]
    56           ==> Says A Server {|Agent A, Agent B|} # evs1
    57                 :  kerberos_ban"
    58 
    59 
    60     Kb2  "[| evs2: kerberos_ban;  Key KAB ~: used evs2;
    61              Says A' Server {|Agent A, Agent B|} : set evs2 |]
    62           ==> Says Server A 
    63                 (Crypt (shrK A)
    64                    {|Number (CT evs2), Agent B, Key KAB,  
    65                     (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 
    66                 # evs2 : kerberos_ban"
    67 
    68 
    69     Kb3  "[| evs3: kerberos_ban;  
    70              Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
    71                : set evs3;
    72              Says A Server {|Agent A, Agent B|} : set evs3;
    73              ~ Expired Ts evs3 |]
    74           ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 
    75                # evs3 : kerberos_ban"
    76 
    77 
    78     Kb4  "[| evs4: kerberos_ban;  
    79              Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
    80 		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
    81              ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
    82           ==> Says B A (Crypt K (Number Ta)) # evs4
    83                 : kerberos_ban"
    84 
    85          (*Old session keys may become compromised*)
    86     Oops "[| evso: kerberos_ban;  
    87              Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    88                : set evso;
    89              Expired Ts evso |]
    90           ==> Notes Spy {|Number Ts, Key K|} # evso : kerberos_ban"
    91 
    92 
    93 end