src/HOL/Auth/KerberosIV.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6452 6a1b393ccdc0
child 11185 1b737b4c2108
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Auth/KerberosIV
     2     ID:         $Id$
     3     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The Kerberos protocol, version IV.
     7 *)
     8 
     9 KerberosIV = Shared +
    10 
    11 syntax
    12   Kas, Tgs :: agent    (*the two servers are translations...*)
    13 
    14 
    15 translations
    16   "Kas"       == "Server"
    17   "Tgs"       == "Friend 0"   
    18 
    19 
    20 rules
    21   (*Tgs is secure --- we already know that Kas is secure*)
    22   Tgs_not_bad "Tgs ~: bad"
    23   
    24 (*The current time is just the length of the trace!*)
    25 syntax
    26     CT :: event list=>nat
    27 
    28     ExpirAuth :: [nat, event list] => bool
    29 
    30     ExpirServ :: [nat, event list] => bool 
    31 
    32     ExpirAutc :: [nat, event list] => bool 
    33 
    34     RecentResp :: [nat, nat] => bool
    35 
    36 
    37 constdefs
    38  (* AuthKeys are those contained in an AuthTicket *)
    39     AuthKeys :: event list => key set
    40     "AuthKeys evs == {AuthKey. EX A Peer Tk. Says Kas A
    41                         (Crypt (shrK A) {|Key AuthKey, Agent Peer, Tk, 
    42                    (Crypt (shrK Peer) {|Agent A, Agent Peer, Key AuthKey, Tk|})
    43                   |}) : set evs}"
    44                       
    45  (* A is the true creator of X if she has sent X and X never appeared on
    46     the trace before this event. Recall that traces grow from head. *)
    47   Issues :: [agent , agent, msg, event list] => bool ("_ Issues _ with _ on _")
    48    "A Issues B with X on evs == 
    49       EX Y. Says A B Y : set evs & X : parts {Y} &
    50       X ~: parts (spies (takeWhile (% z. z  ~= Says A B Y) (rev evs)))"
    51 
    52 
    53 consts
    54 
    55     (*Duration of the authentication key*)
    56     AuthLife   :: nat
    57 
    58     (*Duration of the service key*)
    59     ServLife   :: nat
    60 
    61     (*Duration of an authenticator*)
    62     AutcLife   :: nat
    63 
    64     (*Upper bound on the time of reaction of a server*)
    65     RespLife   :: nat 
    66 
    67 rules
    68      AuthLife_LB    "2 <= AuthLife"
    69      ServLife_LB    "2 <= ServLife"
    70      AutcLife_LB    "1 <= AutcLife" 
    71      RespLife_LB    "1 <= RespLife"
    72 
    73 translations
    74    "CT" == "length"
    75 
    76    "ExpirAuth T evs" == "AuthLife + T < CT evs"
    77 
    78    "ExpirServ T evs" == "ServLife + T < CT evs"
    79 
    80    "ExpirAutc T evs" == "AutcLife + T < CT evs"
    81 
    82    "RecentResp T1 T2" == "T1 <= RespLife + T2"
    83 
    84 (*---------------------------------------------------------------------*)
    85 
    86 
    87 (* Predicate formalising the association between AuthKeys and ServKeys *)
    88 constdefs 
    89   KeyCryptKey :: [key, key, event list] => bool
    90   "KeyCryptKey AuthKey ServKey evs ==
    91      EX A B tt. 
    92        Says Tgs A (Crypt AuthKey
    93                      {|Key ServKey, Agent B, tt,
    94                        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
    95          : set evs"
    96 
    97 consts
    98 
    99 kerberos   :: event list set
   100 inductive "kerberos"
   101   intrs 
   102         
   103     Nil  "[]: kerberos"
   104 
   105     Fake "[| evs: kerberos;  B ~= Spy;  
   106              X: synth (analz (spies evs)) |]
   107           ==> Says Spy B X  # evs : kerberos"
   108 
   109 (* FROM the initiator *)
   110     K1   "[| evs1: kerberos |]
   111           ==> Says A Kas {|Agent A, Agent Tgs, Number (CT evs1)|} # evs1 
   112           : kerberos"
   113 
   114 (* Adding the timestamp serves to A in K3 to check that
   115    she doesn't get a reply too late. This kind of timeouts are ordinary. 
   116    If a server's reply is late, then it is likely to be fake. *)
   117 
   118 (*---------------------------------------------------------------------*)
   119 
   120 (*FROM Kas *)
   121     K2  "[| evs2: kerberos; Key AuthKey ~: used evs2;
   122             Says A' Kas {|Agent A, Agent Tgs, Number Ta|} : set evs2 |]
   123           ==> Says Kas A
   124                 (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number (CT evs2), 
   125                       (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, 
   126                           Number (CT evs2)|})|}) # evs2 : kerberos"
   127 (* 
   128   The internal encryption builds the AuthTicket.
   129   The timestamp doesn't change inside the two encryptions: the external copy
   130   will be used by the initiator in K3; the one inside the 
   131   AuthTicket by Tgs in K4.
   132 *)
   133 
   134 (*---------------------------------------------------------------------*)
   135 
   136 (* FROM the initiator *)
   137     K3  "[| evs3: kerberos; 
   138             Says A Kas {|Agent A, Agent Tgs, Number Ta|} : set evs3;
   139             Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, 
   140               AuthTicket|}) : set evs3; 
   141             RecentResp Tk Ta
   142          |]
   143           ==> Says A Tgs {|AuthTicket, 
   144                            (Crypt AuthKey {|Agent A, Number (CT evs3)|}), 
   145                            Agent B|} # evs3 : kerberos"
   146 (*The two events amongst the premises allow A to accept only those AuthKeys 
   147   that are not issued late. *)
   148 
   149 (*---------------------------------------------------------------------*)
   150 
   151 (* FROM Tgs *)
   152 (* Note that the last temporal check is not mentioned in the original MIT
   153    specification. Adding it strengthens the guarantees assessed by the 
   154    protocol. Theorems that exploit it have the suffix `_refined'
   155 *) 
   156     K4  "[| evs4: kerberos; Key ServKey ~: used evs4; B ~= Tgs; 
   157             Says A' Tgs {|
   158              (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
   159 				 Number Tk|}),
   160              (Crypt AuthKey {|Agent A, Number Ta1|}), Agent B|}
   161 	        : set evs4;
   162             ~ ExpirAuth Tk evs4;
   163             ~ ExpirAutc Ta1 evs4; 
   164             ServLife + (CT evs4) <= AuthLife + Tk
   165          |]
   166           ==> Says Tgs A 
   167                 (Crypt AuthKey {|Key ServKey, Agent B, Number (CT evs4),  
   168 			       Crypt (shrK B) {|Agent A, Agent B, Key ServKey,
   169 		 			        Number (CT evs4)|} |})
   170 	        # evs4 : kerberos"
   171 (* Tgs creates a new session key per each request for a service, without 
   172    checking if there is still a fresh one for that service.
   173    The cipher under Tgs' key is the AuthTicket, the cipher under B's key
   174    is the ServTicket, which is built now.
   175    NOTE that the last temporal check is not present in the MIT specification.
   176   
   177 *)
   178 
   179 (*---------------------------------------------------------------------*)
   180 
   181 (* FROM the initiator *)
   182     K5  "[| evs5: kerberos;  
   183             Says A Tgs 
   184                 {|AuthTicket, (Crypt AuthKey {|Agent A, Number Ta1|} ),
   185 		  Agent B|}
   186               : set evs5;
   187             Says Tgs' A 
   188              (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} ) 
   189                 : set evs5;
   190             RecentResp Tt Ta1 |]
   191           ==> Says A B {|ServTicket,
   192 			 Crypt ServKey {|Agent A, Number (CT evs5)|} |}
   193                # evs5 : kerberos"
   194 (* Checks similar to those in K3. *)
   195 
   196 (*---------------------------------------------------------------------*)
   197 
   198 (* FROM the responder*)
   199      K6  "[| evs6: kerberos;
   200             Says A' B {|           
   201               (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} ),
   202               (Crypt ServKey {|Agent A, Number Ta2|} )|}
   203             : set evs6;
   204             ~ ExpirServ Tt evs6;
   205             ~ ExpirAutc Ta2 evs6
   206          |]
   207           ==> Says B A (Crypt ServKey (Number Ta2) )
   208                # evs6 : kerberos"
   209 (* Checks similar to those in K4. *)
   210 
   211 (*---------------------------------------------------------------------*)
   212 
   213 (* Leaking an AuthKey... *)
   214     Oops1 "[| evsO1: kerberos;  A ~= Spy;
   215               Says Kas A
   216                 (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, 
   217                                   AuthTicket|})  : set evsO1;
   218               ExpirAuth Tk evsO1 |]
   219           ==> Says A Spy {|Agent A, Agent Tgs, Number Tk, Key AuthKey|} 
   220                # evsO1 : kerberos"
   221 
   222 (*---------------------------------------------------------------------*)
   223 
   224 (*Leaking a ServKey... *)
   225     Oops2 "[| evsO2: kerberos;  A ~= Spy;
   226               Says Tgs A 
   227                 (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
   228                    : set evsO2;
   229               ExpirServ Tt evsO2 |]
   230           ==> Says A Spy {|Agent A, Agent B, Number Tt, Key ServKey|} 
   231                # evsO2 : kerberos"
   232 
   233 (*---------------------------------------------------------------------*)
   234 
   235 
   236 end