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