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